Rewrite the following data expressions of and LPS:
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%.
lpsrewr [OPTION]... [INFILE [OUTFILE]]
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
-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
-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
Wieger Wesselink and Muck van Weerdenburg