source: vis_dev/vis-2.3/share/help/lang_emptyCmd.txt @ 87

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

vis2.3
File size: 5.9 KB
Line 
1
2  lang_empty - perform language emptiness check on a flattened network
3     _________________________________________________________________
4
5   lang_empty  [-b]  [-d  <dbg_level>] [-f <dbg_file>] [-h] [-i] [-s] [-t
6   <time_out_period>] [-v <verbosity_level>] [-A <le_method>] [-D <dc_level>]
7   [-S <schedule>] [-L <lockstep_mode>]
8
9   Performs language emptiness check on a flattened network. The language is
10   not empty when there is a fair path starting at an initial state. Before
11   calling this command, the user should have initialized the design by calling
12   the command [1]init_verify.
13
14   A  fairness  constraint can be read in by calling the [2]read_fairness
15   command; if none is specified, all paths are taken to be fair.
16
17   The system is reduced automatically with respect to the set of fairness
18   constraints.  If  the  language  is not empty, a proof of this fact is
19   generated. A proof is a fair path starting at an initial state. This is
20   represented by a finite sequence of states starting at an initial state (the
21   stem) leading to a fair cycle, i.e., a cycle on which there lies a state
22   from each fairness condition.
23
24   Command options:
25
26   -b
27          Use backward analysis when performing debugging; the default is to
28          use forward analysis. This should be tried when the debugger spends a
29          large amount of time when creating a path to a fair cycle.
30
31   -d <dbg_level>
32          Specify whether to demonstrate a proof of the language non-emptiness
33
34          dbg_level must be one of the following:
35
36          0 : No debugging performed. This is the default.
37
38          1 : Generate a path to a fair cycle.
39
40   -f <dbg_file>
41          Write the debugger output to dbg_file.
42
43   -h
44          Print the command usage.
45
46   -m
47          Pipe debugger output through the UNIX utility more.
48
49   -i
50          Print  input  values  causing transitions between states during
51          debugging. Both primary and pseudo inputs are printed.
52
53   -s
54          Print debug output in the format accepted by the [3]simulate command.
55
56   -t <timeOutPeriod>
57          Specify the time out period (in seconds) after which the command
58          aborts. By default this option is set to infinity.
59
60   -v <verbosity_level>
61          Specify verbosity level. This sets the amount of feedback on CPU
62          usage and code status.
63
64          verbosity_level must be one of the following:
65
66          0 : No feedback provided. This is the default.
67
68          1 : Feedback on code location.
69
70          2 : Feedback on code location and CPU usage.
71
72   -A <le_method>
73          Specify whether the compositional SCC analysis algorithm, Divide and
74          Compose (DnC), is enabled for language emptiness checking. The DnC
75          algorithm first enumerates fair SCCs in an over-approximated abstract
76          model,  and then successively refines them in the more concrete
77          models. Since non-fair SCCs can be ignored in the more concrete
78          models, a potentially large part of the state space are pruned away
79          early on when the computations are cheap.
80
81          le_method must be one of the following:
82
83          0 : no use of Divide and Compose (Default).
84
85          1 : use Divide and Compose.
86
87   -D <dc_level>
88          Specify extent to which don't cares are used to simplify MDDs. Don't
89          cares are minterms on which the value taken by functions does not
90          affect the computation; potentially, these minterms can be used to
91          simplify MDDs and reduce time taken to perform MDD computations.
92
93          dc_level must be one of the following:
94
95          0 : No don't cares are used.
96
97          1 : Use unreachable states as don't cares. This is the default.
98
99   -S <schedule>
100          Specify schedule for GSH algorithm, which generalizes the Emerson-Lei
101          algorithm and is used to compute greatest fixpoints. The choice of
102          schedule  affects the sequence in which EX and EU operators are
103          applied. It makes a difference only when fairness constraints are
104          specified.
105          <schedule> must be one of the following:
106
107          EL : EU and EX operators strictly alternate. This is the default.
108
109          EL1 : EX is applied once for every application of all EUs.
110
111          EL2 : EX is applied repeatedly after each application of all EUs.
112
113          budget : a hybrid of EL and EL2.
114
115          random : enabled operators are applied in (pseudo-)random order.
116
117          off : GSH is disabled, and the old algorithm is used instead. The old
118          algorithm  uses  the  EL  , but the termination checks are less
119          sophisticated than in GSH.
120
121   -F
122          Use forward analysis in the computation of the greatest fixpoint.
123          This option is incompatible with -d 1 or higher and can only be used
124          with -D 1.
125
126   -L <lockstep_mode>
127          Use the lockstep algorithm, which is based on fair SCC enumeration.
128          <lockstep_mode> must be one of the following:
129
130          off : Lockstep is disabled. This is the default. Language emptiness
131          is checked by computing a hull of the fair SCCs.
132
133          on : Lockstep is enabled.
134
135          all : Lockstep is enabled; all fair SCCs are enumerated instead of
136          terminating as soon as one is found. This can be used to study the
137          SCCs of a graph, but it is slower than the default option.
138
139          n : (n is a positive integer). Lockstep is enabled and up to n fair
140          SCCs are enumerated. This is less expensive than all , but still less
141          efficient than on , even when n = 1 .
142     _________________________________________________________________
143
144   Last updated on 20100410 00h02
145
146References
147
148   1. file://localhost/projects/development/hsv/vis/common/doc/html/init_verifyCmd.html
149   2. file://localhost/projects/development/hsv/vis/common/doc/html/read_fairnessCmd.html
150   3. file://localhost/projects/development/hsv/vis/common/doc/html/simulateCmd.html
Note: See TracBrowser for help on using the repository browser.