Preprocessing

Found invariant X₂ ≤ X₁ ∧ 0 ≤ 2+X₂ ∧ 0 ≤ 1+X₁+X₂ ∧ 0 ≤ X₁ ∧ 0 ≤ X₀+X₁ for location h

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

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

new bound:

X₀ {O(n)}

MPRF:

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

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

new bound:

2⋅X₀+X₁+2 {O(n)}

MPRF:

• g: [2⋅X₀+X₁-2]
• h: [2⋅X₀+2⋅X₁+X₂]

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

new bound:

X₀ {O(n)}

MPRF:

• g: [X₀]
• h: [1+X₀+X₁]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:4⋅X₀+X₁+3 {O(n)}
g₁: 1 {O(1)}
g₃: X₀ {O(n)}
g₅: 2⋅X₀+X₁+2 {O(n)}
g₇: X₀ {O(n)}

Costbounds

Overall costbound: 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₀: X₀ {O(n)}
(g₃,h), X₁: X₁ {O(n)}
(g₃,h), X₂: 2⋅X₁ {O(n)}
(g₅,h), X₀: X₀ {O(n)}
(g₅,h), X₁: X₁ {O(n)}
(g₅,h), X₂: 2⋅X₁ {O(n)}
(g₇,g), X₀: X₀ {O(n)}
(g₇,g), X₁: X₁ {O(n)}
(g₇,g), X₂: 2 {O(1)}

Run probabilistic analysis on SCC: [g; h]

Results of Probabilistic Analysis

All Bounds

Timebounds

Overall timebound:4⋅X₀+X₁+3 {O(n)}
g₁: 1 {O(1)}
g₃: X₀ {O(n)}
g₅: 2⋅X₀+X₁+2 {O(n)}
g₇: X₀ {O(n)}

Costbounds

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

Sizebounds

(g₁,g), X₀: X₀ {O(n)}
(g₁,g), X₁: X₁ {O(n)}
(g₁,g), X₂: X₂ {O(n)}
(g₃,h), X₀: X₀ {O(n)}
(g₃,h), X₁: X₁ {O(n)}
(g₃,h), X₂: 2⋅X₁ {O(n)}
(g₅,h), X₀: X₀ {O(n)}
(g₅,h), X₁: X₁ {O(n)}
(g₅,h), X₂: 2⋅X₁ {O(n)}
(g₇,g), X₀: X₀ {O(n)}
(g₇,g), X₁: X₁ {O(n)}
(g₇,g), X₂: 2 {O(1)}