# pbesrewr

This tool is can be used to apply one of several rewriters on a parameterised Boolean equation system.

The simplifying rewriter simplifies pbes expressions by applying the rewrite rules for the data types, and by simplifying boolean expressions. It pushes quantifiers inside as much as possible, removes quantifiers over variables that are not used, and applies straightforward boolean simplifications.

The quantifier-all rewriter expands all quantifiers. The pbes:

```map  f: Nat -> Bool;
pbes nu Y = forall x: Nat. val(x < 3 => f(x));
init Y;
```

is rewriten to:

```map  f: Nat -> Bool;
pbes nu Y = val(f(0)) && val(f(1)) && val(f(2));
init Y;
```

In case the rewriter is requested to expand a quantifier over an unbounded domain it will not terminate. The quantifier-finite rewriter only expands variables over data types that are guaranteed to be finite. If applied to the example above where the quantifier ranges over natural numbers, it does not touch it there are an infinite number of natural numbers.

The quantifier one point rewriter tries to eliminate quantifiers if it can determine that they range over only one element. This works independently of the domain. Contrary to the quantifier-all and quantifier-finite rewriters, the bound variable can be equal to a symbolic value:

```map  f:Nat->Bool;
N:Nat;
pbes nu Y = forall x:Nat.(val(x==N => f(x)));
init Y;
```

rewrites to:

```map  f: Nat -> Bool;
N: Nat;
pbes nu Y = val(f(N));
init Y;
```

The quantifier-one-point rewriter works on both universal and existential quantifiers. It uses equalities (==) and inequallities (!=) to determine to which the bound variable is equal.

The quantifiers-inside rewriter tries to push quantifiers as deeply as possible inside a formula. This is sometimes useful before applying the quantifier-one-point rewriter. It is also useful before applying a quantifier-all or quantifier-finite as it can avoid many copies of the same expression the the expanded pbesses.

The pfnf rewriter transforms the pbes to Predicate Formula Normal Form. In this form all quantifiers are moved to the front of each pbes equation. The right hand side is transformed into a big conjunction over disjunctions of pbes variables.

Specifications of the rewriters can be found in the developers documenation in the document about PBES rewriters.

orphan:

## Usage

```pbesrewr   [OPTION]... [INFILE [OUTFILE]]
```

## Description

Rewrite the PBES in INFILE, remove quantified variables and write the resulting PBES to OUTFILE. If INFILE is not present, stdin is used. If OUTFILE is not present, stdout 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

`-pNAME` , `--pbes-rewriter=NAME`

use pbes rewrite strategy NAME:

`simplify`

for simplification

`quantifier-all`

for eliminating all quantifiers

`quantifier-finite`

for eliminating finite quantifier variables

`quantifier-inside`

for pushing quantifiers inside

`quantifier-one-point`

for one point rule quantifier elimination

`pfnf`

for rewriting into PFNF normal form

`ppg`

for rewriting into Parameterised Parity Game form

`bqnf-quantifier`

for rewriting quantifiers over conjuncts to conjuncts of quantifiers (experimental)

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

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

Jan Friso Groote and Wieger Wesselink