Preprocessing

Found invariant X₂ ≤ 3 ∧ X₂ ≤ 3+X₀ ∧ X₀+X₂ ≤ 6 ∧ 1 ≤ X₂ ∧ 1 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ X₀ ≤ 3 ∧ 0 ≤ X₀ for location h

Found invariant X₀ ≤ 3 ∧ 1 ≤ X₀ for location g

Found invariant X₂ ≤ 3 ∧ X₂ ≤ 3+X₁ ∧ X₁+X₂ ≤ 6 ∧ X₂ ≤ 2+X₀ ∧ X₀+X₂ ≤ 6 ∧ 1 ≤ X₂ ∧ 1 ≤ X₁+X₂ ∧ X₁ ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ X₁ ≤ 3 ∧ X₁ ≤ 2+X₀ ∧ X₀+X₁ ≤ 6 ∧ 0 ≤ X₁ ∧ 1 ≤ X₀+X₁ ∧ X₀ ≤ 3+X₁ ∧ X₀ ≤ 3 ∧ 1 ≤ X₀ for location i

Probabilistic Analysis

Probabilistic Program after Preprocessing

Start: f
Program_Vars: X₀, X₁, X₂
Temp_Vars:
Locations: f, g, h, i
Transitions:
g₀:f(X₀,X₁,X₂) → [1/3]:t₁:g(1,X₁,X₂) :+: [1/3]:t₂:g(2,X₁,X₂) :+: [1/3]:t₃:g(3,X₁,X₂) :|:
g₄:g(X₀,X₁,X₂) → t₅:h(X₀,X₁,X₀) :|: X₀ ≤ 3 ∧ 1 ≤ X₀
g₆:h(X₀,X₁,X₂) → t₇:i(X₀,X₂,X₂) :|: 1 ≤ X₀ ∧ X₀+X₂ ≤ 6 ∧ X₂ ≤ 3+X₀ ∧ X₀ ≤ 3 ∧ X₂ ≤ 3 ∧ 1 ≤ X₀+X₂ ∧ 1 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
g₈:i(X₀,X₁,X₂) → t₉:i(X₀,X₁-1,X₂) :|: 1 ≤ X₁ ∧ X₀+X₁ ≤ 6 ∧ X₀+X₂ ≤ 6 ∧ X₁+X₂ ≤ 6 ∧ X₀ ≤ 3 ∧ X₀ ≤ 3+X₁ ∧ X₂ ≤ 3+X₁ ∧ X₁ ≤ 3 ∧ X₂ ≤ 3 ∧ X₁ ≤ 2+X₀ ∧ X₂ ≤ 2+X₀ ∧ 1 ≤ X₀ ∧ 1 ≤ X₀+X₁ ∧ 1 ≤ X₁+X₂ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₁ ∧ X₁ ≤ X₂
g₁₀:i(X₀,X₁,X₂) → t₁₁:h(X₀-1,X₁,X₂) :|: X₁ ≤ 0 ∧ X₀+X₁ ≤ 6 ∧ X₀+X₂ ≤ 6 ∧ X₁+X₂ ≤ 6 ∧ X₀ ≤ 3 ∧ X₀ ≤ 3+X₁ ∧ X₂ ≤ 3+X₁ ∧ X₁ ≤ 3 ∧ X₂ ≤ 3 ∧ X₁ ≤ 2+X₀ ∧ X₂ ≤ 2+X₀ ∧ 1 ≤ X₀ ∧ 1 ≤ X₀+X₁ ∧ 1 ≤ X₁+X₂ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₁ ∧ X₁ ≤ X₂

Run classical analysis on SCC: [f]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:inf {Infinity}
g₀: 3 {O(1)}
g₄: 1 {O(1)}
g₆: inf {Infinity}
g₈: inf {Infinity}
g₁₀: inf {Infinity}

Costbounds

Overall costbound: inf {Infinity}
g₀: inf {Infinity}
g₄: inf {Infinity}
g₆: inf {Infinity}
g₈: inf {Infinity}
g₁₀: inf {Infinity}

Sizebounds

(g₀,g), X₀: 6 {O(1)}
(g₀,g), X₁: 3⋅X₁ {O(n)}
(g₀,g), X₂: 3⋅X₂ {O(n)}

Run probabilistic analysis on SCC: [f]

Run classical analysis on SCC: [g]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:inf {Infinity}
g₀: 3 {O(1)}
g₄: 1 {O(1)}
g₆: inf {Infinity}
g₈: inf {Infinity}
g₁₀: inf {Infinity}

Costbounds

Overall costbound: inf {Infinity}
g₀: inf {Infinity}
g₄: inf {Infinity}
g₆: inf {Infinity}
g₈: inf {Infinity}
g₁₀: inf {Infinity}

Sizebounds

(g₀,g), X₀: 6 {O(1)}
(g₀,g), X₁: X₁ {O(n)}
(g₀,g), X₂: X₂ {O(n)}
(g₄,h), X₀: 3 {O(1)}
(g₄,h), X₁: 3⋅X₁ {O(n)}
(g₄,h), X₂: 3 {O(1)}

