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:
pbesPBES in internal format
pgsolverBES in PGSolver format
textPBES in textual (mCRL2) format
-sSTRATEGY , --strategy=STRATEGY
solve the BES using the specified STRATEGY:
spmSmall progress measures
gaussGauss 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 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