pbesrewr

This tool is can be used to apply one of several rewriters on a parameterised Boolean equation system.

The simplifying rewriter simplifies pbes expressions by applying the rewrite rules for the data types, and by simplifying boolean expressions. It pushes quantifiers inside as much as possible, removes quantifiers over variables that are not used, and applies straightforward boolean simplifications.

The quantifier-all rewriter expands all quantifiers. The pbes:

map  f: Nat -> Bool;
pbes nu Y = forall x: Nat. val(x < 3 => f(x));
init Y;

is rewriten to:

map  f: Nat -> Bool;
pbes nu Y = val(f(0)) && val(f(1)) && val(f(2));
init Y;

In case the rewriter is requested to expand a quantifier over an unbounded domain it will not terminate. The quantifier-finite rewriter only expands variables over data types that are guaranteed to be finite. If applied to the example above where the quantifier ranges over natural numbers, it does not touch it there are an infinite number of natural numbers.

The quantifier one point rewriter tries to eliminate quantifiers if it can determine that they range over only one element. This works independently of the domain. Contrary to the quantifier-all and quantifier-finite rewriters, the bound variable can be equal to a symbolic value:

map  f:Nat->Bool;
     N:Nat;
pbes nu Y = forall x:Nat.(val(x==N => f(x)));
init Y;

rewrites to:

map  f: Nat -> Bool;
     N: Nat;
pbes nu Y = val(f(N));
init Y;

The quantifier-one-point rewriter works on both universal and existential quantifiers. It uses equalities (==) and inequallities (!=) to determine to which the bound variable is equal.

The quantifiers-inside rewriter tries to push quantifiers as deeply as possible inside a formula. This is sometimes useful before applying the quantifier-one-point rewriter. It is also useful before applying a quantifier-all or quantifier-finite as it can avoid many copies of the same expression the the expanded pbesses.

The pfnf rewriter transforms the pbes to Predicate Formula Normal Form. In this form all quantifiers are moved to the front of each pbes equation. The right hand side is transformed into a big conjunction over disjunctions of pbes variables.

Specifications of the rewriters can be found in the developers documenation in the document about PBES rewriters.

Usage

pbesrewr   [OPTION]... [INFILE [OUTFILE]]

Description

Rewrite the PBES in INFILE, remove quantified variables and write the resulting PBES to OUTFILE. If INFILE is not present, stdin is used. If OUTFILE is not present, stdout is used.

Command line options

-iFORMAT , --in=FORMAT

use input format FORMAT:

pbes

PBES in internal format

pgsolver

BES in PGSolver format

text

PBES in textual (mCRL2) format

-oFORMAT , --out=FORMAT

use output format FORMAT:

bes

BES in internal format

pbes

PBES in internal format

pgsolver

BES in PGSolver format

text

PBES in textual (mCRL2) format

-pNAME , --pbes-rewriter=NAME

use pbes rewrite strategy NAME:

simplify

for simplification

quantifier-all

for eliminating all quantifiers

quantifier-finite

for eliminating finite quantifier variables

quantifier-inside

for pushing quantifiers inside

quantifier-one-point

for one point rule quantifier elimination

pfnf

for rewriting into PFNF normal form

ppg

for rewriting into Parameterised Parity Game form

srf

for rewriting into SRF normal form

pre-srf

for rewriting into pre-SRF normal form

prune-dataspec

for removing unused data equations and mappings

bqnf-quantifier

for rewriting quantifiers over conjuncts to conjuncts of quantifiers (experimental)

remove-cex-variables

for removing counterexample variables from the right-hand side of each equation, i.e., obtaining the core of a pbes

-QNUM , --qlimit=NUM

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

-rNAME , --rewriter=NAME

use rewrite strategy NAME:

jitty

jitty rewriting

jittyc

compiled jitty rewriting

jittyp

jitty rewriting with prover

--srf-split-conditions

split disjunctive SRF conditions

--srf-total

make the SRF PBES total

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

Jan Friso Groote and Wieger Wesselink