Preprocessing

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

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

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

Found invariant 1 ≤ 0 for location ac

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

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

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

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

Cut unsatisfiable transition [t₁₂∈g₁₁: ac→1/3:ac; t₁₃∈g₁₁: ac→2/3:ac; t₁₅∈g₁₄: ac→1:ac_end; t₂₈∈g₂₇: ab_end→1:ac]

Cut unreachable locations [ac] from the program graph

Probabilistic Analysis

Probabilistic Program after Preprocessing

Start: f
Program_Vars: X₀, X₁, X₂
Temp_Vars:
Locations: ab, ab_end, abc, abc_end, ac_end, bc, bc_end, f
Transitions:
g₀:abc(X₀,X₁,X₂) → [1/6]:t₁:abc_end(X₀,0,0) :+: [1/6]:t₂:abc_end(0,0,0) :+: [1/3]:t₃:abc_end(X₀,0,0) :+: [1/3]:t₄:abc_end(0,0,X₂) :|: X₀+X₁ ≤ 2 ∧ X₀+X₂ ≤ 2 ∧ X₁+X₂ ≤ 2 ∧ X₀ ≤ 1 ∧ X₁ ≤ 1 ∧ X₂ ≤ 1 ∧ 1 ≤ X₀ ∧ 1 ≤ X₁ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₁ ∧ 2 ≤ X₀+X₂ ∧ 2 ≤ X₁+X₂ ∧ X₁ ≤ X₀ ∧ X₂ ≤ X₀ ∧ X₀ ≤ X₁ ∧ X₀ ≤ X₂ ∧ X₂ ≤ X₁ ∧ X₁ ≤ X₂
g₅:ab(X₀,X₁,X₂) → [1/3]:t₆:ab(0,X₁,X₂) :+: [1/3]:t₇:ab(0,X₁,X₂) :+: [1/3]:t₈:ab(1,X₁,X₂) :|: 1 ≤ X₀ ∧ X₀ ≤ 1 ∧ X₀ ≤ 1+X₁ ∧ X₀+X₁ ≤ 1 ∧ X₀ ≤ 1+X₂ ∧ X₀+X₂ ≤ 1 ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₁ ∧ X₁ ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₂ ≤ X₀ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₂ ∧ X₂ ≤ X₁ ∧ X₁ ≤ 0 ∧ X₁ ≤ X₂ ∧ X₁+X₂ ≤ 0 ∧ 0 ≤ X₂ ∧ X₂ ≤ 0
g₉:ab(X₀,X₁,X₂) -{0}> t₁₀:ab_end(X₀,X₁,X₂) :|: X₀ ≤ 0 ∧ X₀ ≤ 1 ∧ X₀ ≤ 1+X₁ ∧ X₀+X₁ ≤ 1 ∧ X₀ ≤ 1+X₂ ∧ X₀+X₂ ≤ 1 ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₁ ∧ X₁ ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₂ ≤ X₀ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₂ ∧ X₂ ≤ X₁ ∧ X₁ ≤ 0 ∧ X₁ ≤ X₂ ∧ X₁+X₂ ≤ 0 ∧ 0 ≤ X₂ ∧ X₂ ≤ 0
g₁₆:bc(X₀,X₁,X₂) → [1/2]:t₁₇:bc(X₀,X₁,0) :+: [1/2]:t₁₈:bc(X₀,X₁,0) :|: 1 ≤ X₂ ∧ X₂ ≤ 1+X₀ ∧ X₀+X₂ ≤ 1 ∧ X₂ ≤ 1+X₁ ∧ X₁+X₂ ≤ 1 ∧ X₂ ≤ 1 ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₁ ∧ X₁ ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ 0 ∧ X₀ ≤ X₁ ∧ X₀+X₁ ≤ 0 ∧ X₀ ≤ X₂ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₂ ∧ X₁ ≤ 0 ∧ X₁ ≤ X₂ ∧ 0 ≤ X₂
g₁₉:bc(X₀,X₁,X₂) -{0}> t₂₀:bc_end(X₀,X₁,X₂) :|: X₂ ≤ 0 ∧ X₂ ≤ 1+X₀ ∧ X₀+X₂ ≤ 1 ∧ X₂ ≤ 1+X₁ ∧ X₁+X₂ ≤ 1 ∧ X₂ ≤ 1 ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₁ ∧ X₁ ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ 0 ∧ X₀ ≤ X₁ ∧ X₀+X₁ ≤ 0 ∧ X₀ ≤ X₂ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₂ ∧ X₁ ≤ 0 ∧ X₁ ≤ X₂ ∧ 0 ≤ X₂
g₂₁:f(X₀,X₁,X₂) -{0}> t₂₂:abc(1,1,1) :|:
g₂₃:abc_end(X₀,X₁,X₂) -{0}> t₂₄:ab(X₀,X₁,X₂) :|: X₀ ≤ 1 ∧ 1 ≤ X₀ ∧ X₂ ≤ 1+X₀ ∧ X₀ ≤ 1+X₁ ∧ X₀+X₁ ≤ 1 ∧ X₀ ≤ 1+X₂ ∧ X₀+X₂ ≤ 1 ∧ X₂ ≤ 1+X₁ ∧ X₁+X₂ ≤ 1 ∧ X₂ ≤ 1 ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₁ ∧ X₁ ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₂ ∧ X₁ ≤ 0 ∧ X₁ ≤ X₂ ∧ 0 ≤ X₂
g₂₅:abc_end(X₀,X₁,X₂) -{0}> t₂₆:ab_end(X₀,X₁,X₂) :|: 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ X₂ ≤ 1+X₀ ∧ X₀ ≤ 1 ∧ X₀ ≤ 1+X₁ ∧ X₀+X₁ ≤ 1 ∧ X₀ ≤ 1+X₂ ∧ X₀+X₂ ≤ 1 ∧ X₂ ≤ 1+X₁ ∧ X₁+X₂ ≤ 1 ∧ X₂ ≤ 1 ∧ 0 ≤ X₀+X₁ ∧ X₁ ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₂ ∧ X₁ ≤ 0 ∧ X₁ ≤ X₂ ∧ 0 ≤ X₂
g₂₉:ab_end(X₀,X₁,X₂) -{0}> t₃₀:ac_end(X₀,X₁,X₂) :|: 0 ≤ X₁ ∧ X₁ ≤ 0 ∧ X₂ ≤ 1+X₀ ∧ X₀+X₂ ≤ 1 ∧ X₂ ≤ 1+X₁ ∧ X₁+X₂ ≤ 1 ∧ X₂ ≤ 1 ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₁ ∧ X₁ ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ 0 ∧ X₀ ≤ X₁ ∧ X₀+X₁ ≤ 0 ∧ X₀ ≤ X₂ ∧ 0 ≤ X₁+X₂ ∧ X₁ ≤ X₂ ∧ 0 ≤ X₂
g₃₁:ac_end(X₀,X₁,X₂) -{0}> t₃₂:bc(X₀,X₁,X₂) :|: X₂ ≤ 1 ∧ 1 ≤ X₂ ∧ X₂ ≤ 1+X₀ ∧ X₀+X₂ ≤ 1 ∧ X₂ ≤ 1+X₁ ∧ X₁+X₂ ≤ 1 ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₁ ∧ X₁ ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ 0 ∧ X₀ ≤ X₁ ∧ X₀+X₁ ≤ 0 ∧ X₀ ≤ X₂ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₂ ∧ X₁ ≤ 0 ∧ X₁ ≤ X₂ ∧ 0 ≤ X₂
g₃₃:ac_end(X₀,X₁,X₂) -{0}> t₃₄:bc_end(X₀,X₁,X₂) :|: 0 ≤ X₂ ∧ X₂ ≤ 0 ∧ X₂ ≤ 1+X₀ ∧ X₀+X₂ ≤ 1 ∧ X₂ ≤ 1+X₁ ∧ X₁+X₂ ≤ 1 ∧ X₂ ≤ 1 ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₁ ∧ X₁ ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ 0 ∧ X₀ ≤ X₁ ∧ X₀+X₁ ≤ 0 ∧ X₀ ≤ X₂ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₂ ∧ X₁ ≤ 0 ∧ 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₉: 1 {O(1)}
g₁₆: inf {Infinity}
g₁₉: 1 {O(1)}
g₂₁: 1 {O(1)}
g₂₃: 1 {O(1)}
g₂₅: 1 {O(1)}
g₂₉: 1 {O(1)}
g₃₁: 1 {O(1)}
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}
g₂₅: inf {Infinity}
g₂₉: inf {Infinity}
g₃₁: inf {Infinity}
g₃₃: inf {Infinity}

