pbessolve

The tool pbessolve can solve a PBES. The solution is printed as true or false on the command line output. If the property encoded in the PBES holds, in addition a witness can be constructed, and if the property does not hold a counter example can be constructed. We refer to the witness or counter example as the evidence of a property.

If the PBES was constructed via lps2pbes, then the evidence is an LPS that is a submodel of the LPS that was passed to lps2pbes. If the PBES was constructed via lts2pbes, then the evidence is an LTS that is a submodel of the LTS that was passed to lts2pbes. The evidence is written to a file named <<pbesfile>>.evidence.lps or <<pbesfile>>.evidence.lts. A different name can be specified using the command line option --evidence-file.

A counter example for the “infinitely often enabled then infinitely often taken” property of the ABP protocol can be generated as follows:

mcrl22lps abp.mcrl2 abp.lps
lps2pbes -v -c -f infinitely_often_enabled_then_infinitely_often_taken.mcf abp.lps abp.pbes
pbessolve -v --file=abp.lps abp.pbes
lps2lts abp.pbes.evidence.lps abp.pbes.evidence.lts
ltsgraph abp.pbes.evidence.lts

Note that lps2pbes is called with the option -c to include counter example information in the generated PBES. Also note that the specification abp.lps that was used to create the PBES is passed as an argument to pbessolve with the option --file. It is needed to construct the counter example.

Similarly it can be done starting from an LTS instead of an LPS:

mcrl22lps abp.mcrl2 abp.lps
lps2lts abp.lps abp.lts
lts2pbes -v -c -f infinitely_often_enabled_then_infinitely_often_taken.mcf abp.lts abp.pbes
pbessolve -v --file=abp.lts abp.pbes
ltsgraph abp.pbes.evidence.lts
../../_images/infinitely_often_enabled_then_infinitely_often_taken.png

Counter example for the property “infinitely often enabled then infinitely often taken”.

Note

The interface of pbessolve is not stable yet. In particular the strategies that are available through the option -s are subject to change.

Manual page for pbessolve

Usage

pbessolve   [OPTION]... [INFILE]

Description

Solves (P)BES from INFILE. If INFILE is not present, stdin is used. The PBES is first instantiated into a parity game, which is then solved using Zielonka’s algorithm. It supports the generation of a witness or counter example for the property encoded by the PBES.

Command line options

--evidence-fileNAME

The file to which the evidence is written. If not set, a default name will be chosen.

-fNAME , --fileNAME

The file containing the LPS or LTS that was used to generate the PBES using lps2pbes -c. If this option is set, a counter example or witness for the encoded property will be generated. The extension of the file should be .lps in case of an LPS file, in all other cases it is assumed to be an LTS.

-iFORMAT , --inFORMAT

use input format FORMAT:

pbes

PBES in internal format

-QNUM , --qlimitNUM

limit enumeration of quantifiers to NUM variables. (Default NUM=1000, NUM=0 for unlimited).

-rNAME , --rewriterNAME

use rewrite strategy NAME:

jitty

jitty rewriting

jittyc

compiled jitty rewriting

jittyp

jitty rewriting with prover

-zSEARCH , --searchSEARCH

use search strategy SEARCH:

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 after a larger depths.

-sSTRATEGY , --strategySTRATEGY

use strategy STRATEGY

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

In addition to 0, remove self loops.

2

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.

3

In addition to 2, 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.

4

In addition to 3, 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. N.B. This optimization may cause stack overflow issues.

5

A generalization of strategy 4, where a so-calledfatal attractor is applied.

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

-d , --debug

display detailed intermediate messages

--log-levelLEVEL

display intermediate messages up to and including level

-h , --help

display help information

--version

display version information

Author

Wieger Wesselink