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