The tool bessolve
can be used to solve a BES. The solution is printed as true
or false
on the command line output.
Three different solving algorithms have been implemented:
Note that a BES can also be solved by the tool pbessolve
. This tool uses Zielonka’s
algorithm, which often performs better than the ones implemented in bessolve
.
bessolve [OPTION]... [INFILE]
Solve the BES in INFILE. If INFILE is not present, stdin is used.
-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
-j
, --print-justification
print justification for solution. Works only with the local fixpoint strategy.
-sSTRATEGY
, --strategy=STRATEGY
solve the BES using the specified STRATEGY:
spm
Small progress measures
gauss
Gauss elimination (inefficient; plain implementation)
lf
Local fixpoints (advanced form of Gauss elimination, especially effective without alternating fixed points)
--timings[=FILE]
append timing measurements to FILE. Measurements are written to standard error if no FILE is provided
-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
Jeroen Keiren