Sizebounds

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

Run probabilistic analysis on SCC: [f]

Run classical analysis on SCC: [abc]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:inf {Infinity}
g₀: 4 {O(1)}
g₅: inf {Infinity}
g₉: 1 {O(1)}
g₁₆: inf {Infinity}
g₁₉: 1 {O(1)}
g₂₁: 1 {O(1)}
g₂₃: 1 {O(1)}
g₂₅: 1 {O(1)}
g₂₉: 1 {O(1)}
g₃₁: 1 {O(1)}
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}
g₂₅: inf {Infinity}
g₂₉: inf {Infinity}
g₃₁: inf {Infinity}
g₃₃: inf {Infinity}

Sizebounds

(g₀,abc_end), X₀: 2 {O(1)}
(g₀,abc_end), X₁: 0 {O(1)}
(g₀,abc_end), X₂: 1 {O(1)}
(g₂₁,abc), X₀: 1 {O(1)}
(g₂₁,abc), X₁: 1 {O(1)}
(g₂₁,abc), X₂: 1 {O(1)}

Run probabilistic analysis on SCC: [abc]

Run classical analysis on SCC: [abc_end]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:inf {Infinity}
g₀: 4 {O(1)}
g₅: inf {Infinity}
g₉: 1 {O(1)}
g₁₆: inf {Infinity}
g₁₉: 1 {O(1)}
g₂₁: 1 {O(1)}
g₂₃: 1 {O(1)}
g₂₅: 1 {O(1)}
g₂₉: 1 {O(1)}
g₃₁: 1 {O(1)}
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}
g₂₅: inf {Infinity}
g₂₉: inf {Infinity}
g₃₁: inf {Infinity}
g₃₃: inf {Infinity}