Run probabilistic analysis on SCC: [g]

Run classical analysis on SCC: [h; i]

MPRF for transition t₇: h(X₀,X₁,X₂) → i(X₀,X₂,X₂) :|: X₀+X₂ ≤ 6 ∧ X₂ ≤ 3+X₀ ∧ X₀ ≤ 3 ∧ X₂ ≤ 3 ∧ 1 ≤ X₀+X₂ ∧ 1 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₀ of depth 1:

new bound:

4 {O(1)}

MPRF:

• h: [1+X₀]
• i: [X₀]

MPRF for transition t₉: i(X₀,X₁,X₂) → i(X₀,X₁-1,X₂) :|: X₀+X₁ ≤ 6 ∧ X₀+X₂ ≤ 6 ∧ X₁+X₂ ≤ 6 ∧ X₀ ≤ 3 ∧ X₀ ≤ 3+X₁ ∧ X₂ ≤ 3+X₁ ∧ X₁ ≤ 3 ∧ X₂ ≤ 3 ∧ X₁ ≤ 2+X₀ ∧ X₂ ≤ 2+X₀ ∧ 1 ≤ X₀ ∧ 1 ≤ X₀+X₁ ∧ 1 ≤ X₁+X₂ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₁ ∧ X₁ ≤ X₂ ∧ 1 ≤ X₁ of depth 1:

new bound:

12 {O(1)}

MPRF:

• h: [3⋅X₀+X₂]
• i: [3⋅X₀+X₁]

MPRF for transition t₁₁: i(X₀,X₁,X₂) → h(X₀-1,X₁,X₂) :|: X₀+X₁ ≤ 6 ∧ X₀+X₂ ≤ 6 ∧ X₁+X₂ ≤ 6 ∧ X₀ ≤ 3 ∧ X₀ ≤ 3+X₁ ∧ X₂ ≤ 3+X₁ ∧ X₁ ≤ 3 ∧ X₂ ≤ 3 ∧ X₁ ≤ 2+X₀ ∧ X₂ ≤ 2+X₀ ∧ 1 ≤ X₀ ∧ 1 ≤ X₀+X₁ ∧ 1 ≤ X₁+X₂ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₁ ∧ X₁ ≤ X₂ ∧ X₁ ≤ 0 of depth 1:

new bound:

3 {O(1)}

MPRF:

• h: [X₀]
• i: [X₀]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:23 {O(1)}
g₀: 3 {O(1)}
g₄: 1 {O(1)}
g₆: 4 {O(1)}
g₈: 12 {O(1)}
g₁₀: 3 {O(1)}

Costbounds

Overall costbound: inf {Infinity}
g₀: inf {Infinity}
g₄: inf {Infinity}
g₆: inf {Infinity}
g₈: inf {Infinity}
g₁₀: inf {Infinity}

Sizebounds

(g₀,g), X₀: 6 {O(1)}
(g₀,g), X₁: X₁ {O(n)}
(g₀,g), X₂: X₂ {O(n)}
(g₄,h), X₀: 3 {O(1)}
(g₄,h), X₁: X₁ {O(n)}
(g₄,h), X₂: 3 {O(1)}
(g₆,i), X₀: 3 {O(1)}
(g₆,i), X₁: 3 {O(1)}
(g₆,i), X₂: 3 {O(1)}
(g₈,i), X₀: 3 {O(1)}
(g₈,i), X₁: 2 {O(1)}
(g₈,i), X₂: 3 {O(1)}
(g₁₀,h), X₀: 2 {O(1)}
(g₁₀,h), X₁: 0 {O(1)}
(g₁₀,h), X₂: 3 {O(1)}

Run probabilistic analysis on SCC: [h; i]

Results of Probabilistic Analysis

All Bounds

Timebounds

Overall timebound:23 {O(1)}
g₀: 3 {O(1)}
g₄: 1 {O(1)}
g₆: 4 {O(1)}
g₈: 12 {O(1)}
g₁₀: 3 {O(1)}

Costbounds

Overall costbound: 29 {O(1)}
g₀: 9 {O(1)}
g₄: 1 {O(1)}
g₆: 4 {O(1)}
g₈: 12 {O(1)}
g₁₀: 3 {O(1)}

Sizebounds

(g₀,g), X₀: 6 {O(1)}
(g₀,g), X₁: X₁ {O(n)}
(g₀,g), X₂: X₂ {O(n)}
(g₄,h), X₀: 3 {O(1)}
(g₄,h), X₁: X₁ {O(n)}
(g₄,h), X₂: 3 {O(1)}
(g₆,i), X₀: 3 {O(1)}
(g₆,i), X₁: 3 {O(1)}
(g₆,i), X₂: 3 {O(1)}
(g₈,i), X₀: 3 {O(1)}
(g₈,i), X₁: 2 {O(1)}
(g₈,i), X₂: 3 {O(1)}
(g₁₀,h), X₀: 2 {O(1)}
(g₁₀,h), X₁: 0 {O(1)}
(g₁₀,h), X₂: 3 {O(1)}