Preprocessing

Cut unsatisfiable transition [t₁₉∈g₁₈: j→1:g]

Found invariant X₃ ≤ 0 ∧ X₃ ≤ X₀ ∧ 0 ≤ X₃ ∧ 0 ≤ X₀+X₃ ∧ X₁ ≤ X₀ ∧ 0 ≤ X₀ for location termination

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

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

Found invariant X₃ ≤ 0 ∧ X₃ ≤ X₀ ∧ 0 ≤ X₃ ∧ 0 ≤ X₀+X₃ ∧ 0 ≤ X₀ for location g

Found invariant 0 ≤ X₃ ∧ 0 ≤ 2+X₂+X₃ ∧ X₂ ≤ 3+X₃ ∧ 0 ≤ X₁+X₃ ∧ 0 ≤ X₀+X₃ ∧ X₂ ≤ 3 ∧ X₂ ≤ 3+X₁ ∧ X₂ ≤ 3+X₀ ∧ 0 ≤ 2+X₂ ∧ 0 ≤ 2+X₁+X₂ ∧ 0 ≤ 2+X₀+X₂ ∧ 0 ≤ X₁ ∧ 0 ≤ X₀+X₁ ∧ X₀ ≤ X₁ ∧ 0 ≤ X₀ for location i

Cut unsatisfiable transition [t₂₃∈g₂₂: termination→1:termination]

Probabilistic Analysis

Probabilistic Program after Preprocessing

Start: f
Program_Vars: X₀, X₁, X₂, X₃
Temp_Vars:
Locations: f, g, h, i, j, termination
Transitions:
g₀:f(X₀,X₁,X₂,X₃) -{0}> t₁:g(X₀,X₁,X₂,0) :|: 0 ≤ X₀
g₂:g(X₀,X₁,X₂,X₃) -{0}> [1/4]:t₃:h(X₀,1+X₁,X₂,X₃) :+: [3/4]:t₄:h(X₀,X₁-1,X₂,X₃) :|: 1+X₀ ≤ X₁ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₃ ∧ X₃ ≤ X₀ ∧ 0 ≤ X₃ ∧ X₃ ≤ 0
g₅:h(X₀,X₁,X₂,X₃) -{0}> [1/6]:t₆:i(X₀,X₁,-2,X₃) :+: [1/6]:t₇:i(X₀,X₁,-1,X₃) :+: [1/6]:t₈:i(X₀,X₁,0,X₃) :+: [1/6]:t₉:i(X₀,X₁,1,X₃) :+: [1/6]:t₁₀:i(X₀,X₁,2,X₃) :+: [1/6]:t₁₁:i(X₀,X₁,3,X₃) :|: 0 ≤ X₀ ∧ 0 ≤ X₀+X₁ ∧ 0 ≤ X₀+X₃ ∧ X₃ ≤ X₀ ∧ X₀ ≤ X₁ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₃ ∧ X₃ ≤ X₁ ∧ 0 ≤ X₃ ∧ X₃ ≤ 0
g₁₂:i(X₀,X₁,X₂,X₃) -{0}> t₁₃:i(X₀,X₁,X₂-1,X₁+X₃) :|: 1 ≤ X₂ ∧ X₂ ≤ 3+X₀ ∧ X₂ ≤ 3+X₁ ∧ X₂ ≤ 3 ∧ X₂ ≤ 3+X₃ ∧ 0 ≤ 2+X₀+X₂ ∧ 0 ≤ 2+X₁+X₂ ∧ 0 ≤ 2+X₂ ∧ 0 ≤ 2+X₂+X₃ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₁ ∧ 0 ≤ X₀+X₃ ∧ X₀ ≤ X₁ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₃ ∧ 0 ≤ X₃
g₁₄:i(X₀,X₁,X₂,X₃) -{0}> t₁₅:j(X₀,X₁,X₂-1,X₃) :|: X₂ ≤ 0 ∧ X₂ ≤ 3+X₀ ∧ X₂ ≤ 3+X₁ ∧ X₂ ≤ 3 ∧ X₂ ≤ 3+X₃ ∧ 0 ≤ 2+X₀+X₂ ∧ 0 ≤ 2+X₁+X₂ ∧ 0 ≤ 2+X₂ ∧ 0 ≤ 2+X₂+X₃ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₁ ∧ 0 ≤ X₀+X₃ ∧ X₀ ≤ X₁ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₃ ∧ 0 ≤ X₃
g₁₆:j(X₀,X₁,X₂,X₃) -{0}> t₁₇:j(X₀,X₁,X₂-1,X₃-X₁) :|: 1+X₂ ≤ 0 ∧ 1+X₂ ≤ X₀ ∧ 1+X₂ ≤ X₁ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₁ ∧ X₀ ≤ X₁ ∧ 0 ≤ X₁
g₂₀:g(X₀,X₁,X₂,X₃) -{0}> t₂₁:termination(X₀,X₁,X₂,X₃) :|: X₁ ≤ X₀ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₃ ∧ X₃ ≤ X₀ ∧ 0 ≤ X₃ ∧ X₃ ≤ 0

