Here, we list and describe the 15 new examples that we added to the benchmark collection of probabilistic programs. The benchmarks can be downloaded here. To run KoAT on our benchmarks, we suggest to use our web interface.
cfr01.koat
The following example is the while-loop from the paper.
(GOAL EXPECTEDCOMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR X0)
(RULES
l0(X0) -> l1(T) :|: T > 0
l1(X0) -> 0.5:l1(0) :+: 0.5:l1(X0) :|: X0 > 0
)
cfr02.koat
This benchmark corresponds to the leading example from the paper.
(GOAL EXPECTEDCOMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR X0 X1)
(RULES
l0(X0, X1) -> l1(T, X1) :|: T > 0
l1(X0, X1) -> 0.5:l1(0, X1) :+: 0.5:l1(X0, X1) :|: X0 > 0
l1(X0, X1) -> l2(X0, X1 - 1)
l2(X0, X1) -> l1(X0, X1) :|: X0 = 0 && 0 < X1
)
cfr03.koat
This example is an advanced version of the leading example where we extended the third transition by probabilities.
(GOAL EXPECTEDCOMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR X0 X1)
(RULES
l0(X0, X1) -> l1(T, X1) :|: T > 0
l1(X0, X1) -> 0.5:l1(0, X1) :+: 0.5:l1(X0, X1) :|: X0 > 0
l1(X0, X1) -> 0.5:l2(X0, X1 - 1) :+: 0.5:l2(X0, X1)
l2(X0, X1) -> l1(X0, X1) :|: X0 = 0 && 0 < X1
)
cfr04.koat
Either always the third or the fourth general transition is executed in this benchmark. Here, control-flow refinement separates these transitions into two independent components.
(GOAL EXPECTEDCOMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR X0 X1 X2)
(RULES
l0(X0, X1, X2) -> l1(X0, X1, X2)
l1(X0, X1, X2) -> l2(X0, X1, X2) :|: 0 <= X0 && X0 <= X2
l2(X0, X1, X2) -> 0.5:l1(X0 + 1, X1, X2) :+: 0.5:l1(X0, X1, X2) :|: X1 <= 0
l2(X0, X1, X2) -> 0.5:l1(X0 - 1, X1, X2) :+: 0.5:l1(X0, X1, X2) :|: 0 < X1
)
cfr05.koat
In contrast to cfr04.koat, this benchmark consists of a loop which does not admit a linear ranking function.
(GOAL EXPECTEDCOMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR X0 X1 X2)
(RULES
l0(X0, X1, X2) -> l1(X0, X1, X2)
l1(X0, X1, X2) -> l2(X0, X1, X2) :|: 0 < X0 && X0 <= X2
l2(X0, X1, X2) -> l1(3*X0, X1, 2*X2) :|: X1 <= 0
l2(X0, X1, X2) -> 0.5:l1(X0 - 1, X1, X2) :+: 0.5:l1(X0, X1, X2) :|: 0 < X1
)
cfr06.koat
This benchmarks extends cfr05.koat by a consecutive loop (transitions five and six).
However, this consecutive loop can only be executed if the fourth transition is evaluated.
CFR recognizes this and separates transition three from the
transitions four, five, and six.
In particular, we do not have to consider the exponential size bound of X2 when evaluating the third transition.
(GOAL EXPECTEDCOMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR X0 X1 X2)
(RULES
l0(X0, X1, X2) -> l1(X0, X1, X2)
l1(X0, X1, X2) -> l2(X0, X1, X2) :|: 0 < X0 && X0 <= X2
l2(X0, X1, X2) -> l1(3*X0, X1, 2*X2) :|: X1 <= 0
l2(X0, X1, X2) -> 0.5:l1(X0 - 1, X1, X2 + 1) :+: 0.5:l1(X0, X1, X2) :|: 0 < X1
l1(X0, X1, X2) -> l3(X0, X1, X2) :|: 0 < X1 && X0 = 0
l3(X0, X1, X2) -> l3(X0, X1, X2 - 1) :|: 0 < X2
)
cfr07.koat
This benchmark is the tail-recursive version of the McCarthy 91 function (see the C-version in the Termination Problem Data Base (TPDB) here).
(GOAL EXPECTEDCOMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR X0 X1)
(RULES
l0(X0, X1) -> l1(1, X1)
l1(X0, X1) -> l2(X0, X1) :|: X0 > 0
l2(X0, X1) -> l1(X0 - 1, X1 - 10) :|: X1 > 100
l2(X0, X1) -> l1(X0 + 1, X1 + 11) :|: X1 <= 100
)
cfr08.koat
This benchmark extends cfr07.koat by probabilities.
(GOAL EXPECTEDCOMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR X0 X1)
(RULES
l0(X0, X1) -> l1(1, X1)
l1(X0, X1) -> l2(X0, X1) :|: X0 > 0
l2(X0, X1) -> 0.5:l1(X0 - 1, X1 - 10) :+: 0.5:l1(X0,X1) :|: X1 > 100
l2(X0, X1) -> 0.5:l1(X0 + 1, X1 + 11) :+: 0.5:l1(X0,X1) :|: X1 <= 100
)
cfr09.koat
Simplified version of a benchmark from the TPDB.
(GOAL EXPECTEDCOMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR X Y)
(RULES
l0(X, Y) -> l1(X, Y)
l1(X, Y) -> l2(X, Y) :|: X < Y && X > 0
l2(X, Y) -> l1(T, X - 1)
l2(X, Y) -> l1(X - 1, T)
)
cfr10.koat
In this benchmark we extended cfr09.koat by probabilities.
(GOAL EXPECTEDCOMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR X Y)
(RULES
l0(X, Y) -> l1(X, Y)
l1(X, Y) -> l2(X, Y) :|: X < Y && X > 0
l2(X, Y) -> 0.5:l1(T, X - 1) :+: 0.5:l1(T, X)
l2(X, Y) -> 0.5:l1(X - 1, T) :+: 0.5:l1(X, T)
)
cfr11.koat
In this benchmark either X or Y is set to X - 1 with probability ½.
This a probabilistic version of a similar non-probabilistic C-program benchmark from the TPDB.
(GOAL EXPECTEDCOMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR X Y)
(RULES
l0(X, Y) -> l1(X, Y)
l1(X, Y) -> l2(X, Y) :|: X < Y && X > 0
l2(X, Y) -> 0.5:l1(T, X - 1) :+: 0.5:l1(X - 1, T)
)
cfr12.koat
This benchmark is the combination of cfr10.koat and cfr11.koat.
(GOAL EXPECTEDCOMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR X Y)
(RULES
l0(X, Y) -> l1(X, Y)
l1(X, Y) -> l2(X, Y) :|: X < Y && X > 0
l2(X, Y) -> 0.25:l1(T, X - 1) :+: 0.25:l1(X - 1, T) :+: 0.25:l1(T, X) :+: 0.25:l1(X, T)
)
cfr13.koat
Here, both transitions that make up the loop l1 → l1 can only be executed alternatingly.
CFR detects this and allows for the computation of a constant runtime bound.
While the loop is also a TWN loop, this technique alone, i.e., without CFR, only leads to a linear runtime bound.
Thus, the constant runtime bound can only be found by KoAT when TWN is disabled as TWN would report a linear bound and hence lead to termination of the analysis.
(GOAL EXPECTEDCOMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR phase x)
(RULES
l0(phase,x) -> l1(1,x)
l1(phase,x) -> l1(- phase, - x - phase) :|: x <= 10 && phase > 0
l1(phase,x) -> l1(- phase, - x - phase) :|: x <= 10 && phase < 0
)
cfr14.koat
This is a variant of cfr13.koat where the loop is positively almost-surely terminating, i.e., after an finite expected number of steps.
However, in contrast to the previous example, the loop is not certainly terminating.
(GOAL EXPECTEDCOMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR phase x)
(RULES
l0(phase,x) -> l1(1,x)
l1(phase,x) -> 0.5:l1(- phase, - x - phase) :+: 0.5:l1(-phase, - x) :|: x <= 10 && phase > 0
l1(phase,x) -> 0.5:l1(- phase, - x - phase) :+: 0.5:l1(-phase, - x) :|: x <= 10 && phase < 0
)
cfr15.koat
This is a more concise variant of cfr13.koat showcasing the limits of the control-flow refinement.
Here, CFR does not lead to a finite time bound (In fact KoAT is not able to find a finite runtime bound for this example).
The reason is that the abstraction layer proposed by a heuristic is lacking the two crucial comparisons phase > 0 and phase < 0.
Moreover, in contrast to cfr13.koat for which the TWN technique gives rise to a linear (instead of the more precise constant) runtime bound, this technique is not applicable here.
The reason for this is that we consider conjunctive invariants only.
Hence we are missing the crucial information that in l1 we always have phase ≠ 0.
(GOAL EXPECTEDCOMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR phase x)
(RULES
l0(phase,x) -> l1(1,x)
l1(phase,x) -> 0.5:l1(- phase, - x) :+: 0.5:l1(- phase, - x - phase) :|: x <= 10
)