User manual/pbes2bool

From MCRL2

Determine whether a PBES is valid by translating it to a BES.

Synopsis

pbes2bool [OPTIONS]... [[INFILE] [OUTFILE]]

Short description

The tool pbes2bool computes a boolean equation system (BES) of the parameterised boolean equation system (PBES) in INFILE. Unless indicated otherwise, pbes2bool subsequently tries to solve the BES.

Options

OPTION can be any of the following:

-c --counter

print at the end a tree labelled with instantiations of the left hand side of equations; this tree is an indication of how pbes2bool came to the validity/invalidity of the PBES

-H --hashtables

use hashtables when substituting in bes equations, and translate internal expressions to binary decision diagrams (the use of this flag is discouraged, due to heavy performance penalties)

-oFORMAT --output=FORMAT

use output format FORMAT:

• 'none': no output is printed, and the BES is solved within pbes2bool (default)
• 'cwi': output is printed is a very straightforward BES format to be used by tools developed at CWI; the BES is not solved
• 'vasy': output BES is printed for use within the CADP toolset; the BES is not solved
• 'pbes': output BES in internal PBES format suitable for further processing in the toolset; the BES is not solved

-p --precompile

precompile the pbes for faster rewriting; does not work when the toolset is compiled in debug mode

-rNAME --rewriter=NAME

use rewrite strategy NAME

-sNUMBER --strategy=NUMBER

use strategy NUMBER (default '0') to generate the BES:

