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.
Manual page for bessolve¶
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:
besBES in internal format
pbesPBES in internal format
pgsolverBES in PGSolver format
textPBES 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:
spmSmall progress measures
gaussGauss elimination (inefficient; plain implementation)
lfLocal 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
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
Author¶
Jeroen Keiren
