pbessolve can solve a PBES. The solution is printed as
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
<<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
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
The interface of pbessolve is not stable yet. In particular the strategies that are available through the option -s are subject to change.
pbessolve [OPTION]... [INFILE]
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
The file to which the evidence is written. If not set, a default name will be chosen.
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.
use input format FORMAT:
PBES in internal format
Prune the todo list periodically.
limit enumeration of quantifiers to NUM iterations. (Default NUM=1000, NUM=0 for unlimited).
use rewrite strategy NAME:
compiled jitty rewriting
jitty rewriting with prover
Use search strategy NAME:
Leads to smaller counter examples
Use solve strategy NAME. Strategies 1-4 periodically apply on-the-fly solving, which may lead to early termination.
No on-the-fly solving is applied
Propagate solved equations using an attractor.
Detect winning loops.
Solve subgames using a fatal attractor.
Solve subgames using the solver.
run with NUM threads (default=1). With multiple threads the stack size on a Mac is limited which can lead to bus errors.
append timing measurements to FILE. Measurements are written to standard error if no FILE is provided
do not display warning messages
display short intermediate messages
display detailed intermediate messages
display intermediate messages up to and including level
display help information
display version information
display help information, including hidden and experimental options