lps2pbes1
Generate a pbes from an lps and a state formula
Usage
lps2pbes [OPTION] ...
--formula=FILE
[INFILE
[OUTFILE]]
Overview
Convert the state formula in FILE and the LPS in INFILE to a parameterised boolean equation system (PBES) and save it to OUTFILE. If OUTFILE is not present, stdout is used. If INFILE is not present, stdin is used.
Options
- OPTION can be any of the following:
-
-fFILE, --formula=FILE -
use the state formula from FILE
-
-oFORMAT, --out=FORMAT -
use output format FORMAT: 'pbes' PBES in internal format 'pbes_text' PBES in internal textual format 'text' PBES in textual (mCRL2) format
-
-s, --structured -
generate equations such that no mixed conjunctions and disjunctions occur
-
-t, --timed -
use the timed version of the algorithm, even for untimed LPS's
-
--timings[=FILE] -
append timing measurements to FILE. Measurements are written to standard error if no FILE is provided
-
-u, --unoptimized -
do not simplify boolean expressions
- 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
Releases
4 releases since Debian 6.0 (Squeeze); the text changed 3 times.
--log-level since Debian 7 (Wheezy);
--out since Debian 8 (Jessie);
--structured since Debian 8 (Jessie);
--timings since Debian 7 (Wheezy);
--unoptimized since Debian 8 (Jessie);
-o since Debian 8 (Jessie);
-s since Debian 8 (Jessie);
-u since Debian 8 (Jessie).
--mcrl2-gui until Debian 6.0 (Squeeze).