Questions tagged [ctl]

83 questions
7
votes
2 answers

LTL, CTL or TLA for modelling for my model (detailed description inside)?

I am currently writing my master thesis and am confronted with specifying and verifying my approach in a temporal logic. Which temporal logic would be the best to use in my circumstances? I would really like some feedback on my approach and how to…
nanoquack
  • 949
  • 2
  • 9
  • 26
5
votes
2 answers

Client Certificates and FireFox

I need some help to understand what is happening with my web application. I have a simple web app (c# .Net 2.0) that uses a smartcard authentication. In my testing box (win 2k3 32 bits, iis6) everything works fine but in my production box (win2k3…
GRGodoi
  • 1,946
  • 2
  • 24
  • 38
4
votes
3 answers

Certificate Trust Lists and IIS7

I need to generate a CTL for use with IIS7. I generated a CTL file using MakeCTL (on Win2k3 SDK) and put only my own RootCA certificate in the CTL. However, when I then use adsutil.vbs to set my website to use this CTL, I get: ErrNumber: -2147023584…
Neil Deadman
4
votes
1 answer

pgloader - fast data loading for PostgreSQL

I would like to accelerate loading data to PostgreSQL. I started using the pgloader https://github.com/dimitri/pgloader and wanted to utilize parallel loading. I was tinkering with different parameters but I couldn't activate more than two cores on…
ady
  • 1,108
  • 13
  • 19
2
votes
3 answers

SQL Loader ctl file - how to skip columns

Let's say in my database 4 columns: Column1, Column2, Column3, Column4 My data file is CSV file (comma delimited, length of column is unknown): xxx,yyy,zzz,000 a,bb,ccccc,ddddddd 1,2,3,4 The CTL will be: LOAD DATA INTO TABLE "TABLE"…
kenny
  • 2,000
  • 6
  • 28
  • 38
2
votes
4 answers

Linear Temporal Logic Questions (2)

If you are not familiar with LTL (linear temporal logic), please skip this question! And yes, LTL is very significant to programming, as it is a core to the model checking system we use to verify programs. Given these proposition symbols and their…
CODe
  • 2,253
  • 6
  • 36
  • 65
2
votes
1 answer

Check CTL specification in SMV

When I try to check "EG (!s11included & !s10included)" in SMV, it is reported false and gives a counter example as follows, which I think on the contrary it support this CTL specification. Is there something wrong with my CTL specification? --…
2
votes
1 answer

How do you read a set of atomic propositions?

I am given the above system for atomic propositions {a,b,c}. I'm then meant to say if certain LTL formulae hold (such as ♢☐c). I understand what the LTL formulae mean (eventually forever c holds) but I have no idea how to read the diagram and…
Aequitas
  • 2,205
  • 1
  • 25
  • 51
2
votes
1 answer

NuSMV passes wrong specification

I am new to NuSMV and CTL and was trying simple Examples. I have 3 states A, B, and C and there is a transition from A-> B I modeled it in NuSMV and want to check if there is any execution path from B to A. Eventhough I have not defined such…
karthi
  • 2,762
  • 4
  • 30
  • 28
2
votes
0 answers

Stop Postgres via windows service

I am currently setting up a c# app to allow me to control applications on my windows 2012 server. Architecture: Master Server - Postgres x64 9.3 running from a windows service as read/write database, with hot-standby mode and a replication…
Mr.Adam
  • 294
  • 5
  • 23
2
votes
2 answers

How to trim the new line character of column data in ctl file of SQL Loader

My table data has contains new line character it is loading from sql loader ctl file, one column called 'IPADDRESS'is loading with new line character: My ctl file : load data INFILE 'abc.txt' INTO TABLE TABLENAME APPEND FIELDS TERMINATED BY…
Chaya
  • 95
  • 3
  • 12
2
votes
1 answer

CTL fomula until contains implication

when I use NuSMV tools to verify if my CTL is right, I encounter a problem that make me so confused. My model is and here's the NuSMV code: MODULE main VAR state : {ROOT, A1, B1, C1, D1, F1, M1}; ASSIGN init(state) := ROOT; next(state) :=…
2
votes
2 answers

constructing valid CTL or LTL expression (in NuSMV)

I'm trying to create a valid CTL or LTL expression for model checking in NuSMV. I have a variable in a game, with actors running around trying to catch each other. Variable is, State_Of_Game : {Win,Lose,Playing} and I want to express that from every…
Sven
  • 1,133
  • 1
  • 11
  • 22
2
votes
3 answers

Insert and update rows from a file in oracle

I have a file in linux, the file is something like: (I have millions of rows) date number name id state 20131110 1089 name1 123 start 20131110 1080 name2 …
user2768380
  • 151
  • 1
  • 5
  • 21
2
votes
1 answer

Load CSV with SQLLDR (Rejected)

i have CSV file. i want to load content of csv file to oracle database with SQLLDR. My SQLLDR is @echo off sqlldr black@user/password data=D:\csv\data.csv control=D:\ctl\loader.ctl log=D:\ctl \loader.log bad=D:\ctl\loader.bad pause My loader.ctl…
flyingbird013
  • 446
  • 2
  • 12
  • 28
1
2 3 4 5 6