bessolve can be used to solve a BES. The solution is printed as
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 [OPTION]... [INFILE]
Solve the BES in INFILE. If INFILE is not present, stdin is used.
Command line options
use input format FORMAT:
PBES in internal format
BES in PGSolver format
PBES in textual (mCRL2) format
solve the BES using the specified STRATEGY:
Small progress measures
Gauss elimination (inefficient; plain implementation)
append timing measurements to FILE. Measurements are written to standard error if no FILE is provided
do not display warning messages
display short intermediate messages
display detailed intermediate messages
display intermediate messages up to and including level
display help information
display version information
display help information, including hidden and experimental options