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.
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 , --in=FORMAT
use input format FORMAT:
pbesPBES in internal format
pgsolverBES in PGSolver format
textPBES in textual (mCRL2) format
-L , --loop
Eliminate self-loops
-g , --onlygenerate
Only generate the BES without solving
-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:
jittyjitty rewriting
jittyccompiled jitty rewriting
jittypjitty rewriting with prover
-c , --scc
Use scc decomposition
-sNAME , --solver-type=NAME
Use the solver type NAME:
spmSmall progress measures
altspmAlternative implementation of small progress measures
recursiveRecursive algorithm
priopromPriority 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 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