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.

There are two rewriters. The default simplifying rewriter simplifies the above mentioned expressions by applying the rewrite rules in the specification together with the rewrite rules for the built-in data types.

The quantifier-one-point rewriter eliminates variables that are bound in quantifiers if the values of these variables can be determined from the expression. Two examples:

exists x:Nat.(x==3 && f(x))      ==>        f(3)
forall x:Nat.(x!=3 || f(x))      ==>        f(3)

The elimination of quantifiers is generally very helpful. In solving pbesses or generating state spaces it helps to avoid enumerating these quantifiers. Symbolic manipulation often becomes much easier if quantifiers are removed.

A specification of the one point rule rewriter can be found in the developers documentation in the PBES rewriters document.

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-rewriter=NAME

use lps rewrite strategy NAME:

simplify

for simplification

quantifier-one-point

for one point rule quantifier elimination

condition-one-point

simplify summands using equalities appearing in condition

-QNUM , --qlimit=NUM

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

-rNAME , --rewriter=NAME

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-level=LEVEL

display intermediate messages up to and including level

-h , --help

display help information

--version

display version information

--help-all

display help information, including hidden and experimental options

Author

Wieger Wesselink and Muck van Weerdenburg