Preprocessing

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

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

Costbounds

Overall costbound: inf {Infinity}
g₀: inf {Infinity}
g₂: inf {Infinity}
g₅: inf {Infinity}

Sizebounds

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

Run probabilistic analysis on SCC: [f]

Run classical analysis on SCC: [g; h]

MPRF for transition t₃: g(X₀,X₁,X₂) → h(X₀,Temp_Int₄₇,X₂) :|: X₁ ≤ 1 ∧ X₁ ≤ 1+X₂ ∧ 1 ≤ X₁+X₂ ∧ 0 ≤ X₁ ∧ 0 ≤ X₂ ∧ 1+X₂ ≤ X₀ ∧ 0 ≤ X₂ ∧ X₁ ≤ 1 ∧ 1 ≤ X₁ ∧ Temp_Int₄₇ ≤ 0 ∧ 0 ≤ Temp_Int₄₇ ∧ 1+X₂ ≤ X₀ ∧ 1 ≤ X₁ of depth 1:

new bound:

2 {O(1)}

MPRF:

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

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

new bound:

X₀ {O(n)}

MPRF:

• g: [X₀-X₂]
• h: [X₀-1-X₂]

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

new bound:

X₀+1 {O(n)}

MPRF:

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

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:2⋅X₀+4 {O(n)}
g₀: 1 {O(1)}
g₂: X₀+2 {O(n)}
g₅: X₀+1 {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₁: 1 {O(1)}
(g₀,g), X₂: 0 {O(1)}
(g₂,h), X₀: 2⋅X₀ {O(n)}
(g₂,h), X₁: 1 {O(1)}
(g₂,h), X₂: 2⋅X₀+2 {O(n)}
(g₅,g), X₀: X₀ {O(n)}
(g₅,g), X₁: 1 {O(1)}
(g₅,g), X₂: X₀+1 {O(n)}

Run probabilistic analysis on SCC: [g; h]

Results of Probabilistic Analysis

All Bounds

Timebounds

Overall timebound:2⋅X₀+4 {O(n)}
g₀: 1 {O(1)}
g₂: X₀+2 {O(n)}
g₅: X₀+1 {O(n)}

Costbounds

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

Sizebounds

(g₀,g), X₀: X₀ {O(n)}
(g₀,g), X₁: 1 {O(1)}
(g₀,g), X₂: 0 {O(1)}
(g₂,h), X₀: X₀ {O(n)}
(g₂,h), X₁: 1 {O(1)}
(g₂,h), X₂: X₀+1 {O(n)}
(g₅,g), X₀: X₀ {O(n)}
(g₅,g), X₁: 1 {O(1)}
(g₅,g), X₂: X₀+1 {O(n)}