pbes2bes
Generation of a BES
A BES is generated as follows. First the initial instantiated variable is
considered. The instantiated right hand side for this variable is calculated,
where all expressions without PBES variables are eliminated. Expressions are
reduced to true
or false
and quantifiers are eliminated by
enumerating its elements. As an example consider the PBES (where we use natural
numbers as parameters, but these could be different of course).
pbes mu X(n:Nat)=(n<5)||(forall m:Nat.(m<=n+1) => X(m));
init X(0);
The initial instantiated variable is X(0)
. The right hand side belonging to
X(0)
is
(0<5)||(forall m:Nat.(m<=0+1) => X(m))
which using rewriting reduces to:
(forall m:Nat.(m<=1) => X(m))
The variable m
can either be 0
or 1
. Using that natural numbers are
defined by constructors, a technique called narrowing is used, using which it is
calculated that 0
and 1
are the only useful values for m
.
The expression reduces to:
X(0) && X(1)
So, the first boolean equation that results is
mu X(0)=X(0) && X(1)
The next step is to calculate the equation for X(1)
.
Strategies
There are different strategies to generate the equations.
0
In strategy 0, all equations are generated in a breadth first search. The equations generated in the order the instantiated variables are encountered.
1
In strategy 1, a small improvement is made. If an equation of the form
nu X(17)=(X(10) && X(18)) || X(19)is encountered and the right hand side for
X(10)
isfalse
, then by substitutingfalse
forX(10)
the equation reduces tonu X(17)=X(19)Note
The instantiated variable
X(18)
disappears. It can be thatX(18)
does not have to be investigated at all, saving work compared to strategy 0.
2
The idea of substituting
true
andfalse
and avoiding unnecessary work is taken one step further in strategy 2. Here, whenever a right hand side of an instantiated bes variable istrue
orfalse
, this value is substituted for the instantiated variable every where. The advantage of strategy 2 is that when the validity of a modal formula can be detected by only investigating parts of the state space, this is detected. The costs of strategy 2 is a higher memory footprint than for strategy 0 and 1. Consider the following partially generated BES from some PBES, which typically is the result of a deadlock check on a transition system with a deadlock.nu X(0)=X(1) && X(2) && X(3) nu X(1)=X(4) && X(5) nu X(2)=X(6) nu X(3)=falseWith strategy 2, the value for
X(3)` will be substituted. The result is that ``X(0)
becomesfalse
. Furthermore, the instantiated variablesX(1)
andX(2)
cannot be reached and have become superfluous. Using strategy 2, a garbage collection algorithm prevents such variables from being investigated.
3
Strategy 3 is very comparable to strategy 2, except that when a dependency loop of instantiated variables is detected, it attempts to set all the variables in the loop to
true
in case the fixpoint symbol is a nu, orfalse
if it is a mu. For examplenu X(38)=X(39) nu X(39)=X(38)it can set both
X(38)
andX(39)
totrue
. Moreover, following strategy 2, it can subsequently substitutetrue
forX(38)
andX(39)
in the generated equations.
- orphan:
Usage
pbes2bes [OPTION]... [INFILE [OUTFILE]]
Description
Reads the PBES from INFILE and writes an equivalent BES to OUTFILE. If INFILE is not present, stdin is used. If OUTFILE is not present, stdout is used.
Command line options
-eLEVEL
, --erase=LEVEL
use remove level LEVEL to remove bes variables
none
never remove a generated bes variable and its equation. This can lead to excessive memory usage.
some
remove generated bes variables that do not occur anymore in the generated BES, except if the right hand side of its equation is true or false. The rhss of removed variables must have to be recalculated, when this bes variable is encountered again.
all
remove the equation for bes variables that do not occur anymore in generated boolean equation system. This is quite memory efficient, but it can be very time consuming as the rhss of removed bes variables may have to be recalculated quite often.
-iFORMAT
, --in=FORMAT
use input format 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 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
-zSEARCH
, --search=SEARCH
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 at a larger depth.
b
Shorthand for breadth-first.
d
Shorthand for depth-first.
-sSTRAT
, --strategy=STRAT
use substitution strategy STRAT:
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.
--timings[=FILE]
append timing measurements to FILE. Measurements are written to standard error if no FILE is provided
-u
, --unused_data
do not remove unused parts of the data specification
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