incremental_ctl_verification - Verify a set of CTL formulas by means of an incremental model checking algorithm.

Like model_check, incremental_ctl_verification verifies a set of CTL formulas. It uses a system of abstraction and incremental refinement that works for all of (fair)CTL, using over and underapproximations as appropriate. See [1,2] for details.

Incremental_ctl_verification (also known as Abs or Trasgo) works especially well on large systems on which mc is too slow or runs out of memory. Unlike amc, it can handle full CTL, not just the universal or existential subsets of it. Also, fairness is supported with this command, although it tends to be inefficient. Support for the mu-calculus is not yet implemented.

Before using incremental_ctl_verification, a flattened hierarchy should be present. See `help init`. Using dynamic variable reordering may be benificial on large systems. See `help dynamic_var_ordering`.

Fairness constraints can be apllied using `read_fairness', as with mc. When using incremental verification with fairness, there is no check for unfair initial states. Please be aware that if there are no fair initial states, all formulas starting with "A" will be trivially true. Mc will tell you whether you have fair initial states.

A typical use would be
incremental_ctl_verification -D2 <ctl_file>

For every formula, incremental verification will report whether it is valid or invalid, or it returns an inconclusive result. A formula is valid iff it holds for all initial states. An error trace is not provided. For the people who are used to mc: The -r optoin is not supported, incremental verification always reduces the fsm with respect to individual formulas. The -c option is not supported either. There is no sharing of subformulas between different formulas.

Command options:

-D <number>

Specify extent to which don't cares are used to simplify the MDDs.

• 0: No Don't Cares used.
• 1: Use reachability information to compute the don't-care set. Reachability is performed by formula. This is different from mc, where reachability is performed only once.
• 2: Use reachability information, and minize the transition relation with respect to the `frontier set' (aggresive minimization).

The equivalent of mc -D3 is not implemented.

-e

Compute the set of fair states (those satisfying the formula EGfair TRUE) before the verification process and use the result as care set. In certain cases this will speed up computation when fairness constraints are present. In other cases it will slow it down.

-h

Print the command usage.

-n

Try to prove the negation of every formula. In some cases it may be easier to prove the negation of a formula than the formula itself. For systems with only one initial state, a formula is true iff its negation is false. Note that for systems with multiple initial states a formula and its negation can both be false.

-s

Print a summary of statistics after the verification.

-t <secs>

Time in seconds allowed to spend in the verification. The default is infinity.

-v <number>

Specify verbosity level. Use 0 for no feedback (default), 1 for more and 2 for maximum feedback. This option can not be used in conjunction with -V.

-V <number>

Mask specifying type of information to be printed out while verifying the formulas. This allows for a finer control than -v. -V and -v cannot be used simultaneously. The mask is given as a binary number, by taking the logical or of the following binary values. One does not have to convert these numbers to decimal.

1 number of primary inputs and flip-flops

10 labeled operational graph of the formulas

100 cpu-time for the computation in each vertex

1000 cubes of the function sat for each vertex

10000 cubes of the function goalSet for each vertex

100000 vertex data structure contents after evaluation

1000000 cubes in the care set for every evaluation

10000000 size of care set for every evaluation

100000000 number of states that satisfy every sub-formula

1000000000 number of overall reachable states

10000000000 cubes for every iteration of a fixed point

100000000000 size of the BDD in each iteration in a fix-point

1000000000000 labeled operational graph in dot format

10000000000000 number of envelope states

100000000000000 number of states to be refined

1000000000000000 size of the refinement operands

10000000000000000 cubes of the refinement operands

100000000000000000 Number of latches before and after simplification

1000000000000000000 report partial progress (i.e. reach, EG(true),...)

10000000000000000000 Begin/End refinement process

100000000000000000000 Size of goal set

1000000000000000000000 cubes of the goal set

10000000000000000000000 Contents of vertex after refinement

-x

Perform the verification exactly. No approximation is done.

<ctlfile>

File containing the CTL formulas to be verified.

Related "set" options:

ctl_change_bracket <yes/no>

Vl2mv automatically converts "[]" to "<>" in node names, therefore CTL parser does the same thing. However, in some cases a user does not want to change node names in CTL parsing. Then, use this set option by giving "no" Default is "yes".

See also commands : model_check, incremental_ctl_verification

1. A. Pardo and G. Hachtel. Automatic abstraction techniques for propositional mu-calculus model checking. In 9th Conference on Computer Aided Verification (CAV'97). Springer-Verlag. Pages 12-23, 1997.

2. A. Pardo and G. Hachtel. Incremental CTL model checking using BDD subsetting. In 35th Design Automation Conference (DAC'98). pages 457-462, 1998.