[11] | 1 | |
---|
| 2 | incremental_ctl_verification - Verify a set of CTL formulas by means of an |
---|
| 3 | incremental model checking algorithm. |
---|
| 4 | _________________________________________________________________ |
---|
| 5 | |
---|
| 6 | incremental_ctl_verification [-D <number>] [-e] [-h] [-n] \ [-s] [-t |
---|
| 7 | <seconds>] [-v <number>] [-V <number>] [-x] <ctlfile> |
---|
| 8 | |
---|
| 9 | Like model_check, incremental_ctl_verification verifies a set of CTL |
---|
| 10 | formulas. It uses a system of abstraction and incremental refinement |
---|
| 11 | that works for all of (fair)CTL, using over and underapproximations as |
---|
| 12 | appropriate. See [1,2] for details. |
---|
| 13 | |
---|
| 14 | Incremental_ctl_verification (also known as Abs or Trasgo) works |
---|
| 15 | especially well on large systems on which mc is too slow or runs out |
---|
| 16 | of memory. Unlike amc, it can handle full CTL, not just the universal |
---|
| 17 | or existential subsets of it. Also, fairness is supported with this |
---|
| 18 | command, although it tends to be inefficient. Support for the |
---|
| 19 | mu-calculus is not yet implemented. |
---|
| 20 | |
---|
| 21 | Before using incremental_ctl_verification, a flattened hierarchy |
---|
| 22 | should be present. See `help init`. Using dynamic variable reordering |
---|
| 23 | may be beneficial on large systems. See `help dynamic_var_ordering`. |
---|
| 24 | |
---|
| 25 | Fairness constraints can be applied using `read_fairness', as with mc. |
---|
| 26 | When using incremental verification with fairness, there is no check |
---|
| 27 | for unfair initial states. Please be aware that if there are no fair |
---|
| 28 | initial states, all formulas starting with "A" will be trivially true. |
---|
| 29 | Mc will tell you whether you have fair initial states. |
---|
| 30 | |
---|
| 31 | A typical use would be |
---|
| 32 | incremental_ctl_verification -D2 <ctl_file> |
---|
| 33 | |
---|
| 34 | For every formula, incremental verification will report whether it is |
---|
| 35 | valid or invalid, or it returns an inconclusive result. A formula is |
---|
| 36 | valid iff it holds for all initial states. An error trace is not |
---|
| 37 | provided. For the people who are used to mc: The -r option is not |
---|
| 38 | supported, incremental verification always reduces the fsm with |
---|
| 39 | respect to individual formulas. The -c option is not supported either. |
---|
| 40 | There is no sharing of subformulas between different formulas. |
---|
| 41 | |
---|
| 42 | Command options: |
---|
| 43 | |
---|
| 44 | -D <number> |
---|
| 45 | Specify extent to which don't cares are used to simplify the |
---|
| 46 | MDDs. |
---|
| 47 | |
---|
| 48 | + 0: No Don't Cares used. |
---|
| 49 | + 1: Use reachability information to compute the don't-care |
---|
| 50 | set. Reachability is performed by formula. This is different |
---|
| 51 | from mc, where reachability is performed only once. |
---|
| 52 | + 2: Use reachability information, and minimize the transition |
---|
| 53 | relation with respect to the `frontier set' (aggresive |
---|
| 54 | minimization). |
---|
| 55 | |
---|
| 56 | The equivalent of mc -D3 is not implemented. |
---|
| 57 | |
---|
| 58 | -e |
---|
| 59 | Compute the set of fair states (those satisfying the formula |
---|
| 60 | EGfair TRUE) before the verification process and use the result |
---|
| 61 | as care set. In certain cases this will speed up computation |
---|
| 62 | when fairness constraints are present. In other cases it will |
---|
| 63 | slow it down. |
---|
| 64 | |
---|
| 65 | -h |
---|
| 66 | Print the command usage. |
---|
| 67 | |
---|
| 68 | -n |
---|
| 69 | Try to prove the negation of every formula. In some cases it |
---|
| 70 | may be easier to prove the negation of a formula than the |
---|
| 71 | formula itself. For systems with only one initial state, a |
---|
| 72 | formula is true iff its negation is false. Note that for |
---|
| 73 | systems with multiple initial states a formula and its negation |
---|
| 74 | can both be false. |
---|
| 75 | |
---|
| 76 | -s |
---|
| 77 | Print a summary of statistics after the verification. |
---|
| 78 | |
---|
| 79 | -t <secs> |
---|
| 80 | Time in seconds allowed to spend in the verification. The |
---|
| 81 | default is infinity. |
---|
| 82 | |
---|
| 83 | -v <number> |
---|
| 84 | Specify verbosity level. Use 0 for no feedback (default), 1 for |
---|
| 85 | more and 2 for maximum feedback. This option can not be used in |
---|
| 86 | conjunction with -V. |
---|
| 87 | |
---|
| 88 | -V <number> |
---|
| 89 | Mask specifying type of information to be printed out while |
---|
| 90 | verifying the formulas. This allows for a finer control than |
---|
| 91 | -v. -V and -v cannot be used simultaneously. The mask is given |
---|
| 92 | as a binary number, by taking the logical or of the following |
---|
| 93 | binary values. One does not have to convert these numbers to |
---|
| 94 | decimal. |
---|
| 95 | |
---|
| 96 | 1 number of primary inputs and flip-flops |
---|
| 97 | |
---|
| 98 | 10 labeled operational graph of the formulas |
---|
| 99 | |
---|
| 100 | 100 cpu-time for the computation in each vertex |
---|
| 101 | |
---|
| 102 | 1000 cubes of the function sat for each vertex |
---|
| 103 | |
---|
| 104 | 10000 cubes of the function goalSet for each vertex |
---|
| 105 | |
---|
| 106 | 100000 vertex data structure contents after evaluation |
---|
| 107 | |
---|
| 108 | 1000000 cubes in the care set for every evaluation |
---|
| 109 | |
---|
| 110 | 10000000 size of care set for every evaluation |
---|
| 111 | |
---|
| 112 | 100000000 number of states that satisfy every sub-formula |
---|
| 113 | |
---|
| 114 | 1000000000 number of overall reachable states |
---|
| 115 | |
---|
| 116 | 10000000000 cubes for every iteration of a fixed point |
---|
| 117 | |
---|
| 118 | 100000000000 size of the BDD in each iteration in a fix-point |
---|
| 119 | |
---|
| 120 | 1000000000000 labeled operational graph in dot format |
---|
| 121 | |
---|
| 122 | 10000000000000 number of envelope states |
---|
| 123 | |
---|
| 124 | 100000000000000 number of states to be refined |
---|
| 125 | |
---|
| 126 | 1000000000000000 size of the refinement operands |
---|
| 127 | |
---|
| 128 | 10000000000000000 cubes of the refinement operands |
---|
| 129 | |
---|
| 130 | 100000000000000000 Number of latches before and after |
---|
| 131 | simplification |
---|
| 132 | |
---|
| 133 | 1000000000000000000 report partial progress (i.e. reach, |
---|
| 134 | EG(true),...) |
---|
| 135 | |
---|
| 136 | 10000000000000000000 Begin/End refinement process |
---|
| 137 | |
---|
| 138 | 100000000000000000000 Size of goal set |
---|
| 139 | |
---|
| 140 | 1000000000000000000000 cubes of the goal set |
---|
| 141 | |
---|
| 142 | 10000000000000000000000 Contents of vertex after refinement |
---|
| 143 | |
---|
| 144 | -x |
---|
| 145 | Perform the verification exactly. No approximation is done. |
---|
| 146 | |
---|
| 147 | <ctlfile> |
---|
| 148 | File containing the CTL formulas to be verified. |
---|
| 149 | |
---|
| 150 | Related "set" options: |
---|
| 151 | |
---|
| 152 | ctl_change_bracket <yes/no> |
---|
| 153 | Vl2mv automatically converts "[]" to "<>" in node names, |
---|
| 154 | therefore CTL parser does the same thing. However, in some |
---|
| 155 | cases a user does not want to change node names in CTL parsing. |
---|
| 156 | Then, use this set option by giving "no". Default is "yes". |
---|
| 157 | |
---|
| 158 | See also commands : model_check, incremental_ctl_verification |
---|
| 159 | |
---|
| 160 | 1. A. Pardo and G. Hachtel. Automatic abstraction techniques for |
---|
| 161 | propositional mu-calculus model checking. In 9th Conference on |
---|
| 162 | Computer Aided Verification (CAV'97). Springer-Verlag. Pages 12-23, |
---|
| 163 | 1997. |
---|
| 164 | |
---|
| 165 | 2. A. Pardo and G. Hachtel. Incremental CTL model checking using BDD |
---|
| 166 | subsetting. In 35th Design Automation Conference (DAC'98). pages |
---|
| 167 | 457-462, 1998. |
---|
| 168 | _________________________________________________________________ |
---|
| 169 | |
---|
| 170 | Last updated on 20050519 10h16 |
---|