source: vis_dev/vis-2.1/share/help/iterative_model_checkCmd.txt @ 11

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

Add vis
File size: 3.8 KB
Line 
1
2  iterative_model_check - Perform CTL model checking on an abstracted system
3  with automatic refinement algorithm.
4     _________________________________________________________________
5
6   iterative_model_check  [-h]  [-x]  [-t  <seconds>]  [-v <number>]\ [-D
7   <number>]  [-r  <number>]  [-i <number>] \ [-p <number>] [-g <number>]
8   <ctlfile>
9
10   Command options:
11
12   -h
13          Print the command usage.
14
15   -x
16          Perform the verification exactly. No approximation is done.
17
18   -t <secs>
19          Time  in  seconds  allowed  for verification. The default is no
20          limit.
21
22   -v <number>
23          Specify verbosity level. Use 0 for no feedback (default), 1 for
24          more, and 2 for maximum feedback.
25
26   -D <number>
27          Specify  extent  to  which don't cares are used to simplify the
28          MDDs.
29
30          + 0: No don't cares used. This is the default.
31          + 1:  Use  reachability  information  to compute the don't-care
32            set.
33          + 2:  Use reachability information, and minimize the transition
34            relation  with  respect  to  the  `frontier  set'  (aggresive
35            minimization).
36          + 3: Use approximate reachability information.
37
38   -r <number>
39          Specify refinement method.
40
41          + 0:  Static  scheduling  by name sorting. Fast, easy, but less
42            accurate.
43          + 1:  Static  scheduling  by  latch  affinity.  Slow,  but more
44            accurate. This is the default.
45
46   -i <number>
47          The number of state variables to be added for exact computation
48          at each iteration. The default is 4.
49
50   -l <number>
51          Type of lower-bound approximation method.
52
53          + 0:  Take  a  subset  of  each  transition sub-relation by BDD
54            subsetting.
55          + 1:  Take  a  subset  by universal quantification. This is the
56            default.
57
58   -p <number>
59          Type  of partition method. If 'build_partition_mdds' is already
60          invoked,  this  option  is ignored. Notice that some next state
61          functions might not be available after iterative_model_checking
62          command is performed because of this option.
63
64          + 0:    Build    all    next    state    functions.   Same   as
65            'build_partition_mdds'. This is the default.
66          + 1:  Build  the  next state functions related to the formulas.
67            Build  all  next  state functions that are necessary to prove
68            all formulas.
69          + 2: Build the next state functions incrementally. None of next
70            state functions are removed.
71
72   -g <number>
73          Type of operational graph.
74
75          + 0: Negative Operational Graph. Good to prove a formula true.
76          + 1: Positive Operational Graph. Good to prove a formula false.
77          + 2: Mixed Operational Graph. Good to prove any formula, but it
78            may be slower. This is the default.
79
80   <ctlfile>
81          File containing the CTL formulas to be verified.
82
83   Related "set" options:
84
85   ctl_change_bracket <yes/no>
86          Vl2mv  automatically  converts  "[]"  to  "<>"  in  node names,
87          therefore  CTL  parser  does  the  same thing. However, in some
88          cases a user does not want to change node names in CTL parsing.
89          Then, use this set option by giving "no". Default is "yes".
90
91   See also commands : model_check, incremental_ctl_verification
92
93   1.  Jae-Young  Jang,  In-Ho  Moon,  and  Gary  D.  Hachtel.  Iterative
94   Abstraction-based  CTL  Model Checking. Design, Automation and Test in
95   Europe (DATE), 2000
96
97   2. Jae-Young Jang. Iterative Abstraction-based CTL Model Checking. Ph.
98   D. Thesis. University of Colorado, 1999.
99     _________________________________________________________________
100
101   Last updated on 20050519 10h16
Note: See TracBrowser for help on using the repository browser.