pbesconstelm

The purpose of this tool is to eliminate constant parameters from parameterised Boolean equation sytems, in a similar fashion as lpsconstelm.

Example:

\[\begin{split}\begin{array}{l} \nu X(n, m{:}\mathbb{N}) = n \approx m + 2 \land X(n + 1, m) \land Y(0, m)\\ \mu Y(n, m{:}\mathbb{N}) = n \approx 3*m \land Y(n, 2*m)\\ ~\\ \mathbf{init}\ X(4,7) \end{array}\end{split}\]

In this PBES, the parameters \(m\) of \(X\) and \(n\) of \(Y\) will be eliminated. Their constant values are 7 and 0, respectively. The resulting PBES will be:

\[\begin{split}\begin{array}{l} \nu X(n{:}\mathbb{N}) = n \approx 7 + 2 \land X(n + 1) \land Y(7)\\ \mu Y(m{:}\mathbb{N}) = 0 \approx 3*m \land Y(2*m)\\ ~\\ \mathbf{init}\ X(4) \end{array}\end{split}\]

The option -c/–compute-conditions can be used to analyse conditions with the contants that have been found. This can help the algorithm to find more constants. However, this option typically leads to a large increase in the runtime of the tool.

The algorithm underlying the tool is described in detail in [OWW09].

orphan:

Usage

pbesconstelm   [OPTION]... [INFILE [OUTFILE]]

Description

Reads a file containing a PBES, and applies constant parameter elimination to it. If OUTFILE is not present, standard output is used. If INFILE is not present, standard input is used.

Command line options

-a , --check-quantifiers

also analyse which quantified parameters are constant

-c , --compute-conditions

compute propagation conditions

-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

bqnf-quantifier

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

-QNUM , --qlimit=NUM

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

-e , --remove-equations

remove redundant equations

-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; Simon Janssen and Tim Willemse