pbespgsolve

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