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