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

Author

Jeroen Keiren