pbesstategraph

This tool performs a dead variable analysis on parameterised Boolean equation systems. Dead variables are reset to a constant. The analysis performed in this tool is generally more powerful than the one performed by pbesparelm, but it is also more resource intensive.

Example:

\[\begin{split}\begin{array}{l} \nu X(i,j,k,l{:}\mathbb{N}) = (i \neq 1 \lor j \neq 1 \lor X(2,j,k,l+1)) \land \forall m{:}\mathbb{N} . Z(i,2,m+k,k)\\ \mu Y(i,j,k,l{:}\mathbb{N}) = k = 1 \lor (i = 2 \land X(1,j,k,l))\\ \nu Z(i,j,k,l{:}\mathbb{N}) = (k < 10 \lor j = 2) \land (j \neq 2 \lor Y(1,1,l,1)) \land Y(2,2,1,l)\\ ~\\ \mathbf{init}\ X(1,1,1,1) \end{array}\end{split}\]

Instantiation of this PBES using tools such as pbes2bool or pbessolve does not terminate. Also, pbesparelm is only able to remove parameter \(l\) from equations \(X\) and \(Y\), and parameter \(i\) from \(Z\). The presence of the predicate variable instantiations \(X(2,j,k,l+1)\) and \(Z(i,2,m+k,k)\) in \(X\)’s equation means the solution to \(X(1,1,1,1)\) depends on the solutions to \(X(2,1,1,2)\) and \(X(1,2,v+1,1)\) for all values \(v\), so instantiation will not terminate (not even after applying pbesparelm, since parameter \(k\) in the equation for \(Z\) was not removed).

The dead variable analysis will (among others) observe that the third parameter of \(Z\) does not affect the solution when \(j = 2\). The method will observe this, and replace \(Z(i,2,m+k,k)\) by, for example, \(Z(i,2,1,k)\).

The resulting PBES will be:

\[\begin{split}\begin{array}{l} \nu X(i,j,k,l{:}\mathbb{N}) = (i \neq 1 \lor j \neq 1 \lor X(2,j,k,1)) \land \forall m{:}\mathbb{N} . Z(0,2,0,k)\\ \mu Y(i,j,k,l{:}\mathbb{N}) = k = 1 \lor (i = 2 \land X(1,j,k,1))\\ \nu Z(i,j,k,l{:}\mathbb{N}) = (k < 10 \lor j = 2) \land (j \neq 2 \lor Y(1,1,l,0)) \land Y(2,2,1,0)\\ ~\\ \mathbf{init}\ X(1,1,1,1) \end{array}\end{split}\]

To perform the dead variable analysis, the algorithm computes a set of control flow variables. By default, local control flow graphs are constructed in order to avoid a combinatorial explosion of the control flow graph. The option -g/–use-global-variant uses a global control flow graph instead. The latter option may be able to detect more dead variables, but may use (much) more memory.

The algorithm underlying the tool, including the detection of control flow variables and the construction of local and global control flow graphs, is described in detail in [KWW14].

Manual page for pbesstategraph

Usage

pbesstategraph   [OPTION]... [INFILE [OUTFILE]]

Description

Reads a file containing a PBES, and reduces it based on an analysis of control flow parameters.If OUTFILE is not present, standard output is used. If INFILE is not present, standard input is used.

Command line options

-iFORMAT , --in=FORMAT

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

-m[NAME] , --marking-algorithm[=NAME]

specifies the algorithm that is used for the marking computation 0 (default), 1 or 2. In certain cases this choice can have a significant impact on the performance.

-oFORMAT , --out=FORMAT

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 , --qlimit=NUM

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

-rNAME , --rewriter=NAME

use rewrite strategy NAME:

jitty

jitty rewriting

jittyc

compiled jitty rewriting

jittyp

jitty rewriting with prover

--timings[=FILE]

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

-g , --use-global-variant

use the global variant of the algorithm

Standard options

-q , --quiet

do not display warning messages

-v , --verbose

display short intermediate messages

-d , --debug

display detailed intermediate messages

--log-level=LEVEL

display intermediate messages up to and including level

-h , --help

display help information

--version

display version information

Author

Wieger Wesselink; Jeroen Keiren