pbeschain

This tool is aimed at reducing parameterised Boolean equation systems by selectively ‘unfolding’ specific predicate variable instances if its unfolding contains at most one predicate variable instance.

Usage

pbeschain   [OPTION]... [INFILE [OUTFILE]]

Description

Reads a file containing a PBES. If OUTFILE is not present, standard output is used. If INFILE is not present, standard input is used.

Command line options

--avoid-alternating

Do not chain if the unfolded formula contains a PVI with a different name than the current equation. So X(a) -> Y(b) is not allowed.

-u , --count-unique-pvi

An unfolding is considered less complex if the number of unique predicate variable instances is no more than one.

-f , --fill-pvi

Use the guard of a pvi to fill the pvi with concrete values.

-iFORMAT , --in=FORMAT

use input format FORMAT:

pbes

PBES in internal format

pgsolver

BES in PGSolver format

text

PBES in textual (mCRL2) format

-m[DEPTH] , --max-depth[=DEPTH]

The maximum depth a single predicate variable instances gets unfolded. Default is 12.

-s , --no-back-substitution

Do not substitute the solution to an equation backwards if the number of predicate variable instances in the equation is zero. In some cases, this makes solving the equation faster. However, less paths can be reduced.

--no-remove-equation

Do not remove an equation after its solution has been substituted backwards.

-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

--pvi-pp-factor[=FACTOR]

Set a factor of the maximum size the chained predicate formula should be after chaining compared to the size of the original PVI. 0 means no limit.

-QNUM , --qlimit=NUM

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

--quantifier-free

Do not chain if the unfolded formula contains any quantifier.

--rewrite-only-substitution

Do not use rewriter for any intermediate rewriting, only when substituting right-hand sides.

-rNAME , --rewriter=NAME

use rewrite strategy NAME:

jitty

jitty rewriting

jittyc

compiled jitty rewriting

jittyp

jitty rewriting with prover

--srf-factor[=FACTOR]

Set a factor of the maximum size the chained equation in SRF should be after chaining compared to the size of the original equation. 0 means no limit. Default is 0.

-t[SECONDS] , --timeout[=SECONDS]

Set a timeout in seconds for the substitution process per equation. 0 means no timeout.

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

Jore Booy