Preprocessing

Found invariant X₀ ≤ 10+X₁ for location i

Probabilistic Analysis

Probabilistic Program after Preprocessing

Start: f
Program_Vars: X₀, X₁
Temp_Vars:
Locations: f, g, i
Transitions:
g₁:f(X₀,X₁) -{0}> t₂:g(X₀,X₁) :|:
g₃:g(X₀,X₁) → t₄:i(1+X₀,X₁) :|: X₀ ≤ 9+X₁
g₅:i(X₀,X₁) → t₆:g(X₀+Geometric (1/2),1+X₁) :|: X₀ ≤ 10+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}

Costbounds

Overall costbound: 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; i]

MPRF for transition t₄: g(X₀,X₁) → i(1+X₀,X₁) :|: X₀ ≤ 9+X₁ of depth 1:

new bound:

X₀+X₁+10 {O(n)}

MPRF:

• g: [10+X₁-X₀]
• i: [10+X₁-X₀]

MPRF for transition t₆: i(X₀,X₁) → g(Temp_Int₂₂,1+X₁) :|: X₀ ≤ 10+X₁ ∧ 1 ≤ Temp_Int₂ ∧ 1+X₀ ≤ Temp_Int₂₂ ∧ X₀ ≤ 10+X₁ ∧ Temp_Int₂+X₀ ≤ Temp_Int₁ ∧ Temp_Int₁ ≤ Temp_Int₂+X₀ ∧ Temp_Int₁ ≤ Temp_Int₂+X₀ ∧ Temp_Int₂+X₀ ≤ Temp_Int₁ ∧ 1 ≤ Temp_Int₂ of depth 1:

new bound:

X₀+X₁+10 {O(n)}

MPRF:

• g: [10+X₁-X₀]
• i: [11+X₁-X₀]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:2⋅X₀+2⋅X₁+21 {O(n)}
g₁: 1 {O(1)}
g₃: X₀+X₁+10 {O(n)}
g₅: X₀+X₁+10 {O(n)}

Costbounds

Overall costbound: 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₃,i), X₁: 2⋅X₁+X₀+10 {O(n)}
(g₅,g), X₁: 2⋅X₁+X₀+10 {O(n)}

Run probabilistic analysis on SCC: [g; i]

Results of Probabilistic Analysis

All Bounds

Timebounds

Overall timebound:2⋅X₀+2⋅X₁+21 {O(n)}
g₁: 1 {O(1)}
g₃: X₀+X₁+10 {O(n)}
g₅: X₀+X₁+10 {O(n)}

Costbounds

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

Sizebounds

(g₁,g), X₀: X₀ {O(n)}
(g₁,g), X₁: X₁ {O(n)}
(g₃,i), X₀: 3⋅X₁+4⋅X₀+30 {O(n)}
(g₃,i), X₁: 2⋅X₁+X₀+10 {O(n)}
(g₅,g), X₀: 3⋅X₁+4⋅X₀+30 {O(n)}
(g₅,g), X₁: 2⋅X₁+X₀+10 {O(n)}