Run classical analysis on SCC: [f]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:inf {Infinity}
g₀: 1 {O(1)}
g₂: 1 {O(1)}
g₅: 1 {O(1)}
g₁₂: inf {Infinity}
g₁₄: 1 {O(1)}
g₁₆: inf {Infinity}
g₂₀: 1 {O(1)}

Costbounds

Overall costbound: inf {Infinity}
g₀: 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₀,g), X₂: X₂ {O(n)}
(g₀,g), X₃: 0 {O(1)}

Run probabilistic analysis on SCC: [f]

Run classical analysis on SCC: [g]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:inf {Infinity}
g₀: 1 {O(1)}
g₂: 2 {O(1)}
g₅: 1 {O(1)}
g₁₂: inf {Infinity}
g₁₄: 1 {O(1)}
g₁₆: inf {Infinity}
g₂₀: 1 {O(1)}

Costbounds

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

Run probabilistic analysis on SCC: [g]

Run classical analysis on SCC: [h]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:inf {Infinity}
g₀: 1 {O(1)}
g₂: 2 {O(1)}
g₅: 6 {O(1)}
g₁₂: inf {Infinity}
g₁₄: 1 {O(1)}
g₁₆: inf {Infinity}
g₂₀: 1 {O(1)}

Costbounds

Overall costbound: inf {Infinity}
g₀: 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₀,g), X₂: X₂ {O(n)}
(g₀,g), X₃: 0 {O(1)}
(g₂,h), X₀: X₀ {O(n)}
(g₂,h), X₁: X₁+1 {O(n)}
(g₂,h), X₂: X₂ {O(n)}
(g₂,h), X₃: 0 {O(1)}
(g₅,i), X₀: 12⋅X₀ {O(n)}
(g₅,i), X₁: 12⋅X₁+6 {O(n)}
(g₅,i), X₂: 9 {O(1)}
(g₅,i), X₃: 0 {O(1)}
(g₂₀,termination), X₀: X₀ {O(n)}
(g₂₀,termination), X₁: X₁ {O(n)}
(g₂₀,termination), X₂: X₂ {O(n)}
(g₂₀,termination), X₃: 0 {O(1)}

Run probabilistic analysis on SCC: [h]

Run classical analysis on SCC: [i]

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

new bound:

6 {O(1)}

MPRF:

• i: [X₂]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:inf {Infinity}
g₀: 1 {O(1)}
g₂: 2 {O(1)}
g₅: 6 {O(1)}
g₁₂: 6 {O(1)}
g₁₄: 1 {O(1)}
g₁₆: inf {Infinity}
g₂₀: 1 {O(1)}

Costbounds

Overall costbound: inf {Infinity}
g₀: 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₀,g), X₂: X₂ {O(n)}
(g₀,g), X₃: 0 {O(1)}
(g₂,h), X₀: X₀ {O(n)}
(g₂,h), X₁: X₁+1 {O(n)}
(g₂,h), X₂: X₂ {O(n)}
(g₂,h), X₃: 0 {O(1)}
(g₅,i), X₀: X₀ {O(n)}
(g₅,i), X₁: X₁+1 {O(n)}
(g₅,i), X₂: 9 {O(1)}
(g₅,i), X₃: 0 {O(1)}
(g₁₂,i), X₀: 6⋅X₀ {O(n)}
(g₁₂,i), X₁: 6⋅X₁+3 {O(n)}
(g₁₂,i), X₂: 2 {O(1)}
(g₁₂,i), X₃: 84⋅X₁+42 {O(n)}
(g₁₄,j), X₀: 12⋅X₀ {O(n)}
(g₁₄,j), X₁: 12⋅X₁+6 {O(n)}
(g₁₄,j), X₂: 3 {O(1)}
(g₁₄,j), X₃: 84⋅X₁+42 {O(n)}
(g₂₀,termination), X₀: X₀ {O(n)}
(g₂₀,termination), X₁: X₁ {O(n)}
(g₂₀,termination), X₂: X₂ {O(n)}
(g₂₀,termination), X₃: 0 {O(1)}

Run probabilistic analysis on SCC: [i]

Run classical analysis on SCC: [j]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:inf {Infinity}
g₀: 1 {O(1)}
g₂: 2 {O(1)}
g₅: 6 {O(1)}
g₁₂: 6 {O(1)}
g₁₄: 1 {O(1)}
g₁₆: inf {Infinity}
g₂₀: 1 {O(1)}

Costbounds

