pbespor

This tool transforms a PBES into a BES by means of state-space exploration. However, it attempts to explore only a part of the state space, thus saving time and memory.

This tool is highly experimental, and using it is not recommended.

Usage

pbespor   [OPTION]... [INFILE [OUTFILE]]

Description

Reads a file containing a PBES, and applies partial order reduction to it. If OUTFILE is not present, standard output is used. If INFILE is not present, standard input is used.

Command line options

--full

explore the full state space. No static analysis is performed.

-iFORMAT , --in=FORMAT

use input format FORMAT:

pbes

PBES in internal format

pgsolver

BES in PGSolver format

text

PBES in textual (mCRL2) format

--left

compute the left accordance relation (more expensive, more powerful, static analysis)

--nes

compute the necessary enabling relation (more expensive, more powerful, static analysis)

--no-determinism

do not check whether transitions are deterministic (cheaper, but less powerful, static analysis)

--no-l

do not apply the condition L (might affect correctness)

-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

--triangle

compute the triangle accordance relation (more expensive, more powerful, static analysis)

-s[TIMEOUT] , --use-smt-solver[=TIMEOUT]

Use the SMT solver Z3 (must be in the path). The timeout should be given in milliseconds (0 = no timeout). Very small values may lead to errors.

-w , --weak-conditions

use weak accordance conditions (cheaper, but less exact, static analysis)

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; Thomas Neele and Tim Willemse