pbespareqelm

This tool aims to detect invariants [OW10] of a very specific form in PBESs. The invariants detected by the tool are identities between parameters of predicate variables. Pairs of parameters that are always equal are discovered, and one of these parameters is eliminated.

Consider, for instance, the following example (The Mutual Exclusion Problem (2) taken from [OW10]).

\begin{array}{l} \nu X(n_r,n_w,t,r,w {:} \nat) = (r + w > 0 \implies r \cdot w =0)\\ \qquad \wedge (t \ge 1 \implies X(n_r+1,n_w,t-1,r+1,w))\\ \qquad \wedge (n_r > 0 \implies X(n_r-1,n_w,t+1,r-1,w))\\ \qquad \wedge (t \ge N \implies X(n_r,n_w+1,t-N,r,w+1))\\ \qquad \wedge (n_w > 0 \implies X(n_r,n_w-1,t+N,r,w-1)) ~\\ \mathbf{init}\ X(0,0,N,0,0) \end{array}

Observe that with this initial configuration, $n_r = r$ and $n_w = w$ are invariants. The resulting PBES is as follows.

\begin{array}{l} \nu X(n_r,n_w,t {:} \nat) = (nr + nw > 0 \implies nr \cdot nw =0)\\ \qquad \wedge (t \ge 1 \implies X(n_r+1,n_w,t-1))\\ \qquad \wedge (n_r > 0 \implies X(n_r-1,n_w,t+1))\\ \qquad \wedge (t \ge N \implies X(n_r,n_w+1,t-N))\\ \qquad \wedge (n_w > 0 \implies X(n_r,n_w-1,t+N)) ~\\ \mathbf{init}\ X(0,0,N) \end{array}

Usage

pbeseqelm   [OPTION]... [INFILE [OUTFILE]]

Description

Reads a file containing a PBES, and applies the eqelm algorithm to detect equivalence relations between the parameters. If OUTFILE is not present, standard output is used. If INFILE is not present, standard input is used.

Command line options

-I , --ignore-initial-state

ignore the initial state in the computation

-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

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

Wieger Wesselink; Simona Orzan and Tim Willemse