Sizebounds

(g₀,abc_end), X₀: 2 {O(1)}
(g₀,abc_end), X₁: 0 {O(1)}
(g₀,abc_end), X₂: 1 {O(1)}
(g₂₁,abc), X₀: 1 {O(1)}
(g₂₁,abc), X₁: 1 {O(1)}
(g₂₁,abc), X₂: 1 {O(1)}
(g₂₃,ab), X₀: 1 {O(1)}
(g₂₃,ab), X₁: 0 {O(1)}
(g₂₃,ab), X₂: 0 {O(1)}
(g₂₅,ab_end), X₀: 0 {O(1)}
(g₂₅,ab_end), X₁: 0 {O(1)}
(g₂₅,ab_end), X₂: 1 {O(1)}

Run probabilistic analysis on SCC: [abc_end]

Run classical analysis on SCC: [ab]

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

new bound:

2 {O(1)}

MPRF:

• ab: [1+X₀]

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

new bound:

2 {O(1)}

MPRF:

• ab: [1+X₀]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:inf {Infinity}
g₀: 4 {O(1)}
g₅: inf {Infinity}
g₉: 1 {O(1)}
g₁₆: inf {Infinity}
g₁₉: 1 {O(1)}
g₂₁: 1 {O(1)}
g₂₃: 1 {O(1)}
g₂₅: 1 {O(1)}
g₂₉: 1 {O(1)}
g₃₁: 1 {O(1)}
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}
g₂₅: inf {Infinity}
g₂₉: inf {Infinity}
g₃₁: inf {Infinity}
g₃₃: inf {Infinity}

Sizebounds

