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)}