source: vis_dev/vis-2.1/share/help/_grab_testCmd.txt @ 12

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

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