source: vis_dev/vis-2.3/share/help/incremental_ctl_verificationCmd.txt @ 31

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

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