bessolve
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:
- Gauss elimination
This is a straightforward implementation of the Gauss elimination technique. In general it is very inefficient.
- Local fixpoints
This is a more advanced form of Gauss elimination. It is efficient if the BES contains no alternating fixed points. For this algorithm a justification for the solution can be printed.
- Small progress measures
This is an implementation of the small progress measures algorithm by Marcin Jurdzinski.
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
.
- orphan:
Usage
bessolve [OPTION]... [INFILE]
Description
Solve the BES in INFILE. If INFILE is not present, stdin 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
-sSTRATEGY
, --strategy=STRATEGY
solve the BES using the specified STRATEGY:
spm
Small progress measures
gauss
Gauss elimination (inefficient; plain implementation)
--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 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