besconvert
Convert Boolean equation systems (BESs) from and to different formats. Optionally, a minimisation method can be selected that is applied on the input.
The reductions that can be done are either strong bisimulation reduction or stuttering bisimulation reduction.
Strong bisimulation reduction of BESs is described in [KW11]. Correctness of stuttering equivalence for BESs follows from the corresponding results on parity games in [CKW11]
- orphan:
Usage
besconvert [OPTION]... [INFILE [OUTFILE]]
Description
reduce the (P)BES in INFILE modulo write the result to OUTFILE (as PBES).If INFILE is not present, stdin is used. If OUTFILE is not present, stdout is used.
Command line options
-eNAME
, --equivalence=NAME
generate an equivalent BES, preserving equivalence NAME:’none’ for no reduction (default),’bisim’ for strong bisimulation,’stuttering’ for stuttering equivalence
-iFORMAT
, --in=FORMAT
use input format FORMAT:
pbes
PBES in internal format
pgsolver
BES in PGSolver format
text
PBES in textual (mCRL2) format
-lFILE
, --intermediate=FILE
save the intermediate LTS to FILE
-n
, --noreduction
do not perform the reduction, only store the intermediate LTS
-oFORMAT
, --out=FORMAT
use output format FORMAT:
bes
BES in internal format
pbes
PBES in internal format
pgsolver
BES in PGSolver format
text
PBES in textual (mCRL2) format
--timings[=FILE]
append timing measurements to FILE. Measurements are written to standard error if no FILE is provided
-tTRANSLATION
, --translation=TRANSLATION
translate to intermediate LTS using TRANSLATION:’deadlock’ for an additional deadlock state recording labels, ‘selfloop’ for a self-loop recording the information in each state, ‘successor’ for an edge with the label of the current state to each successor state (may only be used with –equivalence=bisim)
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