Preprocessing

Found invariant 0 ≤ X₂ for location h

Found invariant 0 ≤ X₂ ∧ 1+X₁ ≤ X₀ ∧ X₀ ≤ 3+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₂) -{0}> t₂:g(X₀,X₁,X₂) :|:
g₃:g(X₀,X₁,X₂) -{0}> t₄:h(X₀,X₁,X₂) :|: 0 ≤ X₂
g₅:h(X₀,X₁,X₂) → t₆:h(X₀-1,X₁,X₂) :|: 1+X₁ ≤ X₀ ∧ 0 ≤ X₂
g₇:h(X₀,X₁,X₂) -{0}> [1/10]:t₈:i(1+X₀,X₁,X₂) :+: [7/10]:t₉:i(2+X₀,X₁,X₂) :+: [1/5]:t₁₀:i(3+X₀,X₁,X₂) :|: X₁ ≤ X₀ ∧ X₀ ≤ X₁ ∧ 0 ≤ X₂
g₁₁:i(X₀,X₁,X₂) -{0}> t₁₂:g(X₀+UNIFORM(-1, 1),X₁,X₂-5) :|: X₀ ≤ 3+X₁ ∧ 0 ≤ 1 ∧ 1+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}

Costbounds

Overall costbound: 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)}

Run probabilistic analysis on SCC: [f]

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

MPRF for transition t₄: g(X₀,X₁,X₂) -{0}> h(X₀,X₁,X₂) :|: 0 ≤ X₂ of depth 1:

new bound:

X₂+1 {O(n)}

MPRF:

• g: [1+X₂]
• h: [X₂-4]
• i: [X₂-4]

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

new bound:

4⋅X₂+5⋅X₀+5⋅X₁ {O(n)}

MPRF:

• g: [5⋅X₀+4⋅X₂-5⋅X₁]
• h: [5⋅X₀+4⋅X₂-5⋅X₁]
• i: [4⋅X₂]

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

new bound:

X₂+5 {O(n)}

MPRF:

• g: [5+X₂]
• h: [5+X₂]
• i: [X₂]

MPRF for transition t₉: h(X₀,X₁,X₂) -{0}> i(2+X₀,X₁,X₂) :|: 0 ≤ X₂ ∧ X₀ ≤ X₁ ∧ X₁ ≤ X₀ of depth 1:

new bound:

X₂+5 {O(n)}

MPRF:

• g: [5+X₂]
• h: [5+X₂]
• i: [X₂]

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

new bound:

X₂+5 {O(n)}

MPRF:

• g: [5+X₂]
• h: [5+X₂]
• i: [X₂]

MPRF for transition t₁₂: i(X₀,X₁,X₂) -{0}> g(Temp_Int₇₉,X₁,X₂-5) :|: X₀ ≤ 3+X₁ ∧ 0 ≤ 1 ∧ 1+X₁ ≤ X₀ ∧ 0 ≤ X₂ ∧ X₀ ≤ 1+Temp_Int₇₉ ∧ X₀ ≤ 3+X₁ ∧ Temp_Int₁ ≤ 1+X₀ ∧ Temp_Int₇₉ ≤ 1+X₀ ∧ 1+X₁ ≤ X₀ ∧ X₀ ≤ 1+Temp_Int₁ ∧ 0 ≤ X₂ ∧ Temp_Int₂+X₀ ≤ Temp_Int₁ ∧ Temp_Int₁ ≤ Temp_Int₂+X₀ ∧ Temp_Int₁ ≤ Temp_Int₂+X₀ ∧ Temp_Int₂+X₀ ≤ Temp_Int₁ ∧ 0 ≤ 1+Temp_Int₂ ∧ Temp_Int₂ ≤ 1 of depth 1:

new bound:

X₂+1 {O(n)}

MPRF:

• g: [1+X₂]
• h: [1+X₂]
• i: [1+X₂]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:5⋅X₀+5⋅X₁+9⋅X₂+18 {O(n)}
g₁: 1 {O(1)}
g₃: X₂+1 {O(n)}
g₅: 4⋅X₂+5⋅X₀+5⋅X₁ {O(n)}
g₇: 3⋅X₂+15 {O(n)}
g₁₁: X₂+1 {O(n)}

Costbounds

Overall costbound: 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₃,h), X₀: 11⋅X₂+5⋅X₁+6⋅X₀+31 {O(n)}
(g₃,h), X₁: X₁ {O(n)}
(g₃,h), X₂: X₂+5 {O(n)}
(g₅,h), X₀: 11⋅X₂+5⋅X₁+6⋅X₀+31 {O(n)}
(g₅,h), X₁: X₁ {O(n)}
(g₅,h), X₂: X₂+5 {O(n)}
(g₇,i), X₀: 15⋅X₁+18⋅X₀+33⋅X₂+93 {O(n)}
(g₇,i), X₁: 3⋅X₁ {O(n)}
(g₇,i), X₂: 3⋅X₂+15 {O(n)}
(g₁₁,g), X₀: 11⋅X₂+5⋅X₁+6⋅X₀+31 {O(n)}
(g₁₁,g), X₁: X₁ {O(n)}
(g₁₁,g), X₂: X₂+5 {O(n)}

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

Results of Probabilistic Analysis

All Bounds

Timebounds

Overall timebound:5⋅X₀+5⋅X₁+9⋅X₂+18 {O(n)}
g₁: 1 {O(1)}
g₃: X₂+1 {O(n)}
g₅: 4⋅X₂+5⋅X₀+5⋅X₁ {O(n)}
g₇: 3⋅X₂+15 {O(n)}
g₁₁: X₂+1 {O(n)}

Costbounds

Overall costbound: 4⋅X₂+5⋅X₀+5⋅X₁ {O(n)}
g₁: 0 {O(1)}
g₃: 0 {O(1)}
g₅: 4⋅X₂+5⋅X₀+5⋅X₁ {O(n)}
g₇: 0 {O(1)}
g₁₁: 0 {O(1)}

Sizebounds

(g₁,g), X₀: X₀ {O(n)}
(g₁,g), X₁: X₁ {O(n)}
(g₁,g), X₂: X₂ {O(n)}
(g₃,h), X₀: 11⋅X₂+5⋅X₁+6⋅X₀+31 {O(n)}
(g₃,h), X₁: X₁ {O(n)}
(g₃,h), X₂: X₂+5 {O(n)}
(g₅,h), X₀: 11⋅X₂+5⋅X₁+6⋅X₀+31 {O(n)}
(g₅,h), X₁: X₁ {O(n)}
(g₅,h), X₂: X₂+5 {O(n)}
(g₇,i), X₀: 15⋅X₁+18⋅X₀+33⋅X₂+93 {O(n)}
(g₇,i), X₁: X₁ {O(n)}
(g₇,i), X₂: 6⋅X₂+5 {O(n)}
(g₁₁,g), X₀: 11⋅X₂+5⋅X₁+6⋅X₀+31 {O(n)}
(g₁₁,g), X₁: X₁ {O(n)}
(g₁₁,g), X₂: X₂+5 {O(n)}