Overall costbound: inf {Infinity}
g₀: 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₀,g), X₂: X₂ {O(n)}
(g₀,g), X₃: 0 {O(1)}
(g₂,h), X₀: X₀ {O(n)}
(g₂,h), X₁: X₁+1 {O(n)}
(g₂,h), X₂: X₂ {O(n)}
(g₂,h), X₃: 0 {O(1)}
(g₅,i), X₀: X₀ {O(n)}
(g₅,i), X₁: X₁+1 {O(n)}
(g₅,i), X₂: 9 {O(1)}
(g₅,i), X₃: 0 {O(1)}
(g₁₂,i), X₀: X₀ {O(n)}
(g₁₂,i), X₁: X₁+1 {O(n)}
(g₁₂,i), X₂: 2 {O(1)}
(g₁₂,i), X₃: 84⋅X₁+42 {O(n)}
(g₁₄,j), X₀: 7⋅X₀ {O(n)}
(g₁₄,j), X₁: 7⋅X₁+4 {O(n)}
(g₁₄,j), X₂: 3 {O(1)}
(g₁₄,j), X₃: 84⋅X₁+42 {O(n)}
(g₁₆,j), X₀: 12⋅X₀ {O(n)}
(g₁₆,j), X₁: 12⋅X₁+6 {O(n)}
(g₂₀,termination), X₀: X₀ {O(n)}
(g₂₀,termination), X₁: X₁ {O(n)}
(g₂₀,termination), X₂: X₂ {O(n)}
(g₂₀,termination), X₃: 0 {O(1)}

Run probabilistic analysis on SCC: [j]

Run classical analysis on SCC: [termination]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:inf {Infinity}
g₀: 1 {O(1)}
g₂: 2 {O(1)}
g₅: 6 {O(1)}
g₁₂: 6 {O(1)}
g₁₄: 1 {O(1)}
g₁₆: inf {Infinity}
g₂₀: 1 {O(1)}

Costbounds

Overall costbound: inf {Infinity}
g₀: 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₀,g), X₂: X₂ {O(n)}
(g₀,g), X₃: 0 {O(1)}
(g₂,h), X₀: X₀ {O(n)}
(g₂,h), X₁: X₁+1 {O(n)}
(g₂,h), X₂: X₂ {O(n)}
(g₂,h), X₃: 0 {O(1)}
(g₅,i), X₀: X₀ {O(n)}
(g₅,i), X₁: X₁+1 {O(n)}
(g₅,i), X₂: 9 {O(1)}
(g₅,i), X₃: 0 {O(1)}
(g₁₂,i), X₀: X₀ {O(n)}
(g₁₂,i), X₁: X₁+1 {O(n)}
(g₁₂,i), X₂: 2 {O(1)}
(g₁₂,i), X₃: 84⋅X₁+42 {O(n)}
(g₁₄,j), X₀: 7⋅X₀ {O(n)}
(g₁₄,j), X₁: 7⋅X₁+4 {O(n)}
(g₁₄,j), X₂: 3 {O(1)}
(g₁₄,j), X₃: 84⋅X₁+42 {O(n)}
(g₁₆,j), X₀: 7⋅X₀ {O(n)}
(g₁₆,j), X₁: 7⋅X₁+4 {O(n)}
(g₂₀,termination), X₀: X₀ {O(n)}
(g₂₀,termination), X₁: X₁ {O(n)}
(g₂₀,termination), X₂: X₂ {O(n)}
(g₂₀,termination), X₃: 0 {O(1)}

Run probabilistic analysis on SCC: [termination]

Results of Probabilistic Analysis

All Bounds

Timebounds

Overall timebound:inf {Infinity}
g₀: 1 {O(1)}
g₂: 2 {O(1)}
g₅: 6 {O(1)}
g₁₂: 6 {O(1)}
g₁₄: 1 {O(1)}
g₁₆: inf {Infinity}
g₂₀: 1 {O(1)}

Costbounds

Overall costbound: 0 {O(1)}
g₀: 0 {O(1)}
g₂: 0 {O(1)}
g₅: 0 {O(1)}
g₁₂: 0 {O(1)}
g₁₄: 0 {O(1)}
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₀,g), X₃: 0 {O(1)}
(g₂,h), X₀: X₀ {O(n)}
(g₂,h), X₁: X₁+1 {O(n)}
(g₂,h), X₂: X₂ {O(n)}
(g₂,h), X₃: 0 {O(1)}
(g₅,i), X₀: X₀ {O(n)}
(g₅,i), X₁: X₁+1 {O(n)}
(g₅,i), X₂: 9 {O(1)}
(g₅,i), X₃: 0 {O(1)}
(g₁₂,i), X₀: X₀ {O(n)}
(g₁₂,i), X₁: X₁+1 {O(n)}
(g₁₂,i), X₂: 2 {O(1)}
(g₁₂,i), X₃: 84⋅X₁+42 {O(n)}
(g₁₄,j), X₀: 7⋅X₀ {O(n)}
(g₁₄,j), X₁: 7⋅X₁+4 {O(n)}
(g₁₄,j), X₂: 3 {O(1)}
(g₁₄,j), X₃: 84⋅X₁+42 {O(n)}
(g₁₆,j), X₀: 7⋅X₀ {O(n)}
(g₁₆,j), X₁: 7⋅X₁+4 {O(n)}
(g₂₀,termination), X₀: X₀ {O(n)}
(g₂₀,termination), X₁: X₁ {O(n)}
(g₂₀,termination), X₂: X₂ {O(n)}
(g₂₀,termination), X₃: 0 {O(1)}