pbesinst

Manual page for pbesinst

Usage

pbesinst   [OPTION]... [INFILE [OUTFILE]]

Description

Transforms the PBES from INFILE into an equivalent BES and writes it to OUTFILE. If INFILE is not present, standard input is used. If OUTFILE is not present, standard output is used.The format of OUTFILE is determined by its extension (unless it is specified by an option). The supported formats are:

‘pbes’ for the mCRL2 PBES format, ‘bes’ for the mCRL2 BES format,

Command line options

-iFORMAT , --in=FORMAT

use input format FORMAT:

bes

BES in internal 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

-QNUM , --qlimit=NUM

limit enumeration of quantifiers to NUM iterations. (Default NUM=1000, 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

-zNAME , --search=NAME

search the state space using strategy NAME:

breadth-first

Compute the right hand side of the boolean variables in a first come first served basis. This is comparable with a breadth-first search. This is good for generating counter examples.

depth-first

Compute the right hand side of a boolean variables where the last generated variable is investigated first. This corresponds to a depth-first search. This can substantially outperform breadth-first search when the validity of a formula is determined at a larger depth.

b

Shorthand for breadth-first.

d

Shorthand for depth-first.

-f[PARAMS] , --select[=PARAMS]

select finite parameters that need to be expanded. Examples: –select=X1(b:Bool,c:Bool);X2(b:Bool) or –select=*(*:Bool). Note: this option only has effect when used together with –strategy=finite.

-sNAME , --strategy=NAME

compute the BES using strategy NAME:

lazy

for computing only boolean equations which can be reached from the initial state

alternative-lazy

an alternative version of the lazy strategy that supports more options

finite

for computing all possible boolean equations

--timings[=FILE]

append timing measurements to FILE. Measurements are written to standard error if no FILE is provided

-ONAME , --transformation=NAME

optimize the BES using strategy NAME:

0

Compute all boolean equations which can be reached from the initial state, without optimization. This is is the most data efficient option per generated equation.

1

Optimize by immediately substituting the right hand sides for already investigated variables that are true or false when generating an expression. This is as memory efficient as 0.

2

In addition to 1, also substitute variables that are true or false into an already generated right hand side. This can mean that certain variables become unreachable (e.g. X0 in X0 and X1, when X1 becomes false, assuming X0 does not occur elsewhere. It will be maintained which variables have become unreachable as these do not have to be investigated. Depending on the PBES, this can reduce the size of the generated BES substantially but requires a larger memory footprint.

3

In addition to 2, investigate for generated variables whether they occur on a loop, such that they can be set to true or false, depending on the fixed point symbol. This can increase the time needed to generate an equation substantially.

Standard options

-q , --quiet

do not display warning messages

-v , --verbose

display short intermediate messages

-d , --debug

display detailed intermediate messages

--log-level=LEVEL

display intermediate messages up to and including level

-h , --help

display help information

--version

display version information

--help-all

display help information, including hidden and experimental options

Author

Wieger Wesselink; Alexander van Dam and Tim Willemse