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

.

There are different strategies to generate the equations.

`0`

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

`1`

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 substituting`false`

for`X(10)`

the equation reduces tonu X(17)=X(19)Note

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.

`2`

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)=falseWith 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.

`3`

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

```
pbes2bes [OPTION]... [INFILE [OUTFILE]]
```

Reads the PBES from INFILE and writes an equivalent BES to OUTFILE. If INFILE is not present, stdin is used. If OUTFILE is not present, stdout is used.

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

`-oFORMAT`

, `--outFORMAT`

use output 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.

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

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