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

orphan:

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:

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 universal and existential quantifiers in data expressions to NUM iterations (default NUM=10, 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 log messages

-d , --debug

display detailed log messages

--log-level=LEVEL

display log messages up to and including level; either warn, verbose, debug or trace

-h , --help

display help information

--version

display version information

--help-all

display help information, including hidden and experimental options

Author

Wieger Wesselink; Jeroen Keiren