Preprocessing

Found invariant 0 ≤ X₁ ∧ X₀ ≤ X₁ ∧ X₀ ≤ 0 for location h

Found invariant 0 ≤ X₁ for location g

Found invariant 0 ≤ X₁ ∧ X₀ ≤ X₁ ∧ X₀ ≤ 0 for location i

Probabilistic Analysis

Probabilistic Program after Preprocessing

Start: f
Program_Vars: X₀, X₁
Temp_Vars:
Locations: f, g, h, i
Transitions:
g₀:f(X₀,X₁) -{0}> t₁:g(X₀,X₁) :|: 0 ≤ X₁
g₂:g(X₀,X₁) -{9}> [9/10]:t₃:h(1+X₀,X₁) :+: [1/10]:t₄:h(X₀,X₁) :|: 1+X₀ ≤ 0 ∧ 0 ≤ X₁
g₅:h(X₀,X₁) -{0}> t₆:i(X₀,X₁) :|: X₀ ≤ 0 ∧ X₀ ≤ X₁ ∧ 0 ≤ X₁
g₇:h(X₀,X₁) -{0}> t₈:g(X₀,X₁) :|: X₀ ≤ 0 ∧ X₀ ≤ X₁ ∧ 0 ≤ X₁
g₉:i(X₀,X₁) -{5}> [1/2]:t₁₀:i(X₀,X₁-100) :+: [1/2]:t₁₁:i(X₀,X₁-90) :|: 100 ≤ X₁ ∧ X₀ ≤ 0 ∧ X₀ ≤ X₁ ∧ 0 ≤ X₁
g₁₂:i(X₀,X₁) -{0}> t₁₃:g(X₀,1000+X₁) :|: X₁ ≤ 99 ∧ 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₁₂: 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}

Sizebounds

(g₀,g), X₀: X₀ {O(n)}
(g₀,g), X₁: X₁ {O(n)}

Run probabilistic analysis on SCC: [f]

Run classical analysis on SCC: [g; h; i]

MPRF for transition t₃: g(X₀,X₁) -{9}> h(1+X₀,X₁) :|: 0 ≤ X₁ ∧ 1+X₀ ≤ 0 of depth 1:

new bound:

X₀ {O(n)}

MPRF:

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

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₁₂: 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}

Sizebounds

(g₀,g), X₀: X₀ {O(n)}
(g₀,g), X₁: X₁ {O(n)}
(g₂,h), X₀: 2⋅X₀ {O(n)}
(g₂,h), X₁: 2⋅X₁+2200 {O(n)}
(g₅,i), X₀: X₀ {O(n)}
(g₅,i), X₁: 2⋅X₁+2200 {O(n)}
(g₇,g), X₀: X₀ {O(n)}
(g₇,g), X₁: X₁+1100 {O(n)}
(g₉,i), X₀: 2⋅X₀ {O(n)}
(g₉,i), X₁: 4⋅X₁+4400 {O(n)}
(g₁₂,g), X₀: X₀ {O(n)}
(g₁₂,g), X₁: 1100 {O(1)}

Run probabilistic analysis on SCC: [g; h; i]

Plrf for transition g₂:g(X₀,X₁) -{9}> [9/10]:t₃:h(1+X₀,X₁) :+: [1/10]:t₄:h(X₀,X₁) :|: 1+X₀ ≤ 0 ∧ 0 ≤ X₁:

new bound:

10/9⋅X₀ {O(n)}

PLRF:

• g: -10/9⋅X₀
• h: -10/9⋅X₀
• i: -10/9⋅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₁) -{0}> t₆:i(X₀,X₁) :|: X₀ ≤ 0 ∧ X₀ ≤ X₁ ∧ 0 ≤ X₁:

new bound:

10/9⋅X₀ {O(n)}

PLRF:

• g: -10/9⋅X₀
• h: 1-10/9⋅X₀
• i: -10/9⋅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₁) -{0}> t₈:g(X₀,X₁) :|: X₀ ≤ 0 ∧ X₀ ≤ X₁ ∧ 0 ≤ X₁:

new bound:

10/9⋅X₀ {O(n)}

PLRF:

• g: -10/9⋅X₀
• h: 1-10/9⋅X₀
• i: -10/9⋅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₁) -{5}> [1/2]:t₁₀:i(X₀,X₁-100) :+: [1/2]:t₁₁:i(X₀,X₁-90) :|: 100 ≤ X₁ ∧ X₀ ≤ 0 ∧ X₀ ≤ X₁ ∧ 0 ≤ X₁:

new bound:

1/95⋅X₁+2000/171⋅X₀ {O(n)}

PLRF:

• g: 1/95⋅X₁-2000/171⋅X₀
• h: 200/19+1/95⋅X₁-2000/171⋅X₀
• i: 200/19+1/95⋅X₁-2000/171⋅X₀

Use expected size bounds for entry point (g₀:f→[t₁:1:g],g)
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₁) -{0}> t₁₃:g(X₀,1000+X₁) :|: X₁ ≤ 99 ∧ X₀ ≤ 0 ∧ X₀ ≤ X₁ ∧ 0 ≤ X₁:

new bound:

10/9⋅X₀ {O(n)}

PLRF:

• g: -10/9⋅X₀
• h: 1-10/9⋅X₀
• i: 1-10/9⋅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)

Results of Probabilistic Analysis

All Bounds

Timebounds

Overall timebound:1/95⋅X₁+920/57⋅X₀+1 {O(n)}
g₀: 1 {O(1)}
g₂: 10/9⋅X₀ {O(n)}
g₅: 10/9⋅X₀ {O(n)}
g₇: 10/9⋅X₀ {O(n)}
g₉: 1/95⋅X₁+2000/171⋅X₀ {O(n)}
g₁₂: 10/9⋅X₀ {O(n)}

Costbounds

Overall costbound: 2/19⋅X₁+23420/171⋅X₀ {O(n)}
g₀: 0 {O(1)}
g₂: 20⋅X₀ {O(n)}
g₅: 0 {O(1)}
g₇: 0 {O(1)}
g₉: 2/19⋅X₁+20000/171⋅X₀ {O(n)}
g₁₂: 0 {O(1)}

Sizebounds

(g₀,g), X₀: X₀ {O(n)}
(g₀,g), X₁: X₁ {O(n)}
(g₂,h), X₀: X₀ {O(n)}
(g₂,h), X₁: 2⋅X₁+2200 {O(n)}
(g₅,i), X₀: X₀ {O(n)}
(g₅,i), X₁: 2⋅X₁+2200 {O(n)}
(g₇,g), X₀: X₀ {O(n)}
(g₇,g), X₁: X₁+1100 {O(n)}
(g₉,i), X₀: X₀ {O(n)}
(g₉,i), X₁: 4⋅X₁+4400 {O(n)}
(g₁₂,g), X₀: X₀ {O(n)}
(g₁₂,g), X₁: 1100 {O(1)}