Preprocessing
Found invariant 1 ≤ X₂ ∧ 2 ≤ X₁+X₂ ∧ X₁ ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ 4+X₂ ∧ 1 ≤ X₁ ∧ 2 ≤ X₀+X₁ ∧ X₀ ≤ 4+X₁ ∧ X₀ ≤ 6 ∧ 1 ≤ X₀ for location h
Found invariant 0 ≤ X₁ ∧ 1 ≤ X₀+X₁ ∧ X₀ ≤ 5+X₁ ∧ X₀ ≤ 6 ∧ 1 ≤ X₀ for location g
Probabilistic Analysis
Probabilistic Program after Preprocessing
Start: f
Program_Vars: X₀, X₁, X₂
Temp_Vars:
Locations: f, g, h
Transitions:
g₁:f(X₀,X₁,X₂) -{0}> t₂:g(1,0,X₂) :|:
g₃:g(X₀,X₁,X₂) → t₄:h(X₀,1+X₁,X₂) :|: 1+X₁ ≤ X₂ ∧ X₀ ≤ 6 ∧ X₀ ≤ 5+X₁ ∧ 1 ≤ X₀ ∧ 1 ≤ X₀+X₁ ∧ 0 ≤ X₁
g₅:h(X₀,X₁,X₂) -{41}> t₆:g(1,X₁,X₂) :|: 4 ≤ X₀ ∧ X₀ ≤ 6 ∧ X₀ ≤ 4+X₁ ∧ X₀ ≤ 4+X₂ ∧ 1 ≤ X₀ ∧ 1 ≤ X₁ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₁ ∧ 2 ≤ X₀+X₂ ∧ 2 ≤ X₁+X₂ ∧ X₁ ≤ X₂
g₇:h(X₀,X₁,X₂) → t₈:g(X₀+UNIFORM(1, 3),X₁,X₂) :|: X₀ ≤ 3 ∧ X₀ ≤ 6 ∧ X₀ ≤ 4+X₁ ∧ X₀ ≤ 4+X₂ ∧ 0 ≤ 1 ∧ 1 ≤ X₀ ∧ 1 ≤ X₁ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₁ ∧ 2 ≤ X₀+X₂ ∧ 2 ≤ X₁+X₂ ∧ X₁ ≤ X₂
Run classical analysis on SCC: [f]
Classical Approximation after Lifting Classical Results
All Bounds
Timebounds
Overall timebound:inf {Infinity}
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}
Sizebounds
(g₁,g), X₀: 1 {O(1)}
(g₁,g), X₁: 0 {O(1)}
(g₁,g), X₂: X₂ {O(n)}
Run probabilistic analysis on SCC: [f]
Run classical analysis on SCC: [g; h]
MPRF for transition t₄: g(X₀,X₁,X₂) → h(X₀,1+X₁,X₂) :|: X₀ ≤ 6 ∧ X₀ ≤ 5+X₁ ∧ 1 ≤ X₀ ∧ 1 ≤ X₀+X₁ ∧ 0 ≤ X₁ ∧ 1+X₁ ≤ X₂ of depth 1:
new bound:
X₂ {O(n)}
MPRF:
• g: [X₂-X₁]
• h: [X₂-X₁]
MPRF for transition t₆: h(X₀,X₁,X₂) -{41}> g(Temp_Int₅₀,X₁,X₂) :|: X₀ ≤ 6 ∧ X₀ ≤ 4+X₁ ∧ X₀ ≤ 4+X₂ ∧ 1 ≤ X₀ ∧ 1 ≤ X₁ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₁ ∧ 2 ≤ X₀+X₂ ∧ 2 ≤ X₁+X₂ ∧ X₁ ≤ X₂ ∧ X₀ ≤ 6 ∧ 4 ≤ X₀ ∧ 1 ≤ X₁ ∧ X₀ ≤ 4+X₁ ∧ X₁ ≤ X₂ ∧ Temp_Int₅₀ ≤ 1 ∧ 1 ≤ Temp_Int₅₀ ∧ 4 ≤ X₀ of depth 1:
new bound:
X₂ {O(n)}
MPRF:
• g: [X₂-X₁]
• h: [1+X₂-X₁]
MPRF for transition t₈: h(X₀,X₁,X₂) → g(Temp_Int₅₁,X₁,X₂) :|: X₀ ≤ 6 ∧ X₀ ≤ 4+X₁ ∧ X₀ ≤ 4+X₂ ∧ 0 ≤ 1 ∧ 1 ≤ X₀ ∧ 1 ≤ X₁ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₁ ∧ 2 ≤ X₀+X₂ ∧ 2 ≤ X₁+X₂ ∧ X₁ ≤ X₂ ∧ 1+Temp_Int₁ ≤ Temp_Int₂+Temp_Int₅₁ ∧ 1 ≤ Temp_Int₂ ∧ 1+Temp_Int₂ ≤ Temp_Int₁ ∧ Temp_Int₂+Temp_Int₅₁ ≤ 3+Temp_Int₁ ∧ Temp_Int₂ ≤ 3 ∧ Temp_Int₁ ≤ 3+Temp_Int₂ ∧ 1 ≤ X₁ ∧ X₁ ≤ X₂ ∧ Temp_Int₂+X₀ ≤ Temp_Int₁ ∧ Temp_Int₁ ≤ Temp_Int₂+X₀ ∧ Temp_Int₁ ≤ Temp_Int₂+X₀ ∧ Temp_Int₂+X₀ ≤ Temp_Int₁ ∧ 1 ≤ Temp_Int₂ ∧ Temp_Int₂ ≤ 3 ∧ X₀ ≤ 3 of depth 1:
new bound:
5⋅X₂+3 {O(n)}
MPRF:
• g: [2+5⋅X₂-X₀-5⋅X₁]
• h: [7+5⋅X₂-X₀-5⋅X₁]
Classical Approximation after Lifting Classical Results
All Bounds
Timebounds
Overall timebound:7⋅X₂+4 {O(n)}
g₁: 1 {O(1)}
g₃: X₂ {O(n)}
g₅: X₂ {O(n)}
g₇: 5⋅X₂+3 {O(n)}
Costbounds
Overall costbound: inf {Infinity}
g₁: inf {Infinity}
g₃: inf {Infinity}
g₅: inf {Infinity}
g₇: inf {Infinity}
Sizebounds
(g₁,g), X₀: 1 {O(1)}
(g₁,g), X₁: 0 {O(1)}
(g₁,g), X₂: X₂ {O(n)}
(g₃,h), X₀: 6 {O(1)}
(g₃,h), X₁: X₂ {O(n)}
(g₃,h), X₂: X₂ {O(n)}
(g₅,g), X₀: 1 {O(1)}
(g₅,g), X₁: X₂ {O(n)}
(g₅,g), X₂: X₂ {O(n)}
(g₇,g), X₀: 6 {O(1)}
(g₇,g), X₁: X₂ {O(n)}
(g₇,g), X₂: X₂ {O(n)}
Run probabilistic analysis on SCC: [g; h]
Results of Probabilistic Analysis
All Bounds
Timebounds
Overall timebound:7⋅X₂+4 {O(n)}
g₁: 1 {O(1)}
g₃: X₂ {O(n)}
g₅: X₂ {O(n)}
g₇: 5⋅X₂+3 {O(n)}
Costbounds
Overall costbound: 47⋅X₂+3 {O(n)}
g₁: 0 {O(1)}
g₃: X₂ {O(n)}
g₅: 41⋅X₂ {O(n)}
g₇: 5⋅X₂+3 {O(n)}
Sizebounds
(g₁,g), X₀: 1 {O(1)}
(g₁,g), X₁: 0 {O(1)}
(g₁,g), X₂: X₂ {O(n)}
(g₃,h), X₀: 6 {O(1)}
(g₃,h), X₁: X₂ {O(n)}
(g₃,h), X₂: X₂ {O(n)}
(g₅,g), X₀: 1 {O(1)}
(g₅,g), X₁: X₂ {O(n)}
(g₅,g), X₂: X₂ {O(n)}
(g₇,g), X₀: 6 {O(1)}
(g₇,g), X₁: X₂ {O(n)}
(g₇,g), X₂: X₂ {O(n)}