(g₀,abc_end), X₀: 2 {O(1)}
(g₀,abc_end), X₁: 0 {O(1)}
(g₀,abc_end), X₂: 1 {O(1)}
(g₅,ab), X₀: 1 {O(1)}
(g₅,ab), X₁: 0 {O(1)}
(g₅,ab), X₂: 0 {O(1)}
(g₉,ab_end), X₀: 0 {O(1)}
(g₉,ab_end), X₁: 0 {O(1)}
(g₉,ab_end), X₂: 0 {O(1)}
(g₂₁,abc), X₀: 1 {O(1)}
(g₂₁,abc), X₁: 1 {O(1)}
(g₂₁,abc), X₂: 1 {O(1)}
(g₂₃,ab), X₀: 1 {O(1)}
(g₂₃,ab), X₁: 0 {O(1)}
(g₂₃,ab), X₂: 0 {O(1)}
(g₂₅,ab_end), X₀: 0 {O(1)}
(g₂₅,ab_end), X₁: 0 {O(1)}
(g₂₅,ab_end), X₂: 1 {O(1)}

Run probabilistic analysis on SCC: [ab]

Plrf for transition g₅:ab(X₀,X₁,X₂) → [1/3]:t₆:ab(0,X₁,X₂) :+: [1/3]:t₇:ab(0,X₁,X₂) :+: [1/3]:t₈:ab(1,X₁,X₂) :|: 1 ≤ X₀ ∧ X₀ ≤ 1 ∧ X₀ ≤ 1+X₁ ∧ X₀+X₁ ≤ 1 ∧ X₀ ≤ 1+X₂ ∧ X₀+X₂ ≤ 1 ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₁ ∧ X₁ ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₂ ≤ X₀ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₂ ∧ X₂ ≤ X₁ ∧ X₁ ≤ 0 ∧ X₁ ≤ X₂ ∧ X₁+X₂ ≤ 0 ∧ 0 ≤ X₂ ∧ X₂ ≤ 0:

new bound:

3/2 {O(1)}

PLRF:

• ab: 3/2⋅X₀

Use expected size bounds for entry point (g₂₃:abc_end→[t₂₄:1:ab],ab)
Use classical time bound for entry point (g₂₃:abc_end→[t₂₄:1:ab],ab)

Run classical analysis on SCC: [ab_end]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:inf {Infinity}
g₀: 4 {O(1)}
g₅: 3/2 {O(1)}
g₉: 1 {O(1)}
g₁₆: inf {Infinity}
g₁₉: 1 {O(1)}
g₂₁: 1 {O(1)}
g₂₃: 1 {O(1)}
g₂₅: 1 {O(1)}
g₂₉: 1 {O(1)}
g₃₁: 1 {O(1)}
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}
g₂₅: inf {Infinity}
g₂₉: inf {Infinity}
g₃₁: inf {Infinity}
g₃₃: inf {Infinity}

Sizebounds

(g₀,abc_end), X₀: 2 {O(1)}
(g₀,abc_end), X₁: 0 {O(1)}
(g₀,abc_end), X₂: 1 {O(1)}
(g₅,ab), X₀: 1 {O(1)}
(g₅,ab), X₁: 0 {O(1)}
(g₅,ab), X₂: 0 {O(1)}
(g₉,ab_end), X₀: 0 {O(1)}
(g₉,ab_end), X₁: 0 {O(1)}
(g₉,ab_end), X₂: 0 {O(1)}
(g₂₁,abc), X₀: 1 {O(1)}
(g₂₁,abc), X₁: 1 {O(1)}
(g₂₁,abc), X₂: 1 {O(1)}
(g₂₃,ab), X₀: 1 {O(1)}
(g₂₃,ab), X₁: 0 {O(1)}
(g₂₃,ab), X₂: 0 {O(1)}
(g₂₅,ab_end), X₀: 0 {O(1)}
(g₂₅,ab_end), X₁: 0 {O(1)}
(g₂₅,ab_end), X₂: 1 {O(1)}
(g₂₉,ac_end), X₀: 0 {O(1)}
(g₂₉,ac_end), X₁: 0 {O(1)}
(g₂₉,ac_end), X₂: 1 {O(1)}

