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)}