lpsrewr

Rewrite the following data expressions of and LPS:

• conditions, action parameters, time expressions and next states of LPS summands
• process parameters of the initial state
• conditions and right-hand sides of data equations

Rewriting LPS summands and the initial state is done to simplify these parts of the LPS. Rewriting data equations is done to speed up state space generation. In most cases, this results in a performance gain of at most 5%.

Manual page for lpsrewr

Usage

lpsrewr   [OPTION]... [INFILE [OUTFILE]]

Description

Rewrite data expressions of the LPS in INFILE and save the result to OUTFILE.If OUTFILE is not present, standard output is used. If INFILE is not present,standard input is used

Command line options

-pNAME , --lps-rewriterNAME

use lps rewrite strategy NAME:

simplify

for simplification

quantifier-one-point

for one point rule quantifier elimination

-QNUM , --qlimitNUM

limit enumeration of quantifiers to NUM variables. (Default NUM=1000, NUM=0 for unlimited).

-rNAME , --rewriterNAME

use rewrite strategy NAME:

jitty

jitty rewriting

jittyc

compiled jitty rewriting

jittyp

jitty rewriting with prover

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

-d , --debug

display detailed intermediate messages

--log-levelLEVEL

display intermediate messages up to and including level

-h , --help

display help information

--version

display version information

Author

Wieger Wesselink and Muck van Weerdenburg