• '0': Compute all boolean equations which can be reached from the initial state, without any optimization. This is is the most data efficient option per generated equation. (default)
• '1': Optimize by immediately substituting the right hand sides for already investigated variables that are true or false when generating an expression. This is as memory efficient as strategy 0.
• '2': In addition to '1', also substitute variables that are true or false into an already generated right hand sides. This can mean that certain variables become unreachable (e.g. X0 in X0 && X1,when X1 becomes false, assuming X0 does not occur elsewhere. It will be maintained which variables have become unreachable as these do not have to be investigated. Depending on the PBES, this can reduce the size of the generated BES substantially, but requires a larger memory footstamp.
• '3': In addition to '2', investigate for generated variables whether they occur on a loop, such that they can be set to true or false, depending on the fixed point symbol. This can increase the time needed to generate an equation substantially.

-t --tree

store state in a tree (for memory efficiency, comes with a small performance penalty)

-u --unused-data

do not remove unused parts of the data specification

Standard options:

-q, --quiet

do not display warning messages

-v, --verbose

display short intermediate messages

-d, --debug

display detailed intermediate messages

-h, --help

display help information

--version

display version information

Known issues

The counter example generated when the approximation algorithm of boolean equations is being used is in general huge and not very helpful. This algorithm is always employed with strategies 0 and 1. With strategies 2 and 3 it can be that when generating the boolean equation system from a PBES, it is already detected that the initial instantiated variable is either true or false and the approximation algorithm is not necessary. Counter examples in this case are compact (although we have no proof that the counter examples are always optimal) and also very helpful.

Detailed description

Generation of a BES

A BES is generated as follows. First the initial instantiated variable is considered. The instantiated right hand side for this variable is calculated, where all expressions without PBES variables are eliminated. Expressions are reduced to true or false and quantifiers are eliminated by enumerating its elements. As an example consider the PBES (where we use natural numbers as parameters, but these could be different of course).

pbes mu X(n:Nat)=(n<5)||(forall m:Nat.(m<=n+1) => X(m));
init X(0);

The initial instantiated variable is X(0). The right hand side belonging to X(0) is

(0<5)||(forall m:Nat.(m<=0+1) => X(m))

which using rewriting reduces to:

(forall m:Nat.(m<=1) => X(m))

The variable m can either be 0 or 1. Using that natural numbers are defined by constructors, a technique called narrowing is used, using which it is calculated that 0 and 1 are the only useful values for m. The expression reduces to:

X(0) && X(1)

So, the first boolean equation that results is

mu X(0)=X(0) && X(1)

The next step is to calculate the equation for X(1).

Strategies

There are different strategies to generate the equations. In strategy 0, all equations are generated in a breadth first search. The equations generated in the order the instantiated variables are encountered.

In strategy 1, a small improvement is made. If an equation of the form

nu X(17)=(X(10) && X(18)) || X(19)

is encountered and the right hand side for X(10) is false, then by substitution false for X(10) the equation reduces to

nu X(17)=X(19)

Note that the instantiated variable X(18) disappears. It can be that X(18) does not have to be investigated at all, saving work compared to strategy 0.

The idea of substituting true and false and avoiding unnecessary work is taken one step further in strategy 2. Here, whenever a right hand side of an instantiated bes variable is true or false, this value is substituted for the instantiated variable every where. The advantage of strategy 2 is that when the validity of a modal formula can be detected by only investigating parts of the state space, this is detected. The costs of strategy 2 is a higher memory footprint than for strategy 0 and 1.

Consider the following partially generated BES from some PBES, which typically is the result of a deadlock check on a transition system with a deadlock.

nu X(0)=X(1) && X(2) && X(3)
nu X(1)=X(4) && X(5) 
nu X(2)=X(6)
nu X(3)=false

With strategy 2, the value for X(3) will be substituted. The result is that X(0) becomes false. Furthermore, the instantiated variables X(1) and X(2) cannot be reached and have become superfluous. Using strategy 2, a garbage collection algorithm prevents such variables from being investigated.

Strategy 3 is very comparable to strategy 2, except that when a dependency loop of instantiated variables is detected, it attempts to set all the variables in the loop to true in case the fixpoint symbol is a nu, or false if it is a mu. For example

nu X(38)=X(39)
nu X(39)=X(38)

it can set both X(38) and X(39) to true. Moreover, following strategy 2, it can subsequently substitute true for X(38) and X(39) in the generated equations.

Solving a BES

After the BES is generated, it can be solved. For this a backward approximation technique is followed. First all instantiated BES variables of the highest alternation depth are calculated. The variables are all simultaneously set to true or false depending on the fixpoint symbol at this depth. By a normal fixpoint iteration, a stable solution is calculated. This process must be symbolic, as variables at lower alternation depths can still occur in the approximation.

The results of this approximation are substituted in all equations of lower alternation depth, just as in Gauss-elimination. In a sense this is the ordinary Gauss elimination process, except that it treats all variables at the same alternation depth at once. For instance when the alternation depth is 0, i.e. there is no alternation, this approximation process converges in linear time. For arbitrary nesting depths, this procedure is exponential.

Generation of counter examples

It is possible to let pbes2bool generate a counter example. As it stands, counterexamples are most useful when generated with strategy 2. A counterexample is a tree with the initial instantiated pbes variable as its root. The branches of each node are printed as lines with two extra spaces of indentation. These branches are labelled with instantiated pbes variables of which the value determined the value of our node. Typically a counter example looks like:

Solving the BES with 10 equations.
The pbes is not valid
Below the justification for this outcome is listed
1: X(0)
  2: Subst:false X(2)
    4: Subst:false X(5)
  3: Subst:false X(9)

This says that when solving X(0), it could be determined that it had solution false, because X(2) and X(9) where also false. The instantiated variable X(2) was false because X(5) was false. Apparently, X(5) and X(9) where invalid by itself.

The phrase Subst:false indicates the reason why a substitution was made. The following indications exist:

Mu Cycle

the variable is set to false because it is part of a cycle in a class of variables that all have the same alternation depth, and are preceded by a mu (strategy 3).

Nu Cycle

as in a Mu Cycle, except that the variable is set to true and the variables are preceded by nu (strategy 3).

Subst:false

false is substituted using back or forward substitution (strategy 2).

Subst:true

the value true is substituted using back or forward substitution (strategy 2).

FSubst:false

the value false is substituted by forward substition (strategy 1).

FSubst:true

the value true is substituted by backward substitution (strategy 1).

Set:false

variable is set to false (currently not used).

Set:true

variable is set to true (currently not used).

Appr:false

false is substitued for the variable when solving it using approximation.

Appr:true

true is substituted for the variable when solving it using approximation.

Approxim

a value not equal to true or false is substituted when solving the BES using approximation.

Sometimes the counterexample is recursive, or has re-occuring parts. these parts are only given once in the counterexample. A * at the end of a line in the counterexample indicates that this instantiated variable did already occur earlier in the counterexample and therefore, the reasons why it is true or false are not printed again.

Author

Written by Jan Friso Groote.

Bug reporting

Report bugs at our issue tracking system.

pbesinst

pbesconstelm