Run probabilistic analysis on SCC: [ab_end]

Run classical analysis on SCC: [ac_end]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:inf {Infinity}
g₀: 4 {O(1)}
g₅: 3/2 {O(1)}
g₉: 1 {O(1)}
g₁₆: inf {Infinity}
g₁₉: 1 {O(1)}
g₂₁: 1 {O(1)}
g₂₃: 1 {O(1)}
g₂₅: 1 {O(1)}
g₂₉: 1 {O(1)}
g₃₁: 1 {O(1)}
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}
g₂₅: inf {Infinity}
g₂₉: inf {Infinity}
g₃₁: inf {Infinity}
g₃₃: inf {Infinity}

Sizebounds

(g₀,abc_end), X₀: 2 {O(1)}
(g₀,abc_end), X₁: 0 {O(1)}
(g₀,abc_end), X₂: 1 {O(1)}
(g₅,ab), X₀: 1 {O(1)}
(g₅,ab), X₁: 0 {O(1)}
(g₅,ab), X₂: 0 {O(1)}
(g₉,ab_end), X₀: 0 {O(1)}
(g₉,ab_end), X₁: 0 {O(1)}
(g₉,ab_end), X₂: 0 {O(1)}
(g₂₁,abc), X₀: 1 {O(1)}
(g₂₁,abc), X₁: 1 {O(1)}
(g₂₁,abc), X₂: 1 {O(1)}
(g₂₃,ab), X₀: 1 {O(1)}
(g₂₃,ab), X₁: 0 {O(1)}
(g₂₃,ab), X₂: 0 {O(1)}
(g₂₅,ab_end), X₀: 0 {O(1)}
(g₂₅,ab_end), X₁: 0 {O(1)}
(g₂₅,ab_end), X₂: 1 {O(1)}
(g₂₉,ac_end), X₀: 0 {O(1)}
(g₂₉,ac_end), X₁: 0 {O(1)}
(g₂₉,ac_end), X₂: 1 {O(1)}
(g₃₁,bc), X₀: 0 {O(1)}
(g₃₁,bc), X₁: 0 {O(1)}
(g₃₁,bc), X₂: 1 {O(1)}
(g₃₃,bc_end), X₀: 0 {O(1)}
(g₃₃,bc_end), X₁: 0 {O(1)}
(g₃₃,bc_end), X₂: 0 {O(1)}

Run probabilistic analysis on SCC: [ac_end]

Run classical analysis on SCC: [bc]

knowledge_propagation leads to new time bound 1 {O(1)} for transition t₁₇: bc(X₀,X₁,X₂) → bc(X₀,X₁,0) :|: X₂ ≤ 1+X₀ ∧ X₀+X₂ ≤ 1 ∧ X₂ ≤ 1+X₁ ∧ X₁+X₂ ≤ 1 ∧ X₂ ≤ 1 ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₁ ∧ X₁ ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ 0 ∧ X₀ ≤ X₁ ∧ X₀+X₁ ≤ 0 ∧ X₀ ≤ X₂ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₂ ∧ X₁ ≤ 0 ∧ X₁ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₂

knowledge_propagation leads to new time bound 1 {O(1)} for transition t₁₈: bc(X₀,X₁,X₂) → bc(X₀,X₁,0) :|: X₂ ≤ 1+X₀ ∧ X₀+X₂ ≤ 1 ∧ X₂ ≤ 1+X₁ ∧ X₁+X₂ ≤ 1 ∧ X₂ ≤ 1 ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₁ ∧ X₁ ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ 0 ∧ X₀ ≤ X₁ ∧ X₀+X₁ ≤ 0 ∧ X₀ ≤ X₂ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₂ ∧ X₁ ≤ 0 ∧ X₁ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₂

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:31/2 {O(1)}
g₀: 4 {O(1)}
g₅: 3/2 {O(1)}
g₉: 1 {O(1)}
g₁₆: 2 {O(1)}
g₁₉: 1 {O(1)}
g₂₁: 1 {O(1)}
g₂₃: 1 {O(1)}
g₂₅: 1 {O(1)}
g₂₉: 1 {O(1)}
g₃₁: 1 {O(1)}
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}
g₂₅: inf {Infinity}
g₂₉: inf {Infinity}
g₃₁: inf {Infinity}
g₃₃: inf {Infinity}

