source: vis_dev/vis-2.3/share/help/_grab_testCmd.txt @ 64

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

vis2.3
File size: 4.2 KB
Line 
1
2  _grab_test - Performs invairant checking on a flattened network with the GRAB
3  abstraction refinement algorithm.
4     _________________________________________________________________
5
6   _grab_test [-a <refine_algorithm>] [-c <cex_type>] [-d <dbg_level>] [-F]
7   [-M] [-i] [-m] [-t <time_out_period>] [-v <verbosity_level>] [-f <dbg_file>]
8   [-h] <inv_file>
9
10   Performs invairant checking on a flattened network with the GRAB abstraction
11   refinement algorithm. Before calling this command, the user should have
12   created the flattened netowrk by calling the commands [1]flatten_hierarchy
13   and [2]build_partition_maigs. The default BDD manager and network partition
14   are not mandatory for calling this command, though they will be used if
15   available.  (In other words, the user doesn't have to run the commands
16   [3]static_order and [4]build_partition_mdds before calling this command.)
17   Regardless of the options, no 'false positive' or 'false negatives' will
18   occurs: the result is correct for the given model. Properties to be verified
19   should be provided as invariant formulae in the file inv_file. Node that the
20   support of any wire referred to in a formula should consist only of latches.
21   For the precise syntax of CTL and LTL formulas, see the [5]VIS CTL and LTL
22   syntax manual.
23
24   If  a  formula  does  not  pass,  a proof of failure (referred to as a
25   counter-example) is demonstrated. Whether demostrate the proof or not can be
26   specified (see option -d).
27
28   Command options:
29
30   -a <refine_algorithm>
31          Specify the refinement variable selection algorithm.
32
33          refine_algorithm must be one of the following:
34
35          GRAB: the GRAB refinement method (Default).
36
37   -c <cex_type>
38          Specify the type of abstract counter-examples used in the analysis.
39
40          cex_type must be one of the following:
41
42          0: minterm state counter-example.
43
44          1: cube state counter-example.
45
46          2: synchronous onion rings (Default).
47
48   -d <dbg_level>
49          Specify whether to demonstrate a counter-example when the system
50          fails a formula being checked.
51
52          dbg_level must be one of the following:
53
54          0: No debugging performed. dbg_level=0 is the default.
55
56          1: Generate a counter-example (a path to a fair cycle).
57
58   -F <finegrain_flag>
59          Enable or disable the use of fine-grain abstraction.
60
61          finegrain_flag must be one of the following:
62
63          0: disable fine-grain abstraction.
64
65          1: enable fine-grain abstraction (Default).
66
67   -M <refinemin_flag>
68          Enable or disable the use of greedy refinement minimization.
69
70          refinemin_flag must be one of the following:
71
72          0: disable greedy refinement minimization.
73
74          1: enable greedy refinement minimization (Default).
75
76   -i
77          Print  input  values  causing transitions between states during
78          debugging. Both primary and pseudo inputs are printed.
79
80   -m
81          Pipe debugger output through the UNIX utility more.
82
83   -t <timeOutPeriod>
84          Specify the time out period (in seconds) after which the command
85          aborts. By default this option is set to infinity.
86
87   -v <verbosity_level>
88          Specify verbosity level. This sets the amount of feedback on CPU
89          usage and code status.
90          verbosity_level must be one of the following:
91
92          0: No feedback provided. This is the default.
93
94          1: Feedback on code location.
95
96          2: Feedback on code location and CPU usage.
97
98   -f <dbg_out>
99          Specify the name of the file ot which error trace is written.
100
101   -h
102          Print the command usage.
103
104          See also commands : model_check, check_invariant
105            __________________________________________________________
106
107          Last updated on 20100410 00h02
108
109References
110
111   1. file://localhost/projects/development/hsv/vis/common/doc/html/flatten_hierarchyCmd.html
112   2. file://localhost/projects/development/hsv/vis/common/doc/html/build_partition_maigsCmd.html
113   3. file://localhost/projects/development/hsv/vis/common/doc/html/static_orderCmd.html
114   4. file://localhost/projects/development/hsv/vis/common/doc/html/build_partition_mddsCmd.html
115   5. file://localhost/projects/development/hsv/vis/common/doc/ctl/ctl/ctl.html
Note: See TracBrowser for help on using the repository browser.