User manual/lpsrewr

From MCRL2

User manual

Tool manual pages chi2mcrl2 diagraphica formcheck grapemcrl2 lps2lts lps2pbes lps2torx lpsactionrename lpsbinary lpsbisim2pbes lpsconfcheck lpsconstelm lpsinfo lpsinvelm lpsparelm lpsparunfold lpspp lpsrealelm lpsrewr lpssim lpssumelm lpssuminst lpsuntime lpsxsim lts2lps ltscompare ltsconvert ltsgraph ltsinfo ltsmin ltsview lysa2mcrl2 mcrl22lps mcrl2-gui mcrl2i pbesinst pbes2bool pbesconstelm pbesinfo pbesparelm pbespareqelm pbespgsolve pbespp pbesrewr pnml2mcrl2 squadt tbf2lps tracepp txt2lps txt2pbes

Contents

Contents 1 Synopsis 2 Short Description 3 Options 4 Author 5 Reporting bugs

Synopsis

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

Short 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

The following data expressions are rewritten:

• 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%.

Options

OPTION can be any of the following:

-rNAME, --rewriter=NAME

use rewrite strategy NAME:

 'jitty' for jitty rewriting (default),
 'jittyp' for jitty rewriting with prover,
 'jittyc' for compiled jitty rewriting,
 'inner' for innermost rewriting,
 'innerp' for innermost rewriting with prover, or
 'innerc' for compiled innermost rewriting

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

-h, --help

display help information

--version

display version information

Author

Implemented by Wieger Wesselink and Muck van Weerdenburg.

Reporting bugs

Report bugs at [1].

---

lpsrealelm

lpssim