# 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{split}\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}\end{split}$

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{split}\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}\end{split}$

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

orphan:

## 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:

bes

BES in internal 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 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

--help-all

display help information, including hidden and experimental options

## Author

Wieger Wesselink; Simon Janssen and Tim Willemse