source: vis_dev/vis-2.1/share/help/lang_emptyCmd.txt @ 14

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

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