Sizebounds

(g₀,abc_end), X₀: 2 {O(1)}
(g₀,abc_end), X₁: 0 {O(1)}
(g₀,abc_end), X₂: 1 {O(1)}
(g₅,ab), X₀: 1 {O(1)}
(g₅,ab), X₁: 0 {O(1)}
(g₅,ab), X₂: 0 {O(1)}
(g₉,ab_end), X₀: 0 {O(1)}
(g₉,ab_end), X₁: 0 {O(1)}
(g₉,ab_end), X₂: 0 {O(1)}
(g₁₆,bc), X₀: 0 {O(1)}
(g₁₆,bc), X₁: 0 {O(1)}
(g₁₆,bc), X₂: 0 {O(1)}
(g₁₉,bc_end), X₀: 0 {O(1)}
(g₁₉,bc_end), X₁: 0 {O(1)}
(g₁₉,bc_end), X₂: 0 {O(1)}
(g₂₁,abc), X₀: 1 {O(1)}
(g₂₁,abc), X₁: 1 {O(1)}
(g₂₁,abc), X₂: 1 {O(1)}
(g₂₃,ab), X₀: 1 {O(1)}
(g₂₃,ab), X₁: 0 {O(1)}
(g₂₃,ab), X₂: 0 {O(1)}
(g₂₅,ab_end), X₀: 0 {O(1)}
(g₂₅,ab_end), X₁: 0 {O(1)}
(g₂₅,ab_end), X₂: 1 {O(1)}
(g₂₉,ac_end), X₀: 0 {O(1)}
(g₂₉,ac_end), X₁: 0 {O(1)}
(g₂₉,ac_end), X₂: 1 {O(1)}
(g₃₁,bc), X₀: 0 {O(1)}
(g₃₁,bc), X₁: 0 {O(1)}
(g₃₁,bc), X₂: 1 {O(1)}
(g₃₃,bc_end), X₀: 0 {O(1)}
(g₃₃,bc_end), X₁: 0 {O(1)}
(g₃₃,bc_end), X₂: 0 {O(1)}

Run probabilistic analysis on SCC: [bc]

Run classical analysis on SCC: [bc_end]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:31/2 {O(1)}
g₀: 4 {O(1)}
g₅: 3/2 {O(1)}
g₉: 1 {O(1)}
g₁₆: 2 {O(1)}
g₁₉: 1 {O(1)}
g₂₁: 1 {O(1)}
g₂₃: 1 {O(1)}
g₂₅: 1 {O(1)}
g₂₉: 1 {O(1)}
g₃₁: 1 {O(1)}
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}
g₂₅: inf {Infinity}
g₂₉: inf {Infinity}
g₃₁: inf {Infinity}
g₃₃: inf {Infinity}

Sizebounds

