[11] | 1 | |
---|
| 2 | iterative_model_check - Perform CTL model checking on an abstracted system |
---|
| 3 | with automatic refinement algorithm. |
---|
| 4 | _________________________________________________________________ |
---|
| 5 | |
---|
| 6 | iterative_model_check [-h] [-x] [-t <seconds>] [-v <number>]\ [-D |
---|
| 7 | <number>] [-r <number>] [-i <number>] \ [-p <number>] [-g <number>] |
---|
| 8 | <ctlfile> |
---|
| 9 | |
---|
| 10 | Command options: |
---|
| 11 | |
---|
| 12 | -h |
---|
| 13 | Print the command usage. |
---|
| 14 | |
---|
| 15 | -x |
---|
| 16 | Perform the verification exactly. No approximation is done. |
---|
| 17 | |
---|
| 18 | -t <secs> |
---|
| 19 | Time in seconds allowed for verification. The default is no |
---|
| 20 | limit. |
---|
| 21 | |
---|
| 22 | -v <number> |
---|
| 23 | Specify verbosity level. Use 0 for no feedback (default), 1 for |
---|
| 24 | more, and 2 for maximum feedback. |
---|
| 25 | |
---|
| 26 | -D <number> |
---|
| 27 | Specify extent to which don't cares are used to simplify the |
---|
| 28 | MDDs. |
---|
| 29 | |
---|
| 30 | + 0: No don't cares used. This is the default. |
---|
| 31 | + 1: Use reachability information to compute the don't-care |
---|
| 32 | set. |
---|
| 33 | + 2: Use reachability information, and minimize the transition |
---|
| 34 | relation with respect to the `frontier set' (aggresive |
---|
| 35 | minimization). |
---|
| 36 | + 3: Use approximate reachability information. |
---|
| 37 | |
---|
| 38 | -r <number> |
---|
| 39 | Specify refinement method. |
---|
| 40 | |
---|
| 41 | + 0: Static scheduling by name sorting. Fast, easy, but less |
---|
| 42 | accurate. |
---|
| 43 | + 1: Static scheduling by latch affinity. Slow, but more |
---|
| 44 | accurate. This is the default. |
---|
| 45 | |
---|
| 46 | -i <number> |
---|
| 47 | The number of state variables to be added for exact computation |
---|
| 48 | at each iteration. The default is 4. |
---|
| 49 | |
---|
| 50 | -l <number> |
---|
| 51 | Type of lower-bound approximation method. |
---|
| 52 | |
---|
| 53 | + 0: Take a subset of each transition sub-relation by BDD |
---|
| 54 | subsetting. |
---|
| 55 | + 1: Take a subset by universal quantification. This is the |
---|
| 56 | default. |
---|
| 57 | |
---|
| 58 | -p <number> |
---|
| 59 | Type of partition method. If 'build_partition_mdds' is already |
---|
| 60 | invoked, this option is ignored. Notice that some next state |
---|
| 61 | functions might not be available after iterative_model_checking |
---|
| 62 | command is performed because of this option. |
---|
| 63 | |
---|
| 64 | + 0: Build all next state functions. Same as |
---|
| 65 | 'build_partition_mdds'. This is the default. |
---|
| 66 | + 1: Build the next state functions related to the formulas. |
---|
| 67 | Build all next state functions that are necessary to prove |
---|
| 68 | all formulas. |
---|
| 69 | + 2: Build the next state functions incrementally. None of next |
---|
| 70 | state functions are removed. |
---|
| 71 | |
---|
| 72 | -g <number> |
---|
| 73 | Type of operational graph. |
---|
| 74 | |
---|
| 75 | + 0: Negative Operational Graph. Good to prove a formula true. |
---|
| 76 | + 1: Positive Operational Graph. Good to prove a formula false. |
---|
| 77 | + 2: Mixed Operational Graph. Good to prove any formula, but it |
---|
| 78 | may be slower. This is the default. |
---|
| 79 | |
---|
| 80 | <ctlfile> |
---|
| 81 | File containing the CTL formulas to be verified. |
---|
| 82 | |
---|
| 83 | Related "set" options: |
---|
| 84 | |
---|
| 85 | ctl_change_bracket <yes/no> |
---|
| 86 | Vl2mv automatically converts "[]" to "<>" in node names, |
---|
| 87 | therefore CTL parser does the same thing. However, in some |
---|
| 88 | cases a user does not want to change node names in CTL parsing. |
---|
| 89 | Then, use this set option by giving "no". Default is "yes". |
---|
| 90 | |
---|
| 91 | See also commands : model_check, incremental_ctl_verification |
---|
| 92 | |
---|
| 93 | 1. Jae-Young Jang, In-Ho Moon, and Gary D. Hachtel. Iterative |
---|
| 94 | Abstraction-based CTL Model Checking. Design, Automation and Test in |
---|
| 95 | Europe (DATE), 2000 |
---|
| 96 | |
---|
| 97 | 2. Jae-Young Jang. Iterative Abstraction-based CTL Model Checking. Ph. |
---|
| 98 | D. Thesis. University of Colorado, 1999. |
---|
| 99 | _________________________________________________________________ |
---|
| 100 | |
---|
| 101 | Last updated on 20050519 10h16 |
---|