pbesparelm

The purpose of this tool is to find those parameters in parameterised Boolean equation sytems that do not affect the solution, and remove those in a similar fashion as lpsparelm.

Example:

\begin{array}{l}
\nu V(n{:}\mathbb{N}, b{:}\mathbb{B}) = (b \Rightarrow V(n + 1, b)) \land W(n, b)\\
\mu W(n{:}\mathbb{N}, b{:}\mathbb{B}) = b \lor (b \land W(n+1, b))\\
~\\
\mathbf{init}\ V(0,\mathit{true})
\end{array}

Instantiation of this PBES using tools such as pbes2bool or pbessolve does not terminate. However, in this PBES, parameter n of both equations is redundant (it does not appear positively in any equation), and can be removed. The resulting PBES will be:

\begin{array}{l}
\nu V(b{:}\mathbb{B}) = (b \Rightarrow V(b)) \land W(b)\\
\mu W(b{:}\mathbb{B}) = b \lor (b \land W(b))\\
~\\
\mathbf{init}\ V(0,\mathit{true})
\end{array}

The algorithm underlying the tool is described in detail in [OWW09].

Usage

pbesparelm   [OPTION]... [INFILE [OUTFILE]]

Description

Reads a file containing a PBES, and applies parameter elimination to it. 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

-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

--timings[=FILE]

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

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; Simon Janssen and Tim Willemse