lps2pres

orphan:


Usage

lps2pres   [OPTION]... --formula=FILE [INFILE [OUTFILE]]

Description

Convert the state formula in FILE and the LPS in INFILE to a parameterised real equation system (PRES) and save it to OUTFILE. If OUTFILE is not present, stdout is used. If INFILE is not present, stdin is used.

Command line options

-fFILE , --formula=FILE

use the state formula from FILE

-oFORMAT , --out=FORMAT

use output format FORMAT:

pres

PRES in internal format

text

PRES in textual (mCRL2) format

-m , --preprocess-modal-operators

insert dummy fixpoints in modal operators, which may lead to smaller PRESs

-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 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

Jan Friso Groote. Based on the tool lps2pbes