source: vis_dev/vis-2.3/share/help/iterative_model_checkCmd.txt @ 29

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

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