lts2pres

orphan:


Usage

lts2pres   [OPTION]... [INFILE [OUTFILE]]

Description

Translates an LTS in INFILE and writes the resulting PRES to OUTFILE. If OUTFILE is not present, standard output is used. If INFILE is not present, standard input is used.

Command line options

-DFILE , --data=FILE

use FILE as the data and action specification. FILE must be a .mcrl2 file which does not contain an init clause.

-fFILE , --formula=FILE

use the state formula from FILE

-lFILE , --lps=FILE

use FILE for the data and action specification. FILE must be a .lps file.

-mFILE , --mcrl2=FILE

use FILE as the data and action specification for the LTS. FILE must be a .mcrl2 file.

-oFORMAT , --out=FORMAT

use output format FORMAT:

pres

PRES in internal format

text

PRES in textual (mCRL2) format

-p , --preprocess-modal-operators

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

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