(g₀,abc_end), X₀: 2 {O(1)}
(g₀,abc_end), X₁: 0 {O(1)}
(g₀,abc_end), X₂: 1 {O(1)}
(g₅,ab), X₀: 1 {O(1)}
(g₅,ab), X₁: 0 {O(1)}
(g₅,ab), X₂: 0 {O(1)}
(g₉,ab_end), X₀: 0 {O(1)}
(g₉,ab_end), X₁: 0 {O(1)}
(g₉,ab_end), X₂: 0 {O(1)}
(g₁₆,bc), X₀: 0 {O(1)}
(g₁₆,bc), X₁: 0 {O(1)}
(g₁₆,bc), X₂: 0 {O(1)}
(g₁₉,bc_end), X₀: 0 {O(1)}
(g₁₉,bc_end), X₁: 0 {O(1)}
(g₁₉,bc_end), X₂: 0 {O(1)}
(g₂₁,abc), X₀: 1 {O(1)}
(g₂₁,abc), X₁: 1 {O(1)}
(g₂₁,abc), X₂: 1 {O(1)}
(g₂₃,ab), X₀: 1 {O(1)}
(g₂₃,ab), X₁: 0 {O(1)}
(g₂₃,ab), X₂: 0 {O(1)}
(g₂₅,ab_end), X₀: 0 {O(1)}
(g₂₅,ab_end), X₁: 0 {O(1)}
(g₂₅,ab_end), X₂: 1 {O(1)}
(g₂₉,ac_end), X₀: 0 {O(1)}
(g₂₉,ac_end), X₁: 0 {O(1)}
(g₂₉,ac_end), X₂: 1 {O(1)}
(g₃₁,bc), X₀: 0 {O(1)}
(g₃₁,bc), X₁: 0 {O(1)}
(g₃₁,bc), X₂: 1 {O(1)}
(g₃₃,bc_end), X₀: 0 {O(1)}
(g₃₃,bc_end), X₁: 0 {O(1)}
(g₃₃,bc_end), X₂: 0 {O(1)}

Run probabilistic analysis on SCC: [bc_end]

Results of Probabilistic Analysis

All Bounds

Timebounds

Overall timebound:31/2 {O(1)}
g₀: 4 {O(1)}
g₅: 3/2 {O(1)}
g₉: 1 {O(1)}
g₁₆: 2 {O(1)}
g₁₉: 1 {O(1)}
g₂₁: 1 {O(1)}
g₂₃: 1 {O(1)}
g₂₅: 1 {O(1)}
g₂₉: 1 {O(1)}
g₃₁: 1 {O(1)}
g₃₃: 1 {O(1)}

Costbounds

Overall costbound: 49/2 {O(1)}
g₀: 16 {O(1)}
g₅: 9/2 {O(1)}
g₉: 0 {O(1)}
g₁₆: 4 {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₀,abc_end), X₀: 2 {O(1)}
(g₀,abc_end), X₁: 0 {O(1)}
(g₀,abc_end), X₂: 1 {O(1)}
(g₅,ab), X₀: 1 {O(1)}
(g₅,ab), X₁: 0 {O(1)}
(g₅,ab), X₂: 0 {O(1)}
(g₉,ab_end), X₀: 0 {O(1)}
(g₉,ab_end), X₁: 0 {O(1)}
(g₉,ab_end), X₂: 0 {O(1)}
(g₁₆,bc), X₀: 0 {O(1)}
(g₁₆,bc), X₁: 0 {O(1)}
(g₁₆,bc), X₂: 0 {O(1)}
(g₁₉,bc_end), X₀: 0 {O(1)}
(g₁₉,bc_end), X₁: 0 {O(1)}
(g₁₉,bc_end), X₂: 0 {O(1)}
(g₂₁,abc), X₀: 1 {O(1)}
(g₂₁,abc), X₁: 1 {O(1)}
(g₂₁,abc), X₂: 1 {O(1)}
(g₂₃,ab), X₀: 1 {O(1)}
(g₂₃,ab), X₁: 0 {O(1)}
(g₂₃,ab), X₂: 0 {O(1)}
(g₂₅,ab_end), X₀: 0 {O(1)}
(g₂₅,ab_end), X₁: 0 {O(1)}
(g₂₅,ab_end), X₂: 1 {O(1)}
(g₂₉,ac_end), X₀: 0 {O(1)}
(g₂₉,ac_end), X₁: 0 {O(1)}
(g₂₉,ac_end), X₂: 1 {O(1)}
(g₃₁,bc), X₀: 0 {O(1)}
(g₃₁,bc), X₁: 0 {O(1)}
(g₃₁,bc), X₂: 1 {O(1)}
(g₃₃,bc_end), X₀: 0 {O(1)}
(g₃₃,bc_end), X₁: 0 {O(1)}
(g₃₃,bc_end), X₂: 0 {O(1)}