source: vis_dev/vis-2.3/share/help/check_invariant_satCmd.txt @ 19

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

vis2.3
File size: 1.1 KB
Line 
1
2  check_invariant_sat - Check invariant property using sat based unmounded
3  model checking
4     _________________________________________________________________
5
6   check_invariant_sat  [-h]  [-d] [-t <timeOutPeriod>] [-m <method>] [-v
7   <verbosity_level>] <inv_file>
8
9   Perform  SAT-based unbounded model checking on And-Inverter-Graph. The
10   command compute fixed point of AG using AX operation. AX is implemented
11   using AllSAT enumeration algorithm. Command options:
12
13   -d
14          Disable inclusion test on initial states.
15
16   -v <verbosity_level>
17          Specify verbosity level. This sets the amount of feedback on CPU
18          usage and code status.
19
20   -t <timeOutPeriod>
21          Specify the time out period (in seconds) after which the command
22          aborts. By default this option is set to infinity.
23
24   -m <method>
25          Specify the method for AllSAT algorithm.
26
27   -h
28          Print the command usage.
29
30   <inv_file>
31   File containing Invariant formulae to be checked.
32     _________________________________________________________________
33
34   Last updated on 20100410 00h02
Note: See TracBrowser for help on using the repository browser.