source: vis_dev/vis-2.1/share/help/incremental_ctl_verificationCmd.txt @ 14

Last change on this file since 14 was 11, checked in by cecile, 13 years ago

Add vis
File size: 6.9 KB
Line 
1
2  incremental_ctl_verification - Verify a set of CTL formulas by means of an
3  incremental model checking algorithm.
4     _________________________________________________________________
5
6   incremental_ctl_verification  [-D  <number>] [-e] [-h] [-n] \ [-s] [-t
7   <seconds>] [-v <number>] [-V <number>] [-x] <ctlfile>
8
9   Like  model_check,  incremental_ctl_verification verifies a set of CTL
10   formulas.  It  uses a system of abstraction and incremental refinement
11   that works for all of (fair)CTL, using over and underapproximations as
12   appropriate. See [1,2] for details.
13
14   Incremental_ctl_verification  (also  known  as  Abs  or  Trasgo) works
15   especially  well  on large systems on which mc is too slow or runs out
16   of  memory. Unlike amc, it can handle full CTL, not just the universal
17   or  existential  subsets  of it. Also, fairness is supported with this
18   command,  although  it  tends  to  be  inefficient.  Support  for  the
19   mu-calculus is not yet implemented.
20
21   Before   using  incremental_ctl_verification,  a  flattened  hierarchy
22   should  be present. See `help init`. Using dynamic variable reordering
23   may be beneficial on large systems. See `help dynamic_var_ordering`.
24
25   Fairness constraints can be applied using `read_fairness', as with mc.
26   When  using  incremental verification with fairness, there is no check
27   for  unfair  initial states. Please be aware that if there are no fair
28   initial states, all formulas starting with "A" will be trivially true.
29   Mc will tell you whether you have fair initial states.
30
31   A typical use would be
32   incremental_ctl_verification -D2 <ctl_file>
33
34   For  every formula, incremental verification will report whether it is
35   valid  or  invalid, or it returns an inconclusive result. A formula is
36   valid  iff  it  holds  for  all  initial states. An error trace is not
37   provided.  For  the  people  who  are used to mc: The -r option is not
38   supported,  incremental  verification  always  reduces  the  fsm  with
39   respect to individual formulas. The -c option is not supported either.
40   There is no sharing of subformulas between different formulas.
41
42   Command options:
43
44   -D <number>
45          Specify  extent  to  which don't cares are used to simplify the
46          MDDs.
47
48          + 0: No Don't Cares used.
49          + 1:  Use  reachability  information  to compute the don't-care
50            set.  Reachability is performed by formula. This is different
51            from mc, where reachability is performed only once.
52          + 2:  Use reachability information, and minimize the transition
53            relation  with  respect  to  the  `frontier  set'  (aggresive
54            minimization).
55
56          The equivalent of mc -D3 is not implemented.
57
58   -e
59          Compute  the  set  of fair states (those satisfying the formula
60          EGfair TRUE) before the verification process and use the result
61          as  care  set.  In certain cases this will speed up computation
62          when  fairness  constraints are present. In other cases it will
63          slow it down.
64
65   -h
66          Print the command usage.
67
68   -n
69          Try  to  prove  the negation of every formula. In some cases it
70          may  be  easier  to  prove  the  negation of a formula than the
71          formula  itself.  For  systems  with  only one initial state, a
72          formula  is  true  iff  its  negation  is  false. Note that for
73          systems with multiple initial states a formula and its negation
74          can both be false.
75
76   -s
77          Print a summary of statistics after the verification.
78
79   -t <secs>
80          Time  in  seconds  allowed  to  spend  in the verification. The
81          default is infinity.
82
83   -v <number>
84          Specify verbosity level. Use 0 for no feedback (default), 1 for
85          more and 2 for maximum feedback. This option can not be used in
86          conjunction with -V.
87
88   -V <number>
89          Mask  specifying  type  of  information to be printed out while
90          verifying  the  formulas.  This allows for a finer control than
91          -v.  -V and -v cannot be used simultaneously. The mask is given
92          as  a  binary number, by taking the logical or of the following
93          binary  values.  One  does not have to convert these numbers to
94          decimal.
95
96          1 number of primary inputs and flip-flops
97
98          10 labeled operational graph of the formulas
99
100          100 cpu-time for the computation in each vertex
101
102          1000 cubes of the function sat for each vertex
103
104          10000 cubes of the function goalSet for each vertex
105
106          100000 vertex data structure contents after evaluation
107
108          1000000 cubes in the care set for every evaluation
109
110          10000000 size of care set for every evaluation
111
112          100000000 number of states that satisfy every sub-formula
113
114          1000000000 number of overall reachable states
115
116          10000000000 cubes for every iteration of a fixed point
117
118          100000000000 size of the BDD in each iteration in a fix-point
119
120          1000000000000 labeled operational graph in dot format
121
122          10000000000000 number of envelope states
123
124          100000000000000 number of states to be refined
125
126          1000000000000000 size of the refinement operands
127
128          10000000000000000 cubes of the refinement operands
129
130          100000000000000000   Number   of   latches   before  and  after
131          simplification
132
133          1000000000000000000   report   partial  progress  (i.e.  reach,
134          EG(true),...)
135
136          10000000000000000000 Begin/End refinement process
137
138          100000000000000000000 Size of goal set
139
140          1000000000000000000000 cubes of the goal set
141
142          10000000000000000000000 Contents of vertex after refinement
143
144   -x
145          Perform the verification exactly. No approximation is done.
146
147   <ctlfile>
148          File containing the CTL formulas to be verified.
149
150   Related "set" options:
151
152   ctl_change_bracket <yes/no>
153          Vl2mv  automatically  converts  "[]"  to  "<>"  in  node names,
154          therefore  CTL  parser  does  the  same thing. However, in some
155          cases a user does not want to change node names in CTL parsing.
156          Then, use this set option by giving "no". Default is "yes".
157
158   See also commands : model_check, incremental_ctl_verification
159
160   1.  A.  Pardo  and  G.  Hachtel.  Automatic abstraction techniques for
161   propositional   mu-calculus  model  checking.  In  9th  Conference  on
162   Computer  Aided  Verification  (CAV'97). Springer-Verlag. Pages 12-23,
163   1997.
164
165   2.  A.  Pardo and G. Hachtel. Incremental CTL model checking using BDD
166   subsetting.  In  35th  Design  Automation  Conference  (DAC'98). pages
167   457-462, 1998.
168     _________________________________________________________________
169
170   Last updated on 20050519 10h16
Note: See TracBrowser for help on using the repository browser.