This tool is intended to solve parameterised boolean equation systems (PBES)
using a parity game solver. This is achieved by instantiating the PBES to a
boolean equation system. The resulting BES is equivalent to some parity games
such that a boolean equation is true if and only if the corresponding vertex of
the parity game is won by player even. A parity game solver can be used to
obtain the winning players for all vertices of that parity game. This also
determines the solution for the initial equation of the (P)BES. That solution
is then printed to standard output. The tool also accepts a BES or a parity
game in PGSolver format directly.

## Manual page for pbespgsolve

### Usage

pbespgsolve [OPTION]... [INFILE]

### Description

Reads a file containing a (P)BES or a max-parity game in PGSolver format. A PBES input is first instantiated to a BES; from which a parity game can be obtained. A parity game solver is then used to solve this parity game. The solution of the first vertex, which also defines the solution of initial equation of the (P)BES, is printed to standard output. When INFILE is not present, standard input is used.

### Command line options

`-C`

, `--cycle`

Eliminate cycles

`-iFORMAT`

, `--inFORMAT`

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

`-L`

, `--loop`

Eliminate self-loops

`-g`

, `--onlygenerate`

Only generate the BES without solving

`-QNUM`

, `--qlimitNUM`

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

`-rNAME`

, `--rewriterNAME`

use rewrite strategy NAME:

`jitty`

jitty rewriting

`jittyc`

compiled jitty rewriting

`jittyp`

jitty rewriting with prover

`-c`

, `--scc`

Use scc decomposition

`-sNAME`

, `--solver-typeNAME`

Use the solver type NAME:

`spm`

Small progress measures

`altspm`

Alternative implementation of small progress measures

`recursive`

Recursive algorithm

`prioprom`

Priority promotion (experimental)

`--timings[FILE]`

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

`-e`

, `--verify`

Verify the solution

#### Standard options

`-q`

, `--quiet`

do not display warning messages

`-v`

, `--verbose`

display short intermediate messages

`-d`

, `--debug`

display detailed intermediate messages

`--log-levelLEVEL`

display intermediate messages up to and including level

`-h`

, `--help`

display help information

`--version`

display version information

### Author

Maks Verver and Wieger Wesselink; Michael Weber