Rev | Line | |
---|
[14] | 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.