presinst

orphan:


Usage

presinst   [OPTION]... [INFILE [OUTFILE]]

Description

Transforms the PRES from INFILE into an equivalent BES and writes it to OUTFILE. If INFILE is not present, standard input is used. If OUTFILE is not present, standard output is used.The format of OUTFILE is determined by its extension (unless it is specified by an option). The supported formats are:

‘pres’ for the mCRL2 PRES format, ‘res’ for the mCRL2 BES format,

Command line options

-iFORMAT , --in=FORMAT

use input format FORMAT:

pres

PRES in internal format

text

PRES in textual (mCRL2) format

-oFORMAT , --out=FORMAT

use output format FORMAT:

pres

PRES in internal format

text

PRES in textual (mCRL2) format

-QNUM , --qlimit=NUM

limit enumeration of universal and existential quantifiers in data expressions to NUM iterations (default NUM=10, NUM=0 for unlimited).

-e , --remove-equations

remove redundant equations

-rNAME , --rewriter=NAME

use rewrite strategy NAME:

jitty

jitty rewriting

jittyc

compiled jitty rewriting

jittyp

jitty rewriting with prover

-f[PARAMS] , --select[=PARAMS]

select finite parameters that need to be expanded. Examples: –select=X1(b:Bool,c:Bool);X2(b:Bool) or –select=*(*:Bool). Note: this option only has effect when used together with –strategy=finite.

-sNAME , --strategy=NAME

compute the BES using strategy NAME:

lazy

for computing only boolean equations which can be reached from the initial state

finite

for computing all possible boolean equations

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

Wieger Wesselink; Alexander van Dam and Tim Willemse