The tool uses the algorithm from pbes2bes for generating a BES in case the input file is a PBES.

Note

Also see pbes2bes for a description of the strategies that are referred to in this tool description.

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.

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.

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.

```
pbes2bool [OPTION]...[INFILE]
```

Solves (P)BES from INFILE. If INFILE is not present, stdin is used.

`--approximate-false`

If set, variables that are removed from the todo buffer are set to true. This means that the result false is reliable, and the result true can still mean that the formula is false. Without this flag true is approximated, meaning that true is the reliable answer, and false is not.

`-c`

, `--counter`

print evidence why the formula is valid or invalid. If invalid this information can be used to construct a counterexample using the tool lpsxsim. The evidence consists of a tree labelled with instantiations of the left hand side of PBES equations. These instantiations largely match the states of the lps. An indentation corresponds in general with one (sometimes zero, sometimes more) transition.

`-eLEVEL`

, `--eraseLEVEL`

use remove level LEVEL to remove bes variables

`none`

never remove a generated bes variable and its equation. This can lead to excessive memory usage.

`some`

remove generated bes variables that do not occur anymore in the generated BES, except if the right hand side of its equation is true or false. The rhss of removed variables must have to be recalculated, when this bes variable is encountered again.

`all`

remove the equation for bes variables that do not occur anymore in generated boolean equation system. This is quite memory efficient, but it can be very time consuming as the rhss of removed bes variables may have to be recalculated quite often.

`-iFORMAT`

, `--inFORMAT`

use input format FORMAT:

`bes`

BES in internal format

`pbes`

PBES in internal format

`pgsolver`

BES in PGSolver format

`text`

PBES in textual (mCRL2) format

`-QNUM`

, `--qlimitNUM`

limit enumeration of quantifiers to NUM variables. (Default NUM=1000, NUM=0 for unlimited).

`-rNAME`

, `--rewriterNAME`

use rewrite strategy NAME:

`jitty`

jitty rewriting

`jittyc`

compiled jitty rewriting

`jittyp`

jitty rewriting with prover

`-zSEARCH`

, `--searchSEARCH`

use search strategy SEARCH:

`breadth-first`

Compute the right hand side of the boolean variables in a first come first served basis. This is comparable with a breadth-first search. This is good for generating counter examples.

`depth-first`

Compute the right hand side of a boolean variables where the last generated variable is investigated first. This corresponds to a depth-first search. This can substantially outperform breadth-first search when the validity of a formula is determined after a larger depths.

`b`

Short hand for breadth-first.

`d`

Short hand for depth-first.

`-gSTRATEGY`

, `--solverSTRATEGY`

This flag selects the solver using which the generated bes is solved.

`lf`

Local fixpoints (advanced form of Gauss elimination, especially effective without alternating fixed points)

`spm`

Small progress measures

`-sSTRAT`

, `--strategySTRAT`

use substitution strategy STRAT:

`0`

Compute all boolean equations which can be reached from the initial state, without optimization. This is is the most data efficient option per generated equation.

`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 0.

`2`

In addition to 1, also substitute variables that are true or false into an already generated right hand side. This can mean that certain variables become unreachable (e.g. X0 in X0 and 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 footprint.

`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.

`--timings[FILE]`

append timing measurements to FILE. Measurements are written to standard error if no FILE is provided

`--todo-maxNUM`

limit the number of boolean variables that can reside in the todo buffer. If the todo stack is full, a random element in the buffer is removed and the rhs of this variable is set to false (or true if –approximate-false is used). In this case the result true is reliable, and a result false could mean that the formula is valid (or vice versa, if –approximate-false is used). By replacing the variables in the queue at random, the breadth/depth-first structure is mixed up.

`-u`

, `--unused_data`

do not remove unused parts of the data specification.

`-q`

, `--quiet`

do not display warning messages

`-v`

, `--verbose`

display short intermediate messages

`-d`

, `--debug`

display detailed intermediate messages

`--log-levelLEVEL`

display intermediate messages up to and including level

`-h`

, `--help`

display help information

`--version`

display version information

Jan Friso Groote