Preprocessing

Found invariant X₀ ≤ 1 ∧ 0 ≤ 1+X₀ for location l1

Probabilistic Analysis

Probabilistic Program after Preprocessing

Start: l0
Program_Vars: X₀, X₁
Temp_Vars:
Locations: l0, l1
Transitions:
g₀:l0(X₀,X₁) → t₁:l1(1,X₁) :|:
g₂:l1(X₀,X₁) → t₃:l1(-X₀,-X₀-X₁) :|: X₁ ≤ 10 ∧ 1 ≤ X₀ ∧ 0 ≤ 1+X₀ ∧ X₀ ≤ 1
g₄:l1(X₀,X₁) → t₅:l1(-X₀,-X₀-X₁) :|: X₁ ≤ 10 ∧ 1+X₀ ≤ 0 ∧ 0 ≤ 1+X₀ ∧ X₀ ≤ 1

Run classical analysis on SCC: [l0]

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₀,l1), X₀: 1 {O(1)}
(g₀,l1), X₁: X₁ {O(n)}

Run probabilistic analysis on SCC: [l0]

Run classical analysis on SCC: [l1]

TWN: t₃: l1→l1

cycle: [t₃: l1→l1; t₅: l1→l1]
loop: (X₁ ≤ 10 ∧ 1 ≤ X₀ ∨ X₁ ≤ 10 ∧ 1+X₀ ≤ 0,(X₀,X₁) -> (-X₀,-X₀-X₁)
order: [X₀; X₁]
closed-form:
X₀: X₀
X₁: X₁ + [[n != 0]] * 2⋅X₀ * n^1

Termination: true
Formula:

0 ≤ 10+X₀+X₁ ∧ X₁ ≤ 10 ∧ 0 ≤ 1+X₀ ∧ X₀ ≤ 1 ∧ 1 ≤ X₀ ∧ 1+X₀ ≤ 0 ∧ 10+X₀+X₁ ≤ 0 ∧ 10 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 10+X₀+X₁ ∧ X₁ ≤ 10 ∧ 0 ≤ 1+X₀ ∧ 1+X₀ ≤ 0 ∧ 2 ≤ X₀ ∧ 10+X₀+X₁ ≤ 0 ∧ 10 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 10+X₀+X₁ ∧ X₁ ≤ 10 ∧ X₀ ≤ 1 ∧ 1 ≤ X₀ ∧ 2+X₀ ≤ 0 ∧ 10+X₀+X₁ ≤ 0 ∧ 10 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 10+X₀+X₁ ∧ X₁ ≤ 10 ∧ 2 ≤ X₀ ∧ 2+X₀ ≤ 0 ∧ 10+X₀+X₁ ≤ 0 ∧ 10 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 10+X₀+X₁ ∧ X₁ ≤ 9 ∧ 0 ≤ 1+X₀ ∧ X₀ ≤ 1 ∧ 1 ≤ X₀ ∧ 1+X₀ ≤ 0 ∧ 10+X₀+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 10+X₀+X₁ ∧ X₁ ≤ 9 ∧ 0 ≤ 1+X₀ ∧ 1+X₀ ≤ 0 ∧ 2 ≤ X₀ ∧ 10+X₀+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 10+X₀+X₁ ∧ X₁ ≤ 9 ∧ X₀ ≤ 1 ∧ 1 ≤ X₀ ∧ 2+X₀ ≤ 0 ∧ 10+X₀+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 10+X₀+X₁ ∧ X₁ ≤ 9 ∧ 2 ≤ X₀ ∧ 2+X₀ ≤ 0 ∧ 10+X₀+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 10+X₀+X₁ ∧ 0 ≤ 1+X₀ ∧ X₀ ≤ 1 ∧ 1 ≤ X₀ ∧ 1+X₀ ≤ 0 ∧ 1+2⋅X₀ ≤ 0 ∧ 10+X₀+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 10+X₀+X₁ ∧ 0 ≤ 1+X₀ ∧ 1+X₀ ≤ 0 ∧ 1+2⋅X₀ ≤ 0 ∧ 2 ≤ X₀ ∧ 10+X₀+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 10+X₀+X₁ ∧ X₀ ≤ 1 ∧ 1 ≤ X₀ ∧ 1+2⋅X₀ ≤ 0 ∧ 2+X₀ ≤ 0 ∧ 10+X₀+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 10+X₀+X₁ ∧ 1+2⋅X₀ ≤ 0 ∧ 2 ≤ X₀ ∧ 2+X₀ ≤ 0 ∧ 10+X₀+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ X₁ ≤ 10 ∧ 0 ≤ 9+X₀+X₁ ∧ 0 ≤ 1+X₀ ∧ X₀ ≤ 1 ∧ 1 ≤ X₀ ∧ 1+X₀ ≤ 0 ∧ 10 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ X₁ ≤ 10 ∧ 0 ≤ 9+X₀+X₁ ∧ 0 ≤ 1+X₀ ∧ 1+X₀ ≤ 0 ∧ 2 ≤ X₀ ∧ 10 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ X₁ ≤ 10 ∧ 0 ≤ 9+X₀+X₁ ∧ X₀ ≤ 1 ∧ 1 ≤ X₀ ∧ 2+X₀ ≤ 0 ∧ 10 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ X₁ ≤ 10 ∧ 0 ≤ 9+X₀+X₁ ∧ 2 ≤ X₀ ∧ 2+X₀ ≤ 0 ∧ 10 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ X₁ ≤ 10 ∧ 0 ≤ 1+X₀ ∧ X₀ ≤ 1 ∧ 1 ≤ 2⋅X₀ ∧ 1 ≤ X₀ ∧ 1+X₀ ≤ 0 ∧ 10 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ X₁ ≤ 10 ∧ 0 ≤ 1+X₀ ∧ 1 ≤ 2⋅X₀ ∧ 1+X₀ ≤ 0 ∧ 2 ≤ X₀ ∧ 10 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ X₁ ≤ 10 ∧ X₀ ≤ 1 ∧ 1 ≤ 2⋅X₀ ∧ 1 ≤ X₀ ∧ 2+X₀ ≤ 0 ∧ 10 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ X₁ ≤ 10 ∧ 1 ≤ 2⋅X₀ ∧ 2 ≤ X₀ ∧ 2+X₀ ≤ 0 ∧ 10 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 9+X₀+X₁ ∧ X₁ ≤ 9 ∧ 0 ≤ 1+X₀ ∧ X₀ ≤ 1 ∧ 1 ≤ X₀ ∧ 1+X₀ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 9+X₀+X₁ ∧ X₁ ≤ 9 ∧ 0 ≤ 1+X₀ ∧ 1+X₀ ≤ 0 ∧ 2 ≤ X₀ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 9+X₀+X₁ ∧ X₁ ≤ 9 ∧ X₀ ≤ 1 ∧ 1 ≤ X₀ ∧ 2+X₀ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 9+X₀+X₁ ∧ X₁ ≤ 9 ∧ 2 ≤ X₀ ∧ 2+X₀ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 9+X₀+X₁ ∧ 0 ≤ 1+X₀ ∧ X₀ ≤ 1 ∧ 1 ≤ X₀ ∧ 1+X₀ ≤ 0 ∧ 1+2⋅X₀ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 9+X₀+X₁ ∧ 0 ≤ 1+X₀ ∧ 1+X₀ ≤ 0 ∧ 1+2⋅X₀ ≤ 0 ∧ 2 ≤ X₀ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 9+X₀+X₁ ∧ X₀ ≤ 1 ∧ 1 ≤ X₀ ∧ 1+2⋅X₀ ≤ 0 ∧ 2+X₀ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 9+X₀+X₁ ∧ 1+2⋅X₀ ≤ 0 ∧ 2 ≤ X₀ ∧ 2+X₀ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ X₁ ≤ 9 ∧ 0 ≤ 1+X₀ ∧ X₀ ≤ 1 ∧ 1 ≤ 2⋅X₀ ∧ 1 ≤ X₀ ∧ 1+X₀ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ X₁ ≤ 9 ∧ 0 ≤ 1+X₀ ∧ 1 ≤ 2⋅X₀ ∧ 1+X₀ ≤ 0 ∧ 2 ≤ X₀ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ X₁ ≤ 9 ∧ X₀ ≤ 1 ∧ 1 ≤ 2⋅X₀ ∧ 1 ≤ X₀ ∧ 2+X₀ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ X₁ ≤ 9 ∧ 1 ≤ 2⋅X₀ ∧ 2 ≤ X₀ ∧ 2+X₀ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 1+X₀ ∧ X₀ ≤ 1 ∧ 1 ≤ 2⋅X₀ ∧ 1 ≤ X₀ ∧ 1+X₀ ≤ 0 ∧ 1+2⋅X₀ ≤ 0
∨ 0 ≤ 1+X₀ ∧ 1 ≤ 2⋅X₀ ∧ 1+X₀ ≤ 0 ∧ 1+2⋅X₀ ≤ 0 ∧ 2 ≤ X₀
∨ X₀ ≤ 1 ∧ 1 ≤ 2⋅X₀ ∧ 1 ≤ X₀ ∧ 1+2⋅X₀ ≤ 0 ∧ 2+X₀ ≤ 0
∨ 1 ≤ 2⋅X₀ ∧ 1+2⋅X₀ ≤ 0 ∧ 2 ≤ X₀ ∧ 2+X₀ ≤ 0
∨ 0 ≤ 10+X₀+X₁ ∧ X₁ ≤ 10 ∧ X₀ ≤ 1 ∧ 1 ≤ X₀ ∧ 10+X₀+X₁ ≤ 0 ∧ 10 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 10+X₀+X₁ ∧ X₁ ≤ 10 ∧ 2 ≤ X₀ ∧ 10+X₀+X₁ ≤ 0 ∧ 10 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 10+X₀+X₁ ∧ X₁ ≤ 9 ∧ X₀ ≤ 1 ∧ 1 ≤ X₀ ∧ 10+X₀+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 10+X₀+X₁ ∧ X₁ ≤ 9 ∧ 2 ≤ X₀ ∧ 10+X₀+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 10+X₀+X₁ ∧ X₀ ≤ 1 ∧ 1 ≤ X₀ ∧ 1+2⋅X₀ ≤ 0 ∧ 10+X₀+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 10+X₀+X₁ ∧ 1+2⋅X₀ ≤ 0 ∧ 2 ≤ X₀ ∧ 10+X₀+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ X₁ ≤ 10 ∧ 0 ≤ 9+X₀+X₁ ∧ X₀ ≤ 1 ∧ 1 ≤ X₀ ∧ 10 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ X₁ ≤ 10 ∧ 0 ≤ 9+X₀+X₁ ∧ 2 ≤ X₀ ∧ 10 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ X₁ ≤ 10 ∧ X₀ ≤ 1 ∧ 1 ≤ 2⋅X₀ ∧ 1 ≤ X₀ ∧ 10 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ X₁ ≤ 10 ∧ 1 ≤ 2⋅X₀ ∧ 2 ≤ X₀ ∧ 10 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 9+X₀+X₁ ∧ X₁ ≤ 9 ∧ X₀ ≤ 1 ∧ 1 ≤ X₀ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 9+X₀+X₁ ∧ X₁ ≤ 9 ∧ 2 ≤ X₀ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 9+X₀+X₁ ∧ X₀ ≤ 1 ∧ 1 ≤ X₀ ∧ 1+2⋅X₀ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 9+X₀+X₁ ∧ 1+2⋅X₀ ≤ 0 ∧ 2 ≤ X₀ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ X₁ ≤ 9 ∧ X₀ ≤ 1 ∧ 1 ≤ 2⋅X₀ ∧ 1 ≤ X₀ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ X₁ ≤ 9 ∧ 1 ≤ 2⋅X₀ ∧ 2 ≤ X₀ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ X₀ ≤ 1 ∧ 1 ≤ 2⋅X₀ ∧ 1 ≤ X₀ ∧ 1+2⋅X₀ ≤ 0
∨ 1 ≤ 2⋅X₀ ∧ 1+2⋅X₀ ≤ 0 ∧ 2 ≤ X₀
∨ 0 ≤ 10+X₀+X₁ ∧ X₁ ≤ 10 ∧ 0 ≤ 1+X₀ ∧ 1+X₀ ≤ 0 ∧ 10+X₀+X₁ ≤ 0 ∧ 10 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 10+X₀+X₁ ∧ X₁ ≤ 10 ∧ 2+X₀ ≤ 0 ∧ 10+X₀+X₁ ≤ 0 ∧ 10 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 10+X₀+X₁ ∧ X₁ ≤ 9 ∧ 0 ≤ 1+X₀ ∧ 1+X₀ ≤ 0 ∧ 10+X₀+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 10+X₀+X₁ ∧ X₁ ≤ 9 ∧ 2+X₀ ≤ 0 ∧ 10+X₀+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 10+X₀+X₁ ∧ 0 ≤ 1+X₀ ∧ 1+X₀ ≤ 0 ∧ 1+2⋅X₀ ≤ 0 ∧ 10+X₀+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 10+X₀+X₁ ∧ 1+2⋅X₀ ≤ 0 ∧ 2+X₀ ≤ 0 ∧ 10+X₀+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ X₁ ≤ 10 ∧ 0 ≤ 9+X₀+X₁ ∧ 0 ≤ 1+X₀ ∧ 1+X₀ ≤ 0 ∧ 10 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ X₁ ≤ 10 ∧ 0 ≤ 9+X₀+X₁ ∧ 2+X₀ ≤ 0 ∧ 10 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ X₁ ≤ 10 ∧ 0 ≤ 1+X₀ ∧ 1 ≤ 2⋅X₀ ∧ 1+X₀ ≤ 0 ∧ 10 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ X₁ ≤ 10 ∧ 1 ≤ 2⋅X₀ ∧ 2+X₀ ≤ 0 ∧ 10 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 9+X₀+X₁ ∧ X₁ ≤ 9 ∧ 0 ≤ 1+X₀ ∧ 1+X₀ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 9+X₀+X₁ ∧ X₁ ≤ 9 ∧ 2+X₀ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 9+X₀+X₁ ∧ 0 ≤ 1+X₀ ∧ 1+X₀ ≤ 0 ∧ 1+2⋅X₀ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 9+X₀+X₁ ∧ 1+2⋅X₀ ≤ 0 ∧ 2+X₀ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ X₁ ≤ 9 ∧ 0 ≤ 1+X₀ ∧ 1 ≤ 2⋅X₀ ∧ 1+X₀ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ X₁ ≤ 9 ∧ 1 ≤ 2⋅X₀ ∧ 2+X₀ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 1+X₀ ∧ 1 ≤ 2⋅X₀ ∧ 1+X₀ ≤ 0 ∧ 1+2⋅X₀ ≤ 0
∨ 1 ≤ 2⋅X₀ ∧ 1+2⋅X₀ ≤ 0 ∧ 2+X₀ ≤ 0
∨ 0 ≤ 10+X₀+X₁ ∧ X₁ ≤ 10 ∧ 0 ≤ 1+X₀ ∧ X₀ ≤ 1 ∧ 1 ≤ X₀ ∧ 1+X₀ ≤ 0 ∧ 10+X₀+X₁ ≤ 0 ∧ 10 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 10+X₀+X₁ ∧ X₁ ≤ 10 ∧ 0 ≤ 1+X₀ ∧ 1+X₀ ≤ 0 ∧ 2 ≤ X₀ ∧ 10+X₀+X₁ ≤ 0 ∧ 10 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 10+X₀+X₁ ∧ X₁ ≤ 10 ∧ X₀ ≤ 1 ∧ 1 ≤ X₀ ∧ 2+X₀ ≤ 0 ∧ 10+X₀+X₁ ≤ 0 ∧ 10 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 10+X₀+X₁ ∧ X₁ ≤ 10 ∧ 2 ≤ X₀ ∧ 2+X₀ ≤ 0 ∧ 10+X₀+X₁ ≤ 0 ∧ 10 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 10+X₀+X₁ ∧ X₁ ≤ 9 ∧ 0 ≤ 1+X₀ ∧ X₀ ≤ 1 ∧ 1 ≤ X₀ ∧ 1+X₀ ≤ 0 ∧ 10+X₀+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 10+X₀+X₁ ∧ X₁ ≤ 9 ∧ 0 ≤ 1+X₀ ∧ 1+X₀ ≤ 0 ∧ 2 ≤ X₀ ∧ 10+X₀+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 10+X₀+X₁ ∧ X₁ ≤ 9 ∧ X₀ ≤ 1 ∧ 1 ≤ X₀ ∧ 2+X₀ ≤ 0 ∧ 10+X₀+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 10+X₀+X₁ ∧ X₁ ≤ 9 ∧ 2 ≤ X₀ ∧ 2+X₀ ≤ 0 ∧ 10+X₀+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 10+X₀+X₁ ∧ 0 ≤ 1+X₀ ∧ X₀ ≤ 1 ∧ 1 ≤ X₀ ∧ 1+X₀ ≤ 0 ∧ 1+2⋅X₀ ≤ 0 ∧ 10+X₀+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 10+X₀+X₁ ∧ 0 ≤ 1+X₀ ∧ 1+X₀ ≤ 0 ∧ 1+2⋅X₀ ≤ 0 ∧ 2 ≤ X₀ ∧ 10+X₀+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 10+X₀+X₁ ∧ X₀ ≤ 1 ∧ 1 ≤ X₀ ∧ 1+2⋅X₀ ≤ 0 ∧ 2+X₀ ≤ 0 ∧ 10+X₀+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 10+X₀+X₁ ∧ 1+2⋅X₀ ≤ 0 ∧ 2 ≤ X₀ ∧ 2+X₀ ≤ 0 ∧ 10+X₀+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ X₁ ≤ 10 ∧ 0 ≤ 9+X₀+X₁ ∧ 0 ≤ 1+X₀ ∧ X₀ ≤ 1 ∧ 1 ≤ X₀ ∧ 1+X₀ ≤ 0 ∧ 10 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ X₁ ≤ 10 ∧ 0 ≤ 9+X₀+X₁ ∧ 0 ≤ 1+X₀ ∧ 1+X₀ ≤ 0 ∧ 2 ≤ X₀ ∧ 10 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ X₁ ≤ 10 ∧ 0 ≤ 9+X₀+X₁ ∧ X₀ ≤ 1 ∧ 1 ≤ X₀ ∧ 2+X₀ ≤ 0 ∧ 10 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ X₁ ≤ 10 ∧ 0 ≤ 9+X₀+X₁ ∧ 2 ≤ X₀ ∧ 2+X₀ ≤ 0 ∧ 10 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ X₁ ≤ 10 ∧ 0 ≤ 1+X₀ ∧ X₀ ≤ 1 ∧ 1 ≤ 2⋅X₀ ∧ 1 ≤ X₀ ∧ 1+X₀ ≤ 0 ∧ 10 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ X₁ ≤ 10 ∧ 0 ≤ 1+X₀ ∧ 1 ≤ 2⋅X₀ ∧ 1+X₀ ≤ 0 ∧ 2 ≤ X₀ ∧ 10 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ X₁ ≤ 10 ∧ X₀ ≤ 1 ∧ 1 ≤ 2⋅X₀ ∧ 1 ≤ X₀ ∧ 2+X₀ ≤ 0 ∧ 10 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ X₁ ≤ 10 ∧ 1 ≤ 2⋅X₀ ∧ 2 ≤ X₀ ∧ 2+X₀ ≤ 0 ∧ 10 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 9+X₀+X₁ ∧ X₁ ≤ 9 ∧ 0 ≤ 1+X₀ ∧ X₀ ≤ 1 ∧ 1 ≤ X₀ ∧ 1+X₀ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 9+X₀+X₁ ∧ X₁ ≤ 9 ∧ 0 ≤ 1+X₀ ∧ 1+X₀ ≤ 0 ∧ 2 ≤ X₀ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 9+X₀+X₁ ∧ X₁ ≤ 9 ∧ X₀ ≤ 1 ∧ 1 ≤ X₀ ∧ 2+X₀ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 9+X₀+X₁ ∧ X₁ ≤ 9 ∧ 2 ≤ X₀ ∧ 2+X₀ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 9+X₀+X₁ ∧ 0 ≤ 1+X₀ ∧ X₀ ≤ 1 ∧ 1 ≤ X₀ ∧ 1+X₀ ≤ 0 ∧ 1+2⋅X₀ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 9+X₀+X₁ ∧ 0 ≤ 1+X₀ ∧ 1+X₀ ≤ 0 ∧ 1+2⋅X₀ ≤ 0 ∧ 2 ≤ X₀ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 9+X₀+X₁ ∧ X₀ ≤ 1 ∧ 1 ≤ X₀ ∧ 1+2⋅X₀ ≤ 0 ∧ 2+X₀ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 9+X₀+X₁ ∧ 1+2⋅X₀ ≤ 0 ∧ 2 ≤ X₀ ∧ 2+X₀ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ X₁ ≤ 9 ∧ 0 ≤ 1+X₀ ∧ X₀ ≤ 1 ∧ 1 ≤ 2⋅X₀ ∧ 1 ≤ X₀ ∧ 1+X₀ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ X₁ ≤ 9 ∧ 0 ≤ 1+X₀ ∧ 1 ≤ 2⋅X₀ ∧ 1+X₀ ≤ 0 ∧ 2 ≤ X₀ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ X₁ ≤ 9 ∧ X₀ ≤ 1 ∧ 1 ≤ 2⋅X₀ ∧ 1 ≤ X₀ ∧ 2+X₀ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ X₁ ≤ 9 ∧ 1 ≤ 2⋅X₀ ∧ 2 ≤ X₀ ∧ 2+X₀ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 1+X₀ ∧ X₀ ≤ 1 ∧ 1 ≤ 2⋅X₀ ∧ 1 ≤ X₀ ∧ 1+X₀ ≤ 0 ∧ 1+2⋅X₀ ≤ 0
∨ 0 ≤ 1+X₀ ∧ 1 ≤ 2⋅X₀ ∧ 1+X₀ ≤ 0 ∧ 1+2⋅X₀ ≤ 0 ∧ 2 ≤ X₀
∨ X₀ ≤ 1 ∧ 1 ≤ 2⋅X₀ ∧ 1 ≤ X₀ ∧ 1+2⋅X₀ ≤ 0 ∧ 2+X₀ ≤ 0
∨ 1 ≤ 2⋅X₀ ∧ 1+2⋅X₀ ≤ 0 ∧ 2 ≤ X₀ ∧ 2+X₀ ≤ 0

Stabilization-Threshold for: 0 ≤ 10+X₀+X₁
alphas_abs: 11+X₀+X₁
M: 0
N: 1
Bound: 2⋅X₀+2⋅X₁+24 {O(n)}
Stabilization-Threshold for: X₁ ≤ 10
alphas_abs: 11+X₁
M: 0
N: 1
Bound: 2⋅X₁+24 {O(n)}

TWN - Lifting for [3: l1->l1; 5: l1->l1] of 4⋅X₀+8⋅X₁+105 {O(n)}

relevant size-bounds w.r.t. t₁: l0→l1:
X₀: 1 {O(1)}
X₁: X₁ {O(n)}
Runtime-bound of t₁: 1 {O(1)}
Results in: 8⋅X₁+109 {O(n)}

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:16⋅X₁+219 {O(n)}
g₀: 1 {O(1)}
g₂: 8⋅X₁+109 {O(n)}
g₄: 8⋅X₁+109 {O(n)}

Costbounds

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

Sizebounds

(g₀,l1), X₀: 1 {O(1)}
(g₀,l1), X₁: X₁ {O(n)}
(g₂,l1), X₀: 1 {O(1)}
(g₂,l1), X₁: 17⋅X₁+218 {O(n)}
(g₄,l1), X₀: 1 {O(1)}
(g₄,l1), X₁: 17⋅X₁+218 {O(n)}

Run probabilistic analysis on SCC: [l1]

Results of Probabilistic Analysis

All Bounds

Timebounds

Overall timebound:16⋅X₁+219 {O(n)}
g₀: 1 {O(1)}
g₂: 8⋅X₁+109 {O(n)}
g₄: 8⋅X₁+109 {O(n)}

Costbounds

Overall costbound: 16⋅X₁+219 {O(n)}
g₀: 1 {O(1)}
g₂: 8⋅X₁+109 {O(n)}
g₄: 8⋅X₁+109 {O(n)}

Sizebounds

(g₀,l1), X₀: 1 {O(1)}
(g₀,l1), X₁: X₁ {O(n)}
(g₂,l1), X₀: 1 {O(1)}
(g₂,l1), X₁: 17⋅X₁+218 {O(n)}
(g₄,l1), X₀: 1 {O(1)}
(g₄,l1), X₁: 17⋅X₁+218 {O(n)}