Preprocessing
Found invariant 0 ≤ X₂ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₀ for location l2
Probabilistic Analysis
Probabilistic Program after Preprocessing
Start: l0
Program_Vars: X₀, X₁, X₂
Temp_Vars:
Locations: l0, l1, l2
Transitions:
g₀:l0(X₀,X₁,X₂) → t₁:l1(X₀,X₁,X₂) :|:
g₂:l1(X₀,X₁,X₂) → t₃:l2(X₀,X₁,X₂) :|: 0 ≤ X₀ ∧ X₀ ≤ X₂
g₄:l2(X₀,X₁,X₂) → [1/2]:t₅:l1(1+X₀,X₁,X₂) :+: [1/2]:t₆:l1(X₀,X₁,X₂) :|: X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂
g₇:l2(X₀,X₁,X₂) → [1/2]:t₈:l1(X₀-1,X₁,X₂) :+: [1/2]:t₉:l1(X₀,X₁,X₂) :|: 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂
Show Graph
G
l0
l0
l1
l1
l0->l1
p = 1
t₁ ∈ g₀
l2
l2
l1->l2
p = 1
t₃ ∈ g₂
τ = 0 ≤ X₀ ∧ X₀ ≤ X₂
l2->l1
p = 1/2
t₅ ∈ g₄
η (X₀) = 1+X₀
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2->l1
p = 1/2
t₆ ∈ g₄
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2->l1
p = 1/2
t₈ ∈ g₇
η (X₀) = X₀-1
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2->l1
p = 1/2
t₉ ∈ g₇
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
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}
g₇: inf {Infinity}
Costbounds
Overall costbound: inf {Infinity}
g₀: inf {Infinity}
g₂: inf {Infinity}
g₄: inf {Infinity}
g₇: inf {Infinity}
Sizebounds
(g₀,l1), X₀: X₀ {O(n)}
(g₀,l1), X₁: X₁ {O(n)}
(g₀,l1), X₂: X₂ {O(n)}
Run probabilistic analysis on SCC: [l0]
Run classical analysis on SCC: [l1; l2]
Classical Approximation after Lifting Classical Results
All Bounds
Timebounds
Overall timebound:inf {Infinity}
g₀: 1 {O(1)}
g₂: inf {Infinity}
g₄: inf {Infinity}
g₇: inf {Infinity}
Costbounds
Overall costbound: inf {Infinity}
g₀: inf {Infinity}
g₂: inf {Infinity}
g₄: inf {Infinity}
g₇: inf {Infinity}
Sizebounds
(g₀,l1), X₀: X₀ {O(n)}
(g₀,l1), X₁: X₁ {O(n)}
(g₀,l1), X₂: X₂ {O(n)}
(g₂,l2), X₁: X₁ {O(n)}
(g₂,l2), X₂: X₂ {O(n)}
(g₄,l1), X₁: 2⋅X₁ {O(n)}
(g₄,l1), X₂: 2⋅X₂ {O(n)}
(g₇,l1), X₁: 2⋅X₁ {O(n)}
(g₇,l1), X₂: 2⋅X₂ {O(n)}
Run probabilistic analysis on SCC: [l1; l2]
Analysing control-flow refined program
Run classical analysis on SCC: [l1]
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₁₇: 1 {O(1)}
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}
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}
g₃₆: inf {Infinity}
g₃₈: inf {Infinity}
g₄₁: inf {Infinity}
Sizebounds
(g₀,l1), X₀: X₀ {O(n)}
(g₀,l1), X₁: X₁ {O(n)}
(g₀,l1), X₂: X₂ {O(n)}
(g₁₁,l2_v1), X₀: X₀ {O(n)}
(g₁₁,l2_v1), X₁: X₁ {O(n)}
(g₁₁,l2_v1), X₂: X₂ {O(n)}
Run probabilistic analysis on SCC: [l1]
Run classical analysis on SCC: [l2_v1]
Classical Approximation after Lifting Classical Results
All Bounds
Timebounds
Overall timebound:inf {Infinity}
g₀: 1 {O(1)}
g₁₁: 1 {O(1)}
g₁₄: 2 {O(1)}
g₁₇: 2 {O(1)}
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}
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}
g₃₆: inf {Infinity}
g₃₈: inf {Infinity}
g₄₁: inf {Infinity}
Sizebounds
(g₀,l1), X₀: X₀ {O(n)}
(g₀,l1), X₁: X₁ {O(n)}
(g₀,l1), X₂: X₂ {O(n)}
(g₁₁,l2_v1), X₀: X₀ {O(n)}
(g₁₁,l2_v1), X₁: X₁ {O(n)}
(g₁₁,l2_v1), X₂: X₂ {O(n)}
(g₁₄,l1_v1), X₀: 2⋅X₀+1 {O(n)}
(g₁₄,l1_v1), X₁: 2⋅X₁ {O(n)}
(g₁₄,l1_v1), X₂: 2⋅X₂ {O(n)}
(g₁₄,l1_v2), X₀: 2⋅X₀+1 {O(n)}
(g₁₄,l1_v2), X₁: 2⋅X₁ {O(n)}
(g₁₄,l1_v2), X₂: 2⋅X₂ {O(n)}
(g₁₇,l1_v3), X₀: 2⋅X₀+1 {O(n)}
(g₁₇,l1_v3), X₁: 2⋅X₁ {O(n)}
(g₁₇,l1_v3), X₂: 2⋅X₂ {O(n)}
(g₁₇,l1_v4), X₀: 2⋅X₀+1 {O(n)}
(g₁₇,l1_v4), X₁: 2⋅X₁ {O(n)}
(g₁₇,l1_v4), X₂: 2⋅X₂ {O(n)}
Run probabilistic analysis on SCC: [l2_v1]
Run classical analysis on SCC: [l1_v2; l2_v5]
Classical Approximation after Lifting Classical Results
All Bounds
Timebounds
Overall timebound:inf {Infinity}
g₀: 1 {O(1)}
g₁₁: 1 {O(1)}
g₁₄: 2 {O(1)}
g₁₇: 2 {O(1)}
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}
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}
g₃₆: inf {Infinity}
g₃₈: inf {Infinity}
g₄₁: inf {Infinity}
Sizebounds
(g₀,l1), X₀: X₀ {O(n)}
(g₀,l1), X₁: X₁ {O(n)}
(g₀,l1), X₂: X₂ {O(n)}
(g₁₁,l2_v1), X₀: X₀ {O(n)}
(g₁₁,l2_v1), X₁: X₁ {O(n)}
(g₁₁,l2_v1), X₂: X₂ {O(n)}
(g₁₄,l1_v1), X₀: 2⋅X₀+1 {O(n)}
(g₁₄,l1_v1), X₁: X₁ {O(n)}
(g₁₄,l1_v1), X₂: X₂ {O(n)}
(g₁₄,l1_v2), X₀: X₀ {O(n)}
(g₁₄,l1_v2), X₁: X₁ {O(n)}
(g₁₄,l1_v2), X₂: X₂ {O(n)}
(g₁₇,l1_v3), X₀: 2⋅X₀+1 {O(n)}
(g₁₇,l1_v3), X₁: X₁ {O(n)}
(g₁₇,l1_v3), X₂: X₂ {O(n)}
(g₁₇,l1_v4), X₀: X₀ {O(n)}
(g₁₇,l1_v4), X₁: X₁ {O(n)}
(g₁₇,l1_v4), X₂: X₂ {O(n)}
(g₃₈,l2_v5), X₀: X₀ {O(n)}
(g₃₈,l2_v5), X₁: X₁ {O(n)}
(g₃₈,l2_v5), X₂: X₂ {O(n)}
(g₄₁,l1_v1), X₀: 2⋅X₀+1 {O(n)}
(g₄₁,l1_v1), X₁: 2⋅X₁ {O(n)}
(g₄₁,l1_v1), X₂: 2⋅X₂ {O(n)}
(g₄₁,l1_v2), X₀: 2⋅X₀+1 {O(n)}
(g₄₁,l1_v2), X₁: 2⋅X₁ {O(n)}
(g₄₁,l1_v2), X₂: 2⋅X₂ {O(n)}
Run probabilistic analysis on SCC: [l1_v2; l2_v5]
Plrf for transition g₃₈:l1_v2(X₀,X₁,X₂) → t₃₇:l2_v5(X₀,X₁,X₂) :|: 0 ≤ X₀ ∧ X₀ ≤ X₂ ∧ 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ X₁ ≤ 0 ∧ 0 ≤ X₂:
new bound:
2 {O(1)}
PLRF:
• l1_v1: 0
• l1_v2: 2
• l2_v5: 1
Show Graph
G
l0
l0
l1
l1
l0->l1
p = 1
t₁ ∈ g₀
l2_v1
l2_v1
l1->l2_v1
p = 1
t₁₀ ∈ g₁₁
τ = 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v1
l1_v1
l2_v4
l2_v4
l1_v1->l2_v4
p = 1
t₃₀ ∈ g₃₁
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1 ≤ X₀ ∧ X₁ ≤ 0 ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v2
l1_v2
l2_v5
l2_v5
l1_v2->l2_v5
p = 1
t₃₇ ∈ g₃₈
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ X₁ ≤ 0 ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v3
l1_v3
l2_v2
l2_v2
l1_v3->l2_v2
p = 1
t₁₈ ∈ g₁₉
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1+X₀ ≤ X₂ ∧ 1 ≤ X₁ ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v4
l1_v4
l2_v3
l2_v3
l1_v4->l2_v3
p = 1
t₂₅ ∈ g₂₆
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1 ≤ X₁ ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v5
l1_v5
l1_v5->l2_v2
p = 1
t₂₃ ∈ g₂₄
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1+X₀ ≤ X₂ ∧ 1 ≤ X₁ ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v6
l1_v6
l1_v6->l2_v4
p = 1
t₃₅ ∈ g₃₆
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1 ≤ X₀ ∧ X₁ ≤ 0 ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l2_v1->l1_v1
p = 1/2
t₁₂ ∈ g₁₄
η (X₀) = 1+X₀
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v1->l1_v2
p = 1/2
t₁₃ ∈ g₁₄
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v1->l1_v3
p = 1/2
t₁₅ ∈ g₁₇
η (X₀) = X₀-1
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v1->l1_v4
p = 1/2
t₁₆ ∈ g₁₇
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v2->l1_v3
p = 1/2
t₂₀ ∈ g₂₂
η (X₀) = X₀-1
τ = 1+X₀ ≤ X₂ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v2->l1_v5
p = 1/2
t₂₁ ∈ g₂₂
τ = 1+X₀ ≤ X₂ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v3->l1_v3
p = 1/2
t₂₇ ∈ g₂₉
η (X₀) = X₀-1
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v3->l1_v4
p = 1/2
t₂₈ ∈ g₂₉
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v4->l1_v1
p = 1/2
t₃₂ ∈ g₃₄
η (X₀) = 1+X₀
τ = 1 ≤ X₀ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v4->l1_v6
p = 1/2
t₃₃ ∈ g₃₄
τ = 1 ≤ X₀ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v5->l1_v1
p = 1/2
t₃₉ ∈ g₄₁
η (X₀) = 1+X₀
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v5->l1_v2
p = 1/2
t₄₀ ∈ g₄₁
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
Use classical time bound for entry point (g₁₄:l2_v1→[t₁₂:1/2:l1_v1; t₁₃:1/2:l1_v2],l1_v2)
Plrf for transition g₄₁:l2_v5(X₀,X₁,X₂) → [1/2]:t₃₉:l1_v1(1+X₀,X₁,X₂) :+: [1/2]:t₄₀:l1_v2(X₀,X₁,X₂) :|: X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂:
new bound:
2 {O(1)}
PLRF:
• l1_v1: 0
• l1_v2: 2
• l2_v5: 2
Show Graph
G
l0
l0
l1
l1
l0->l1
p = 1
t₁ ∈ g₀
l2_v1
l2_v1
l1->l2_v1
p = 1
t₁₀ ∈ g₁₁
τ = 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v1
l1_v1
l2_v4
l2_v4
l1_v1->l2_v4
p = 1
t₃₀ ∈ g₃₁
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1 ≤ X₀ ∧ X₁ ≤ 0 ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v2
l1_v2
l2_v5
l2_v5
l1_v2->l2_v5
p = 1
t₃₇ ∈ g₃₈
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ X₁ ≤ 0 ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v3
l1_v3
l2_v2
l2_v2
l1_v3->l2_v2
p = 1
t₁₈ ∈ g₁₉
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1+X₀ ≤ X₂ ∧ 1 ≤ X₁ ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v4
l1_v4
l2_v3
l2_v3
l1_v4->l2_v3
p = 1
t₂₅ ∈ g₂₆
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1 ≤ X₁ ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v5
l1_v5
l1_v5->l2_v2
p = 1
t₂₃ ∈ g₂₄
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1+X₀ ≤ X₂ ∧ 1 ≤ X₁ ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v6
l1_v6
l1_v6->l2_v4
p = 1
t₃₅ ∈ g₃₆
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1 ≤ X₀ ∧ X₁ ≤ 0 ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l2_v1->l1_v1
p = 1/2
t₁₂ ∈ g₁₄
η (X₀) = 1+X₀
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v1->l1_v2
p = 1/2
t₁₃ ∈ g₁₄
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v1->l1_v3
p = 1/2
t₁₅ ∈ g₁₇
η (X₀) = X₀-1
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v1->l1_v4
p = 1/2
t₁₆ ∈ g₁₇
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v2->l1_v3
p = 1/2
t₂₀ ∈ g₂₂
η (X₀) = X₀-1
τ = 1+X₀ ≤ X₂ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v2->l1_v5
p = 1/2
t₂₁ ∈ g₂₂
τ = 1+X₀ ≤ X₂ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v3->l1_v3
p = 1/2
t₂₇ ∈ g₂₉
η (X₀) = X₀-1
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v3->l1_v4
p = 1/2
t₂₈ ∈ g₂₉
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v4->l1_v1
p = 1/2
t₃₂ ∈ g₃₄
η (X₀) = 1+X₀
τ = 1 ≤ X₀ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v4->l1_v6
p = 1/2
t₃₃ ∈ g₃₄
τ = 1 ≤ X₀ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v5->l1_v1
p = 1/2
t₃₉ ∈ g₄₁
η (X₀) = 1+X₀
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v5->l1_v2
p = 1/2
t₄₀ ∈ g₄₁
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
Use classical time bound for entry point (g₁₄:l2_v1→[t₁₂:1/2:l1_v1; t₁₃:1/2:l1_v2],l1_v2)
Run classical analysis on SCC: [l1_v1; l1_v6; l2_v4]
MPRF for transition t₃₀: l1_v1(X₀,X₁,X₂) → l2_v4(X₀,X₁,X₂) :|: 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1 ≤ X₀ ∧ X₁ ≤ 0 ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂ of depth 1:
new bound:
2⋅X₀+2⋅X₂+4 {O(n)}
MPRF:
• l1_v1: [1+X₂-X₀]
• l1_v6: [X₂-X₀]
• l2_v4: [X₂-X₀]
Show Graph
G
l0
l0
l1
l1
l0->l1
t₁
l2_v1
l2_v1
l1->l2_v1
t₁₀
τ = 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v1
l1_v1
l2_v4
l2_v4
l1_v1->l2_v4
t₃₀
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1 ≤ X₀ ∧ X₁ ≤ 0 ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v2
l1_v2
l2_v5
l2_v5
l1_v2->l2_v5
t₃₇
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ X₁ ≤ 0 ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v3
l1_v3
l2_v2
l2_v2
l1_v3->l2_v2
t₁₈
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1+X₀ ≤ X₂ ∧ 1 ≤ X₁ ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v4
l1_v4
l2_v3
l2_v3
l1_v4->l2_v3
t₂₅
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1 ≤ X₁ ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v5
l1_v5
l1_v5->l2_v2
t₂₃
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1+X₀ ≤ X₂ ∧ 1 ≤ X₁ ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v6
l1_v6
l1_v6->l2_v4
t₃₅
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1 ≤ X₀ ∧ X₁ ≤ 0 ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l2_v1->l1_v1
t₁₂
η (X₀) = 1+X₀
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v1->l1_v2
t₁₃
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v1->l1_v3
t₁₅
η (X₀) = X₀-1
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v1->l1_v4
t₁₆
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v2->l1_v3
t₂₀
η (X₀) = X₀-1
τ = 1+X₀ ≤ X₂ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v2->l1_v5
t₂₁
τ = 1+X₀ ≤ X₂ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v3->l1_v3
t₂₇
η (X₀) = X₀-1
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v3->l1_v4
t₂₈
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v4->l1_v1
t₃₂
η (X₀) = 1+X₀
τ = 1 ≤ X₀ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v4->l1_v6
t₃₃
τ = 1 ≤ X₀ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v5->l1_v1
t₃₉
η (X₀) = 1+X₀
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v5->l1_v2
t₄₀
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
MPRF for transition t₃₂: l2_v4(X₀,X₁,X₂) → l1_v1(1+X₀,X₁,X₂) :|: 1 ≤ X₀ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0 of depth 1:
new bound:
2⋅X₀+2⋅X₂+4 {O(n)}
MPRF:
• l1_v1: [1+X₂-X₀]
• l1_v6: [1+X₂-X₀]
• l2_v4: [1+X₂-X₀]
Show Graph
G
l0
l0
l1
l1
l0->l1
t₁
l2_v1
l2_v1
l1->l2_v1
t₁₀
τ = 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v1
l1_v1
l2_v4
l2_v4
l1_v1->l2_v4
t₃₀
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1 ≤ X₀ ∧ X₁ ≤ 0 ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v2
l1_v2
l2_v5
l2_v5
l1_v2->l2_v5
t₃₇
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ X₁ ≤ 0 ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v3
l1_v3
l2_v2
l2_v2
l1_v3->l2_v2
t₁₈
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1+X₀ ≤ X₂ ∧ 1 ≤ X₁ ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v4
l1_v4
l2_v3
l2_v3
l1_v4->l2_v3
t₂₅
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1 ≤ X₁ ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v5
l1_v5
l1_v5->l2_v2
t₂₃
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1+X₀ ≤ X₂ ∧ 1 ≤ X₁ ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v6
l1_v6
l1_v6->l2_v4
t₃₅
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1 ≤ X₀ ∧ X₁ ≤ 0 ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l2_v1->l1_v1
t₁₂
η (X₀) = 1+X₀
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v1->l1_v2
t₁₃
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v1->l1_v3
t₁₅
η (X₀) = X₀-1
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v1->l1_v4
t₁₆
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v2->l1_v3
t₂₀
η (X₀) = X₀-1
τ = 1+X₀ ≤ X₂ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v2->l1_v5
t₂₁
τ = 1+X₀ ≤ X₂ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v3->l1_v3
t₂₇
η (X₀) = X₀-1
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v3->l1_v4
t₂₈
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v4->l1_v1
t₃₂
η (X₀) = 1+X₀
τ = 1 ≤ X₀ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v4->l1_v6
t₃₃
τ = 1 ≤ X₀ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v5->l1_v1
t₃₉
η (X₀) = 1+X₀
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v5->l1_v2
t₄₀
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
Classical Approximation after Lifting Classical Results
All Bounds
Timebounds
Overall timebound:inf {Infinity}
g₀: 1 {O(1)}
g₁₁: 1 {O(1)}
g₁₄: 2 {O(1)}
g₁₇: 2 {O(1)}
g₁₉: inf {Infinity}
g₂₂: inf {Infinity}
g₂₄: inf {Infinity}
g₂₆: inf {Infinity}
g₂₉: inf {Infinity}
g₃₁: 2⋅X₀+2⋅X₂+4 {O(n)}
g₃₄: inf {Infinity}
g₃₆: inf {Infinity}
g₃₈: 2 {O(1)}
g₄₁: 2 {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}
g₃₆: inf {Infinity}
g₃₈: inf {Infinity}
g₄₁: inf {Infinity}
Sizebounds
(g₀,l1), X₀: X₀ {O(n)}
(g₀,l1), X₁: X₁ {O(n)}
(g₀,l1), X₂: X₂ {O(n)}
(g₁₁,l2_v1), X₀: X₀ {O(n)}
(g₁₁,l2_v1), X₁: X₁ {O(n)}
(g₁₁,l2_v1), X₂: X₂ {O(n)}
(g₁₄,l1_v1), X₀: 2⋅X₀+1 {O(n)}
(g₁₄,l1_v1), X₁: X₁ {O(n)}
(g₁₄,l1_v1), X₂: X₂ {O(n)}
(g₁₄,l1_v2), X₀: X₀ {O(n)}
(g₁₄,l1_v2), X₁: X₁ {O(n)}
(g₁₄,l1_v2), X₂: X₂ {O(n)}
(g₁₇,l1_v3), X₀: 2⋅X₀+1 {O(n)}
(g₁₇,l1_v3), X₁: X₁ {O(n)}
(g₁₇,l1_v3), X₂: X₂ {O(n)}
(g₁₇,l1_v4), X₀: X₀ {O(n)}
(g₁₇,l1_v4), X₁: X₁ {O(n)}
(g₁₇,l1_v4), X₂: X₂ {O(n)}
(g₃₁,l2_v4), X₀: 2⋅X₂+4⋅X₀+6 {O(n)}
(g₃₁,l2_v4), X₁: 2⋅X₁ {O(n)}
(g₃₁,l2_v4), X₂: 2⋅X₂ {O(n)}
(g₃₄,l1_v1), X₀: 4⋅X₂+8⋅X₀+12 {O(n)}
(g₃₄,l1_v1), X₁: 4⋅X₁ {O(n)}
(g₃₄,l1_v1), X₂: 4⋅X₂ {O(n)}
(g₃₄,l1_v6), X₀: 4⋅X₂+8⋅X₀+12 {O(n)}
(g₃₄,l1_v6), X₁: 4⋅X₁ {O(n)}
(g₃₄,l1_v6), X₂: 4⋅X₂ {O(n)}
(g₃₆,l2_v4), X₀: 2⋅X₂+4⋅X₀+6 {O(n)}
(g₃₆,l2_v4), X₁: 2⋅X₁ {O(n)}
(g₃₆,l2_v4), X₂: 2⋅X₂ {O(n)}
(g₃₈,l2_v5), X₀: X₀ {O(n)}
(g₃₈,l2_v5), X₁: X₁ {O(n)}
(g₃₈,l2_v5), X₂: X₂ {O(n)}
(g₄₁,l1_v1), X₀: X₀+1 {O(n)}
(g₄₁,l1_v1), X₁: X₁ {O(n)}
(g₄₁,l1_v1), X₂: X₂ {O(n)}
(g₄₁,l1_v2), X₀: X₀+1 {O(n)}
(g₄₁,l1_v2), X₁: X₁ {O(n)}
(g₄₁,l1_v2), X₂: X₂ {O(n)}
Run probabilistic analysis on SCC: [l1_v1; l1_v6; l2_v4]
Plrf for transition g₃₄:l2_v4(X₀,X₁,X₂) → [1/2]:t₃₂:l1_v1(1+X₀,X₁,X₂) :+: [1/2]:t₃₃:l1_v6(X₀,X₁,X₂) :|: X₁ ≤ 0 ∧ 1 ≤ X₀ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂:
new bound:
6⋅X₀+8⋅X₂+4 {O(n)}
PLRF:
• l1_v1: 4⋅X₂-2⋅X₀
• l1_v6: 4⋅X₂-2⋅X₀
• l2_v4: 4⋅X₂-2⋅X₀
Show Graph
G
l0
l0
l1
l1
l0->l1
p = 1
t₁ ∈ g₀
l2_v1
l2_v1
l1->l2_v1
p = 1
t₁₀ ∈ g₁₁
τ = 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v1
l1_v1
l2_v4
l2_v4
l1_v1->l2_v4
p = 1
t₃₀ ∈ g₃₁
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1 ≤ X₀ ∧ X₁ ≤ 0 ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v2
l1_v2
l2_v5
l2_v5
l1_v2->l2_v5
p = 1
t₃₇ ∈ g₃₈
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ X₁ ≤ 0 ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v3
l1_v3
l2_v2
l2_v2
l1_v3->l2_v2
p = 1
t₁₈ ∈ g₁₉
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1+X₀ ≤ X₂ ∧ 1 ≤ X₁ ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v4
l1_v4
l2_v3
l2_v3
l1_v4->l2_v3
p = 1
t₂₅ ∈ g₂₆
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1 ≤ X₁ ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v5
l1_v5
l1_v5->l2_v2
p = 1
t₂₃ ∈ g₂₄
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1+X₀ ≤ X₂ ∧ 1 ≤ X₁ ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v6
l1_v6
l1_v6->l2_v4
p = 1
t₃₅ ∈ g₃₆
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1 ≤ X₀ ∧ X₁ ≤ 0 ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l2_v1->l1_v1
p = 1/2
t₁₂ ∈ g₁₄
η (X₀) = 1+X₀
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v1->l1_v2
p = 1/2
t₁₃ ∈ g₁₄
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v1->l1_v3
p = 1/2
t₁₅ ∈ g₁₇
η (X₀) = X₀-1
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v1->l1_v4
p = 1/2
t₁₆ ∈ g₁₇
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v2->l1_v3
p = 1/2
t₂₀ ∈ g₂₂
η (X₀) = X₀-1
τ = 1+X₀ ≤ X₂ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v2->l1_v5
p = 1/2
t₂₁ ∈ g₂₂
τ = 1+X₀ ≤ X₂ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v3->l1_v3
p = 1/2
t₂₇ ∈ g₂₉
η (X₀) = X₀-1
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v3->l1_v4
p = 1/2
t₂₈ ∈ g₂₉
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v4->l1_v1
p = 1/2
t₃₂ ∈ g₃₄
η (X₀) = 1+X₀
τ = 1 ≤ X₀ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v4->l1_v6
p = 1/2
t₃₃ ∈ g₃₄
τ = 1 ≤ X₀ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v5->l1_v1
p = 1/2
t₃₉ ∈ g₄₁
η (X₀) = 1+X₀
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v5->l1_v2
p = 1/2
t₄₀ ∈ g₄₁
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
Use expected size bounds for entry point (g₁₄:l2_v1→[t₁₂:1/2:l1_v1; t₁₃:1/2:l1_v2],l1_v1)
Use expected size bounds for entry point (g₁₄:l2_v1→[t₁₂:1/2:l1_v1; t₁₃:1/2:l1_v2],l1_v1)
Use classical time bound for entry point (g₁₄:l2_v1→[t₁₂:1/2:l1_v1; t₁₃:1/2:l1_v2],l1_v1)
Use expected size bounds for entry point (g₄₁:l2_v5→[t₃₉:1/2:l1_v1; t₄₀:1/2:l1_v2],l1_v1)
Use expected size bounds for entry point (g₄₁:l2_v5→[t₃₉:1/2:l1_v1; t₄₀:1/2:l1_v2],l1_v1)
Use classical time bound for entry point (g₄₁:l2_v5→[t₃₉:1/2:l1_v1; t₄₀:1/2:l1_v2],l1_v1)
Plrf for transition g₃₆:l1_v6(X₀,X₁,X₂) → t₃₅:l2_v4(X₀,X₁,X₂) :|: 0 ≤ X₀ ∧ X₀ ≤ X₂ ∧ 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1 ≤ X₀ ∧ X₁ ≤ 0 ∧ 0 ≤ X₂:
new bound:
3⋅X₀+4⋅X₂+2 {O(n)}
PLRF:
• l1_v1: 2⋅X₂-X₀
• l1_v6: 1+2⋅X₂-X₀
• l2_v4: 2⋅X₂-X₀
Show Graph
G
l0
l0
l1
l1
l0->l1
p = 1
t₁ ∈ g₀
l2_v1
l2_v1
l1->l2_v1
p = 1
t₁₀ ∈ g₁₁
τ = 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v1
l1_v1
l2_v4
l2_v4
l1_v1->l2_v4
p = 1
t₃₀ ∈ g₃₁
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1 ≤ X₀ ∧ X₁ ≤ 0 ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v2
l1_v2
l2_v5
l2_v5
l1_v2->l2_v5
p = 1
t₃₇ ∈ g₃₈
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ X₁ ≤ 0 ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v3
l1_v3
l2_v2
l2_v2
l1_v3->l2_v2
p = 1
t₁₈ ∈ g₁₉
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1+X₀ ≤ X₂ ∧ 1 ≤ X₁ ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v4
l1_v4
l2_v3
l2_v3
l1_v4->l2_v3
p = 1
t₂₅ ∈ g₂₆
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1 ≤ X₁ ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v5
l1_v5
l1_v5->l2_v2
p = 1
t₂₃ ∈ g₂₄
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1+X₀ ≤ X₂ ∧ 1 ≤ X₁ ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v6
l1_v6
l1_v6->l2_v4
p = 1
t₃₅ ∈ g₃₆
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1 ≤ X₀ ∧ X₁ ≤ 0 ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l2_v1->l1_v1
p = 1/2
t₁₂ ∈ g₁₄
η (X₀) = 1+X₀
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v1->l1_v2
p = 1/2
t₁₃ ∈ g₁₄
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v1->l1_v3
p = 1/2
t₁₅ ∈ g₁₇
η (X₀) = X₀-1
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v1->l1_v4
p = 1/2
t₁₆ ∈ g₁₇
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v2->l1_v3
p = 1/2
t₂₀ ∈ g₂₂
η (X₀) = X₀-1
τ = 1+X₀ ≤ X₂ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v2->l1_v5
p = 1/2
t₂₁ ∈ g₂₂
τ = 1+X₀ ≤ X₂ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v3->l1_v3
p = 1/2
t₂₇ ∈ g₂₉
η (X₀) = X₀-1
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v3->l1_v4
p = 1/2
t₂₈ ∈ g₂₉
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v4->l1_v1
p = 1/2
t₃₂ ∈ g₃₄
η (X₀) = 1+X₀
τ = 1 ≤ X₀ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v4->l1_v6
p = 1/2
t₃₃ ∈ g₃₄
τ = 1 ≤ X₀ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v5->l1_v1
p = 1/2
t₃₉ ∈ g₄₁
η (X₀) = 1+X₀
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v5->l1_v2
p = 1/2
t₄₀ ∈ g₄₁
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
Use expected size bounds for entry point (g₁₄:l2_v1→[t₁₂:1/2:l1_v1; t₁₃:1/2:l1_v2],l1_v1)
Use expected size bounds for entry point (g₁₄:l2_v1→[t₁₂:1/2:l1_v1; t₁₃:1/2:l1_v2],l1_v1)
Use classical time bound for entry point (g₁₄:l2_v1→[t₁₂:1/2:l1_v1; t₁₃:1/2:l1_v2],l1_v1)
Use expected size bounds for entry point (g₄₁:l2_v5→[t₃₉:1/2:l1_v1; t₄₀:1/2:l1_v2],l1_v1)
Use expected size bounds for entry point (g₄₁:l2_v5→[t₃₉:1/2:l1_v1; t₄₀:1/2:l1_v2],l1_v1)
Use classical time bound for entry point (g₄₁:l2_v5→[t₃₉:1/2:l1_v1; t₄₀:1/2:l1_v2],l1_v1)
Run classical analysis on SCC: [l1_v4; l2_v3]
Classical Approximation after Lifting Classical Results
All Bounds
Timebounds
Overall timebound:inf {Infinity}
g₀: 1 {O(1)}
g₁₁: 1 {O(1)}
g₁₄: 2 {O(1)}
g₁₇: 2 {O(1)}
g₁₉: inf {Infinity}
g₂₂: inf {Infinity}
g₂₄: inf {Infinity}
g₂₆: inf {Infinity}
g₂₉: inf {Infinity}
g₃₁: 2⋅X₀+2⋅X₂+4 {O(n)}
g₃₄: 6⋅X₀+8⋅X₂+4 {O(n)}
g₃₆: 3⋅X₀+4⋅X₂+2 {O(n)}
g₃₈: 2 {O(1)}
g₄₁: 2 {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}
g₃₆: inf {Infinity}
g₃₈: inf {Infinity}
g₄₁: inf {Infinity}
Sizebounds
(g₀,l1), X₀: X₀ {O(n)}
(g₀,l1), X₁: X₁ {O(n)}
(g₀,l1), X₂: X₂ {O(n)}
(g₁₁,l2_v1), X₀: X₀ {O(n)}
(g₁₁,l2_v1), X₁: X₁ {O(n)}
(g₁₁,l2_v1), X₂: X₂ {O(n)}
(g₁₄,l1_v1), X₀: 2⋅X₀+1 {O(n)}
(g₁₄,l1_v1), X₁: X₁ {O(n)}
(g₁₄,l1_v1), X₂: X₂ {O(n)}
(g₁₄,l1_v2), X₀: X₀ {O(n)}
(g₁₄,l1_v2), X₁: X₁ {O(n)}
(g₁₄,l1_v2), X₂: X₂ {O(n)}
(g₁₇,l1_v3), X₀: 2⋅X₀+1 {O(n)}
(g₁₇,l1_v3), X₁: X₁ {O(n)}
(g₁₇,l1_v3), X₂: X₂ {O(n)}
(g₁₇,l1_v4), X₀: X₀ {O(n)}
(g₁₇,l1_v4), X₁: X₁ {O(n)}
(g₁₇,l1_v4), X₂: X₂ {O(n)}
(g₂₆,l2_v3), X₀: X₀ {O(n)}
(g₂₆,l2_v3), X₁: X₁ {O(n)}
(g₂₆,l2_v3), X₂: X₂ {O(n)}
(g₂₉,l1_v3), X₀: 2⋅X₀+1 {O(n)}
(g₂₉,l1_v3), X₁: 2⋅X₁ {O(n)}
(g₂₉,l1_v3), X₂: 2⋅X₂ {O(n)}
(g₂₉,l1_v4), X₀: 2⋅X₀+1 {O(n)}
(g₂₉,l1_v4), X₁: 2⋅X₁ {O(n)}
(g₂₉,l1_v4), X₂: 2⋅X₂ {O(n)}
(g₃₁,l2_v4), X₀: 2⋅X₂+4⋅X₀+6 {O(n)}
(g₃₁,l2_v4), X₁: 2⋅X₁ {O(n)}
(g₃₁,l2_v4), X₂: 2⋅X₂ {O(n)}
(g₃₄,l1_v1), X₀: 4⋅X₂+6⋅X₀+4 {O(n)}
(g₃₄,l1_v1), X₁: 4⋅X₁ {O(n)}
(g₃₄,l1_v1), X₂: 4⋅X₂ {O(n)}
(g₃₄,l1_v6), X₀: 4⋅X₂+6⋅X₀+4 {O(n)}
(g₃₄,l1_v6), X₁: 4⋅X₁ {O(n)}
(g₃₄,l1_v6), X₂: 4⋅X₂ {O(n)}
(g₃₆,l2_v4), X₀: 2⋅X₂+4⋅X₀+6 {O(n)}
(g₃₆,l2_v4), X₁: 2⋅X₁ {O(n)}
(g₃₆,l2_v4), X₂: 2⋅X₂ {O(n)}
(g₃₈,l2_v5), X₀: X₀ {O(n)}
(g₃₈,l2_v5), X₁: X₁ {O(n)}
(g₃₈,l2_v5), X₂: X₂ {O(n)}
(g₄₁,l1_v1), X₀: X₀+1 {O(n)}
(g₄₁,l1_v1), X₁: X₁ {O(n)}
(g₄₁,l1_v1), X₂: X₂ {O(n)}
(g₄₁,l1_v2), X₀: X₀ {O(n)}
(g₄₁,l1_v2), X₁: X₁ {O(n)}
(g₄₁,l1_v2), X₂: X₂ {O(n)}
Run probabilistic analysis on SCC: [l1_v4; l2_v3]
Plrf for transition g₂₆:l1_v4(X₀,X₁,X₂) → t₂₅:l2_v3(X₀,X₁,X₂) :|: 0 ≤ X₀ ∧ X₀ ≤ X₂ ∧ 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1 ≤ X₁ ∧ 0 ≤ X₂:
new bound:
X₁+1 {O(n)}
PLRF:
• l1_v3: X₁-1
• l1_v4: 1+X₁
• l2_v3: X₁
Show Graph
G
l0
l0
l1
l1
l0->l1
p = 1
t₁ ∈ g₀
l2_v1
l2_v1
l1->l2_v1
p = 1
t₁₀ ∈ g₁₁
τ = 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v1
l1_v1
l2_v4
l2_v4
l1_v1->l2_v4
p = 1
t₃₀ ∈ g₃₁
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1 ≤ X₀ ∧ X₁ ≤ 0 ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v2
l1_v2
l2_v5
l2_v5
l1_v2->l2_v5
p = 1
t₃₇ ∈ g₃₈
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ X₁ ≤ 0 ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v3
l1_v3
l2_v2
l2_v2
l1_v3->l2_v2
p = 1
t₁₈ ∈ g₁₉
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1+X₀ ≤ X₂ ∧ 1 ≤ X₁ ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v4
l1_v4
l2_v3
l2_v3
l1_v4->l2_v3
p = 1
t₂₅ ∈ g₂₆
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1 ≤ X₁ ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v5
l1_v5
l1_v5->l2_v2
p = 1
t₂₃ ∈ g₂₄
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1+X₀ ≤ X₂ ∧ 1 ≤ X₁ ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v6
l1_v6
l1_v6->l2_v4
p = 1
t₃₅ ∈ g₃₆
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1 ≤ X₀ ∧ X₁ ≤ 0 ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l2_v1->l1_v1
p = 1/2
t₁₂ ∈ g₁₄
η (X₀) = 1+X₀
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v1->l1_v2
p = 1/2
t₁₃ ∈ g₁₄
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v1->l1_v3
p = 1/2
t₁₅ ∈ g₁₇
η (X₀) = X₀-1
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v1->l1_v4
p = 1/2
t₁₆ ∈ g₁₇
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v2->l1_v3
p = 1/2
t₂₀ ∈ g₂₂
η (X₀) = X₀-1
τ = 1+X₀ ≤ X₂ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v2->l1_v5
p = 1/2
t₂₁ ∈ g₂₂
τ = 1+X₀ ≤ X₂ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v3->l1_v3
p = 1/2
t₂₇ ∈ g₂₉
η (X₀) = X₀-1
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v3->l1_v4
p = 1/2
t₂₈ ∈ g₂₉
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v4->l1_v1
p = 1/2
t₃₂ ∈ g₃₄
η (X₀) = 1+X₀
τ = 1 ≤ X₀ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v4->l1_v6
p = 1/2
t₃₃ ∈ g₃₄
τ = 1 ≤ X₀ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v5->l1_v1
p = 1/2
t₃₉ ∈ g₄₁
η (X₀) = 1+X₀
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v5->l1_v2
p = 1/2
t₄₀ ∈ g₄₁
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
Use expected size bounds for entry point (g₁₇:l2_v1→[t₁₅:1/2:l1_v3; t₁₆:1/2:l1_v4],l1_v4)
Use classical time bound for entry point (g₁₇:l2_v1→[t₁₅:1/2:l1_v3; t₁₆:1/2:l1_v4],l1_v4)
Plrf for transition g₂₉:l2_v3(X₀,X₁,X₂) → [1/2]:t₂₇:l1_v3(X₀-1,X₁,X₂) :+: [1/2]:t₂₈:l1_v4(X₀,X₁,X₂) :|: 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂:
new bound:
2⋅X₁ {O(n)}
PLRF:
• l1_v3: 0
• l1_v4: 2⋅X₁
• l2_v3: 1+X₁
Show Graph
G
l0
l0
l1
l1
l0->l1
p = 1
t₁ ∈ g₀
l2_v1
l2_v1
l1->l2_v1
p = 1
t₁₀ ∈ g₁₁
τ = 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v1
l1_v1
l2_v4
l2_v4
l1_v1->l2_v4
p = 1
t₃₀ ∈ g₃₁
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1 ≤ X₀ ∧ X₁ ≤ 0 ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v2
l1_v2
l2_v5
l2_v5
l1_v2->l2_v5
p = 1
t₃₇ ∈ g₃₈
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ X₁ ≤ 0 ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v3
l1_v3
l2_v2
l2_v2
l1_v3->l2_v2
p = 1
t₁₈ ∈ g₁₉
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1+X₀ ≤ X₂ ∧ 1 ≤ X₁ ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v4
l1_v4
l2_v3
l2_v3
l1_v4->l2_v3
p = 1
t₂₅ ∈ g₂₆
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1 ≤ X₁ ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v5
l1_v5
l1_v5->l2_v2
p = 1
t₂₃ ∈ g₂₄
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1+X₀ ≤ X₂ ∧ 1 ≤ X₁ ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v6
l1_v6
l1_v6->l2_v4
p = 1
t₃₅ ∈ g₃₆
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1 ≤ X₀ ∧ X₁ ≤ 0 ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l2_v1->l1_v1
p = 1/2
t₁₂ ∈ g₁₄
η (X₀) = 1+X₀
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v1->l1_v2
p = 1/2
t₁₃ ∈ g₁₄
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v1->l1_v3
p = 1/2
t₁₅ ∈ g₁₇
η (X₀) = X₀-1
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v1->l1_v4
p = 1/2
t₁₆ ∈ g₁₇
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v2->l1_v3
p = 1/2
t₂₀ ∈ g₂₂
η (X₀) = X₀-1
τ = 1+X₀ ≤ X₂ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v2->l1_v5
p = 1/2
t₂₁ ∈ g₂₂
τ = 1+X₀ ≤ X₂ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v3->l1_v3
p = 1/2
t₂₇ ∈ g₂₉
η (X₀) = X₀-1
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v3->l1_v4
p = 1/2
t₂₈ ∈ g₂₉
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v4->l1_v1
p = 1/2
t₃₂ ∈ g₃₄
η (X₀) = 1+X₀
τ = 1 ≤ X₀ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v4->l1_v6
p = 1/2
t₃₃ ∈ g₃₄
τ = 1 ≤ X₀ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v5->l1_v1
p = 1/2
t₃₉ ∈ g₄₁
η (X₀) = 1+X₀
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v5->l1_v2
p = 1/2
t₄₀ ∈ g₄₁
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
Use expected size bounds for entry point (g₁₇:l2_v1→[t₁₅:1/2:l1_v3; t₁₆:1/2:l1_v4],l1_v4)
Use classical time bound for entry point (g₁₇:l2_v1→[t₁₅:1/2:l1_v3; t₁₆:1/2:l1_v4],l1_v4)
Run classical analysis on SCC: [l1_v3; l1_v5; l2_v2]
MPRF for transition t₁₈: l1_v3(X₀,X₁,X₂) → l2_v2(X₀,X₁,X₂) :|: 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1+X₀ ≤ X₂ ∧ 1 ≤ X₁ ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂ of depth 1:
new bound:
2⋅X₀+6 {O(n)}
MPRF:
• l1_v3: [2+X₀]
• l1_v5: [1+X₀]
• l2_v2: [1+X₀]
Show Graph
G
l0
l0
l1
l1
l0->l1
t₁
l2_v1
l2_v1
l1->l2_v1
t₁₀
τ = 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v1
l1_v1
l2_v4
l2_v4
l1_v1->l2_v4
t₃₀
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1 ≤ X₀ ∧ X₁ ≤ 0 ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v2
l1_v2
l2_v5
l2_v5
l1_v2->l2_v5
t₃₇
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ X₁ ≤ 0 ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v3
l1_v3
l2_v2
l2_v2
l1_v3->l2_v2
t₁₈
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1+X₀ ≤ X₂ ∧ 1 ≤ X₁ ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v4
l1_v4
l2_v3
l2_v3
l1_v4->l2_v3
t₂₅
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1 ≤ X₁ ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v5
l1_v5
l1_v5->l2_v2
t₂₃
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1+X₀ ≤ X₂ ∧ 1 ≤ X₁ ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v6
l1_v6
l1_v6->l2_v4
t₃₅
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1 ≤ X₀ ∧ X₁ ≤ 0 ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l2_v1->l1_v1
t₁₂
η (X₀) = 1+X₀
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v1->l1_v2
t₁₃
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v1->l1_v3
t₁₅
η (X₀) = X₀-1
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v1->l1_v4
t₁₆
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v2->l1_v3
t₂₀
η (X₀) = X₀-1
τ = 1+X₀ ≤ X₂ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v2->l1_v5
t₂₁
τ = 1+X₀ ≤ X₂ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v3->l1_v3
t₂₇
η (X₀) = X₀-1
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v3->l1_v4
t₂₈
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v4->l1_v1
t₃₂
η (X₀) = 1+X₀
τ = 1 ≤ X₀ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v4->l1_v6
t₃₃
τ = 1 ≤ X₀ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v5->l1_v1
t₃₉
η (X₀) = 1+X₀
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v5->l1_v2
t₄₀
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
MPRF for transition t₂₀: l2_v2(X₀,X₁,X₂) → l1_v3(X₀-1,X₁,X₂) :|: 1+X₀ ≤ X₂ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁ of depth 1:
new bound:
2⋅X₀+4 {O(n)}
MPRF:
• l1_v3: [1+X₀]
• l1_v5: [1+X₀]
• l2_v2: [1+X₀]
Show Graph
G
l0
l0
l1
l1
l0->l1
t₁
l2_v1
l2_v1
l1->l2_v1
t₁₀
τ = 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v1
l1_v1
l2_v4
l2_v4
l1_v1->l2_v4
t₃₀
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1 ≤ X₀ ∧ X₁ ≤ 0 ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v2
l1_v2
l2_v5
l2_v5
l1_v2->l2_v5
t₃₇
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ X₁ ≤ 0 ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v3
l1_v3
l2_v2
l2_v2
l1_v3->l2_v2
t₁₈
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1+X₀ ≤ X₂ ∧ 1 ≤ X₁ ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v4
l1_v4
l2_v3
l2_v3
l1_v4->l2_v3
t₂₅
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1 ≤ X₁ ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v5
l1_v5
l1_v5->l2_v2
t₂₃
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1+X₀ ≤ X₂ ∧ 1 ≤ X₁ ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v6
l1_v6
l1_v6->l2_v4
t₃₅
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1 ≤ X₀ ∧ X₁ ≤ 0 ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l2_v1->l1_v1
t₁₂
η (X₀) = 1+X₀
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v1->l1_v2
t₁₃
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v1->l1_v3
t₁₅
η (X₀) = X₀-1
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v1->l1_v4
t₁₆
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v2->l1_v3
t₂₀
η (X₀) = X₀-1
τ = 1+X₀ ≤ X₂ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v2->l1_v5
t₂₁
τ = 1+X₀ ≤ X₂ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v3->l1_v3
t₂₇
η (X₀) = X₀-1
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v3->l1_v4
t₂₈
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v4->l1_v1
t₃₂
η (X₀) = 1+X₀
τ = 1 ≤ X₀ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v4->l1_v6
t₃₃
τ = 1 ≤ X₀ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v5->l1_v1
t₃₉
η (X₀) = 1+X₀
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v5->l1_v2
t₄₀
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
Classical Approximation after Lifting Classical Results
All Bounds
Timebounds
Overall timebound:inf {Infinity}
g₀: 1 {O(1)}
g₁₁: 1 {O(1)}
g₁₄: 2 {O(1)}
g₁₇: 2 {O(1)}
g₁₉: 2⋅X₀+6 {O(n)}
g₂₂: inf {Infinity}
g₂₄: inf {Infinity}
g₂₆: X₁+1 {O(n)}
g₂₉: 2⋅X₁ {O(n)}
g₃₁: 2⋅X₀+2⋅X₂+4 {O(n)}
g₃₄: 6⋅X₀+8⋅X₂+4 {O(n)}
g₃₆: 3⋅X₀+4⋅X₂+2 {O(n)}
g₃₈: 2 {O(1)}
g₄₁: 2 {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}
g₃₆: inf {Infinity}
g₃₈: inf {Infinity}
g₄₁: inf {Infinity}
Sizebounds
(g₀,l1), X₀: X₀ {O(n)}
(g₀,l1), X₁: X₁ {O(n)}
(g₀,l1), X₂: X₂ {O(n)}
(g₁₁,l2_v1), X₀: X₀ {O(n)}
(g₁₁,l2_v1), X₁: X₁ {O(n)}
(g₁₁,l2_v1), X₂: X₂ {O(n)}
(g₁₄,l1_v1), X₀: 2⋅X₀+1 {O(n)}
(g₁₄,l1_v1), X₁: X₁ {O(n)}
(g₁₄,l1_v1), X₂: X₂ {O(n)}
(g₁₄,l1_v2), X₀: X₀ {O(n)}
(g₁₄,l1_v2), X₁: X₁ {O(n)}
(g₁₄,l1_v2), X₂: X₂ {O(n)}
(g₁₇,l1_v3), X₀: 2⋅X₀+1 {O(n)}
(g₁₇,l1_v3), X₁: X₁ {O(n)}
(g₁₇,l1_v3), X₂: X₂ {O(n)}
(g₁₇,l1_v4), X₀: X₀ {O(n)}
(g₁₇,l1_v4), X₁: X₁ {O(n)}
(g₁₇,l1_v4), X₂: X₂ {O(n)}
(g₁₉,l2_v2), X₀: 2⋅X₀+3 {O(n)}
(g₁₉,l2_v2), X₁: 2⋅X₁ {O(n)}
(g₁₉,l2_v2), X₂: 2⋅X₂ {O(n)}
(g₂₂,l1_v3), X₀: 4⋅X₀+6 {O(n)}
(g₂₂,l1_v3), X₁: 4⋅X₁ {O(n)}
(g₂₂,l1_v3), X₂: 4⋅X₂ {O(n)}
(g₂₂,l1_v5), X₀: 4⋅X₀+6 {O(n)}
(g₂₂,l1_v5), X₁: 4⋅X₁ {O(n)}
(g₂₂,l1_v5), X₂: 4⋅X₂ {O(n)}
(g₂₄,l2_v2), X₀: 2⋅X₀+3 {O(n)}
(g₂₄,l2_v2), X₁: 2⋅X₁ {O(n)}
(g₂₄,l2_v2), X₂: 2⋅X₂ {O(n)}
(g₂₆,l2_v3), X₀: X₀ {O(n)}
(g₂₆,l2_v3), X₁: X₁ {O(n)}
(g₂₆,l2_v3), X₂: X₂ {O(n)}
(g₂₉,l1_v3), X₀: 2⋅X₀+1 {O(n)}
(g₂₉,l1_v3), X₁: X₁ {O(n)}
(g₂₉,l1_v3), X₂: X₂ {O(n)}
(g₂₉,l1_v4), X₀: 2⋅X₀+1 {O(n)}
(g₂₉,l1_v4), X₁: X₁ {O(n)}
(g₂₉,l1_v4), X₂: X₂ {O(n)}
(g₃₁,l2_v4), X₀: 2⋅X₂+4⋅X₀+6 {O(n)}
(g₃₁,l2_v4), X₁: 2⋅X₁ {O(n)}
(g₃₁,l2_v4), X₂: 2⋅X₂ {O(n)}
(g₃₄,l1_v1), X₀: 4⋅X₂+6⋅X₀+4 {O(n)}
(g₃₄,l1_v1), X₁: 4⋅X₁ {O(n)}
(g₃₄,l1_v1), X₂: 4⋅X₂ {O(n)}
(g₃₄,l1_v6), X₀: 4⋅X₂+6⋅X₀+4 {O(n)}
(g₃₄,l1_v6), X₁: 4⋅X₁ {O(n)}
(g₃₄,l1_v6), X₂: 4⋅X₂ {O(n)}
(g₃₆,l2_v4), X₀: 2⋅X₂+4⋅X₀+6 {O(n)}
(g₃₆,l2_v4), X₁: 2⋅X₁ {O(n)}
(g₃₆,l2_v4), X₂: 2⋅X₂ {O(n)}
(g₃₈,l2_v5), X₀: X₀ {O(n)}
(g₃₈,l2_v5), X₁: X₁ {O(n)}
(g₃₈,l2_v5), X₂: X₂ {O(n)}
(g₄₁,l1_v1), X₀: X₀+1 {O(n)}
(g₄₁,l1_v1), X₁: X₁ {O(n)}
(g₄₁,l1_v1), X₂: X₂ {O(n)}
(g₄₁,l1_v2), X₀: X₀ {O(n)}
(g₄₁,l1_v2), X₁: X₁ {O(n)}
(g₄₁,l1_v2), X₂: X₂ {O(n)}
Run probabilistic analysis on SCC: [l1_v3; l1_v5; l2_v2]
Plrf for transition g₂₂:l2_v2(X₀,X₁,X₂) → [1/2]:t₂₀:l1_v3(X₀-1,X₁,X₂) :+: [1/2]:t₂₁:l1_v5(X₀,X₁,X₂) :|: 1 ≤ X₁ ∧ 1+X₀ ≤ X₂ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂:
new bound:
8⋅X₀+8 {O(n)}
PLRF:
• l1_v3: 2+2⋅X₀
• l1_v5: 2+2⋅X₀
• l2_v2: 2+2⋅X₀
Show Graph
G
l0
l0
l1
l1
l0->l1
p = 1
t₁ ∈ g₀
l2_v1
l2_v1
l1->l2_v1
p = 1
t₁₀ ∈ g₁₁
τ = 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v1
l1_v1
l2_v4
l2_v4
l1_v1->l2_v4
p = 1
t₃₀ ∈ g₃₁
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1 ≤ X₀ ∧ X₁ ≤ 0 ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v2
l1_v2
l2_v5
l2_v5
l1_v2->l2_v5
p = 1
t₃₇ ∈ g₃₈
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ X₁ ≤ 0 ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v3
l1_v3
l2_v2
l2_v2
l1_v3->l2_v2
p = 1
t₁₈ ∈ g₁₉
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1+X₀ ≤ X₂ ∧ 1 ≤ X₁ ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v4
l1_v4
l2_v3
l2_v3
l1_v4->l2_v3
p = 1
t₂₅ ∈ g₂₆
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1 ≤ X₁ ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v5
l1_v5
l1_v5->l2_v2
p = 1
t₂₃ ∈ g₂₄
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1+X₀ ≤ X₂ ∧ 1 ≤ X₁ ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v6
l1_v6
l1_v6->l2_v4
p = 1
t₃₅ ∈ g₃₆
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1 ≤ X₀ ∧ X₁ ≤ 0 ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l2_v1->l1_v1
p = 1/2
t₁₂ ∈ g₁₄
η (X₀) = 1+X₀
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v1->l1_v2
p = 1/2
t₁₃ ∈ g₁₄
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v1->l1_v3
p = 1/2
t₁₅ ∈ g₁₇
η (X₀) = X₀-1
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v1->l1_v4
p = 1/2
t₁₆ ∈ g₁₇
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v2->l1_v3
p = 1/2
t₂₀ ∈ g₂₂
η (X₀) = X₀-1
τ = 1+X₀ ≤ X₂ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v2->l1_v5
p = 1/2
t₂₁ ∈ g₂₂
τ = 1+X₀ ≤ X₂ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v3->l1_v3
p = 1/2
t₂₇ ∈ g₂₉
η (X₀) = X₀-1
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v3->l1_v4
p = 1/2
t₂₈ ∈ g₂₉
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v4->l1_v1
p = 1/2
t₃₂ ∈ g₃₄
η (X₀) = 1+X₀
τ = 1 ≤ X₀ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v4->l1_v6
p = 1/2
t₃₃ ∈ g₃₄
τ = 1 ≤ X₀ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v5->l1_v1
p = 1/2
t₃₉ ∈ g₄₁
η (X₀) = 1+X₀
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v5->l1_v2
p = 1/2
t₄₀ ∈ g₄₁
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
Use expected size bounds for entry point (g₁₇:l2_v1→[t₁₅:1/2:l1_v3; t₁₆:1/2:l1_v4],l1_v3)
Use classical time bound for entry point (g₁₇:l2_v1→[t₁₅:1/2:l1_v3; t₁₆:1/2:l1_v4],l1_v3)
Use expected size bounds for entry point (g₂₉:l2_v3→[t₂₇:1/2:l1_v3; t₂₈:1/2:l1_v4],l1_v3)
Use classical time bound for entry point (g₂₉:l2_v3→[t₂₇:1/2:l1_v3; t₂₈:1/2:l1_v4],l1_v3)
Plrf for transition g₂₄:l1_v5(X₀,X₁,X₂) → t₂₃:l2_v2(X₀,X₁,X₂) :|: 0 ≤ X₀ ∧ X₀ ≤ X₂ ∧ 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1+X₀ ≤ X₂ ∧ 1 ≤ X₁ ∧ 0 ≤ X₂:
new bound:
2⋅X₁+4⋅X₀+2 {O(n)}
PLRF:
• l1_v3: X₀+X₁
• l1_v5: 1+X₀+X₁
• l2_v2: X₀+X₁
Show Graph
G
l0
l0
l1
l1
l0->l1
p = 1
t₁ ∈ g₀
l2_v1
l2_v1
l1->l2_v1
p = 1
t₁₀ ∈ g₁₁
τ = 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v1
l1_v1
l2_v4
l2_v4
l1_v1->l2_v4
p = 1
t₃₀ ∈ g₃₁
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1 ≤ X₀ ∧ X₁ ≤ 0 ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v2
l1_v2
l2_v5
l2_v5
l1_v2->l2_v5
p = 1
t₃₇ ∈ g₃₈
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ X₁ ≤ 0 ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v3
l1_v3
l2_v2
l2_v2
l1_v3->l2_v2
p = 1
t₁₈ ∈ g₁₉
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1+X₀ ≤ X₂ ∧ 1 ≤ X₁ ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v4
l1_v4
l2_v3
l2_v3
l1_v4->l2_v3
p = 1
t₂₅ ∈ g₂₆
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1 ≤ X₁ ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v5
l1_v5
l1_v5->l2_v2
p = 1
t₂₃ ∈ g₂₄
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1+X₀ ≤ X₂ ∧ 1 ≤ X₁ ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v6
l1_v6
l1_v6->l2_v4
p = 1
t₃₅ ∈ g₃₆
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1 ≤ X₀ ∧ X₁ ≤ 0 ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l2_v1->l1_v1
p = 1/2
t₁₂ ∈ g₁₄
η (X₀) = 1+X₀
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v1->l1_v2
p = 1/2
t₁₃ ∈ g₁₄
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v1->l1_v3
p = 1/2
t₁₅ ∈ g₁₇
η (X₀) = X₀-1
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v1->l1_v4
p = 1/2
t₁₆ ∈ g₁₇
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v2->l1_v3
p = 1/2
t₂₀ ∈ g₂₂
η (X₀) = X₀-1
τ = 1+X₀ ≤ X₂ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v2->l1_v5
p = 1/2
t₂₁ ∈ g₂₂
τ = 1+X₀ ≤ X₂ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v3->l1_v3
p = 1/2
t₂₇ ∈ g₂₉
η (X₀) = X₀-1
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v3->l1_v4
p = 1/2
t₂₈ ∈ g₂₉
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v4->l1_v1
p = 1/2
t₃₂ ∈ g₃₄
η (X₀) = 1+X₀
τ = 1 ≤ X₀ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v4->l1_v6
p = 1/2
t₃₃ ∈ g₃₄
τ = 1 ≤ X₀ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v5->l1_v1
p = 1/2
t₃₉ ∈ g₄₁
η (X₀) = 1+X₀
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v5->l1_v2
p = 1/2
t₄₀ ∈ g₄₁
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
Use expected size bounds for entry point (g₁₇:l2_v1→[t₁₅:1/2:l1_v3; t₁₆:1/2:l1_v4],l1_v3)
Use expected size bounds for entry point (g₁₇:l2_v1→[t₁₅:1/2:l1_v3; t₁₆:1/2:l1_v4],l1_v3)
Use classical time bound for entry point (g₁₇:l2_v1→[t₁₅:1/2:l1_v3; t₁₆:1/2:l1_v4],l1_v3)
Use expected size bounds for entry point (g₂₉:l2_v3→[t₂₇:1/2:l1_v3; t₂₈:1/2:l1_v4],l1_v3)
Use expected size bounds for entry point (g₂₉:l2_v3→[t₂₇:1/2:l1_v3; t₂₈:1/2:l1_v4],l1_v3)
Use classical time bound for entry point (g₂₉:l2_v3→[t₂₇:1/2:l1_v3; t₂₈:1/2:l1_v4],l1_v3)
CFR: Improvement to new bound with the following program:
method: PartialEvaluationProbabilistic new bound:
O(n)
cfr-program:
Start: l0
Program_Vars: X₀, X₁, X₂
Temp_Vars:
Locations: l0, l1, l1_v1, l1_v2, l1_v3, l1_v4, l1_v5, l1_v6, l2_v1, l2_v2, l2_v3, l2_v4, l2_v5
Transitions:
g₀:l0(X₀,X₁,X₂) → t₁:l1(X₀,X₁,X₂) :|:
g₁₁:l1(X₀,X₁,X₂) → t₁₀:l2_v1(X₀,X₁,X₂) :|: 0 ≤ X₀ ∧ X₀ ≤ X₂
g₁₄:l2_v1(X₀,X₁,X₂) → [1/2]:t₁₂:l1_v1(1+X₀,X₁,X₂) :+: [1/2]:t₁₃:l1_v2(X₀,X₁,X₂) :|: X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂
g₁₇:l2_v1(X₀,X₁,X₂) → [1/2]:t₁₅:l1_v3(X₀-1,X₁,X₂) :+: [1/2]:t₁₆:l1_v4(X₀,X₁,X₂) :|: 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂
g₁₉:l1_v3(X₀,X₁,X₂) → t₁₈:l2_v2(X₀,X₁,X₂) :|: 0 ≤ X₀ ∧ X₀ ≤ X₂ ∧ 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1+X₀ ≤ X₂ ∧ 1 ≤ X₁ ∧ 0 ≤ X₂
g₂₂:l2_v2(X₀,X₁,X₂) → [1/2]:t₂₀:l1_v3(X₀-1,X₁,X₂) :+: [1/2]:t₂₁:l1_v5(X₀,X₁,X₂) :|: 1 ≤ X₁ ∧ 1+X₀ ≤ X₂ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂
g₂₄:l1_v5(X₀,X₁,X₂) → t₂₃:l2_v2(X₀,X₁,X₂) :|: 0 ≤ X₀ ∧ X₀ ≤ X₂ ∧ 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1+X₀ ≤ X₂ ∧ 1 ≤ X₁ ∧ 0 ≤ X₂
g₂₆:l1_v4(X₀,X₁,X₂) → t₂₅:l2_v3(X₀,X₁,X₂) :|: 0 ≤ X₀ ∧ X₀ ≤ X₂ ∧ 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1 ≤ X₁ ∧ 0 ≤ X₂
g₂₉:l2_v3(X₀,X₁,X₂) → [1/2]:t₂₇:l1_v3(X₀-1,X₁,X₂) :+: [1/2]:t₂₈:l1_v4(X₀,X₁,X₂) :|: 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂
g₃₁:l1_v1(X₀,X₁,X₂) → t₃₀:l2_v4(X₀,X₁,X₂) :|: 0 ≤ X₀ ∧ X₀ ≤ X₂ ∧ 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1 ≤ X₀ ∧ X₁ ≤ 0 ∧ 0 ≤ X₂
g₃₄:l2_v4(X₀,X₁,X₂) → [1/2]:t₃₂:l1_v1(1+X₀,X₁,X₂) :+: [1/2]:t₃₃:l1_v6(X₀,X₁,X₂) :|: X₁ ≤ 0 ∧ 1 ≤ X₀ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂
g₃₆:l1_v6(X₀,X₁,X₂) → t₃₅:l2_v4(X₀,X₁,X₂) :|: 0 ≤ X₀ ∧ X₀ ≤ X₂ ∧ 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1 ≤ X₀ ∧ X₁ ≤ 0 ∧ 0 ≤ X₂
g₃₈:l1_v2(X₀,X₁,X₂) → t₃₇:l2_v5(X₀,X₁,X₂) :|: 0 ≤ X₀ ∧ X₀ ≤ X₂ ∧ 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ X₁ ≤ 0 ∧ 0 ≤ X₂
g₄₁:l2_v5(X₀,X₁,X₂) → [1/2]:t₃₉:l1_v1(1+X₀,X₁,X₂) :+: [1/2]:t₄₀:l1_v2(X₀,X₁,X₂) :|: X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂
Show Graph
G
l0
l0
l1
l1
l0->l1
t₁ ∈ g₀
l2_v1
l2_v1
l1->l2_v1
t₁₀ ∈ g₁₁
τ = 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v1
l1_v1
l2_v4
l2_v4
l1_v1->l2_v4
t₃₀ ∈ g₃₁
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1 ≤ X₀ ∧ X₁ ≤ 0 ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v2
l1_v2
l2_v5
l2_v5
l1_v2->l2_v5
t₃₇ ∈ g₃₈
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ X₁ ≤ 0 ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v3
l1_v3
l2_v2
l2_v2
l1_v3->l2_v2
t₁₈ ∈ g₁₉
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1+X₀ ≤ X₂ ∧ 1 ≤ X₁ ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v4
l1_v4
l2_v3
l2_v3
l1_v4->l2_v3
t₂₅ ∈ g₂₆
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1 ≤ X₁ ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v5
l1_v5
l1_v5->l2_v2
t₂₃ ∈ g₂₄
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1+X₀ ≤ X₂ ∧ 1 ≤ X₁ ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l1_v6
l1_v6
l1_v6->l2_v4
t₃₅ ∈ g₃₆
τ = 0 ≤ 1+X₀ ∧ X₀ ≤ 1+X₂ ∧ 1 ≤ X₀ ∧ X₁ ≤ 0 ∧ 0 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₂
l2_v1->l1_v1
t₁₂ ∈ g₁₄
η (X₀) = 1+X₀
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v1->l1_v2
t₁₃ ∈ g₁₄
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v1->l1_v3
t₁₅ ∈ g₁₇
η (X₀) = X₀-1
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v1->l1_v4
t₁₆ ∈ g₁₇
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v2->l1_v3
t₂₀ ∈ g₂₂
η (X₀) = X₀-1
τ = 1+X₀ ≤ X₂ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v2->l1_v5
t₂₁ ∈ g₂₂
τ = 1+X₀ ≤ X₂ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v3->l1_v3
t₂₇ ∈ g₂₉
η (X₀) = X₀-1
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v3->l1_v4
t₂₈ ∈ g₂₉
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₁
l2_v4->l1_v1
t₃₂ ∈ g₃₄
η (X₀) = 1+X₀
τ = 1 ≤ X₀ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v4->l1_v6
t₃₃ ∈ g₃₄
τ = 1 ≤ X₀ ∧ 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v5->l1_v1
t₃₉ ∈ g₄₁
η (X₀) = 1+X₀
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
l2_v5->l1_v2
t₄₀ ∈ g₄₁
τ = 0 ≤ X₀ ∧ 0 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 0 ≤ X₂ ∧ X₁ ≤ 0
Results of Probabilistic Analysis
All Bounds
Timebounds
Overall timebound:14⋅X₂+25⋅X₀+5⋅X₁+37 {O(n)}
g₀: 1 {O(1)}
g₁₁: 1 {O(1)}
g₁₄: 2 {O(1)}
g₁₇: 2 {O(1)}
g₁₉: 2⋅X₀+6 {O(n)}
g₂₂: 8⋅X₀+8 {O(n)}
g₂₄: 2⋅X₁+4⋅X₀+2 {O(n)}
g₂₆: X₁+1 {O(n)}
g₂₉: 2⋅X₁ {O(n)}
g₃₁: 2⋅X₀+2⋅X₂+4 {O(n)}
g₃₄: 6⋅X₀+8⋅X₂+4 {O(n)}
g₃₆: 3⋅X₀+4⋅X₂+2 {O(n)}
g₃₈: 2 {O(1)}
g₄₁: 2 {O(1)}
Costbounds
Overall costbound: 22⋅X₂+39⋅X₀+7⋅X₁+55 {O(n)}
g₀: 1 {O(1)}
g₁₁: 1 {O(1)}
g₁₄: 4 {O(1)}
g₁₇: 4 {O(1)}
g₁₉: 2⋅X₀+6 {O(n)}
g₂₂: 16⋅X₀+16 {O(n)}
g₂₄: 2⋅X₁+4⋅X₀+2 {O(n)}
g₂₆: X₁+1 {O(n)}
g₂₉: 4⋅X₁ {O(n)}
g₃₁: 2⋅X₀+2⋅X₂+4 {O(n)}
g₃₄: 12⋅X₀+16⋅X₂+8 {O(n)}
g₃₆: 3⋅X₀+4⋅X₂+2 {O(n)}
g₃₈: 2 {O(1)}
g₄₁: 4 {O(1)}
Sizebounds
(g₀,l1), X₀: X₀ {O(n)}
(g₀,l1), X₁: X₁ {O(n)}
(g₀,l1), X₂: X₂ {O(n)}
(g₁₁,l2_v1), X₀: X₀ {O(n)}
(g₁₁,l2_v1), X₁: X₁ {O(n)}
(g₁₁,l2_v1), X₂: X₂ {O(n)}
(g₁₄,l1_v1), X₀: 2⋅X₀+1 {O(n)}
(g₁₄,l1_v1), X₁: X₁ {O(n)}
(g₁₄,l1_v1), X₂: X₂ {O(n)}
(g₁₄,l1_v2), X₀: X₀ {O(n)}
(g₁₄,l1_v2), X₁: X₁ {O(n)}
(g₁₄,l1_v2), X₂: X₂ {O(n)}
(g₁₇,l1_v3), X₀: 2⋅X₀+1 {O(n)}
(g₁₇,l1_v3), X₁: X₁ {O(n)}
(g₁₇,l1_v3), X₂: X₂ {O(n)}
(g₁₇,l1_v4), X₀: X₀ {O(n)}
(g₁₇,l1_v4), X₁: X₁ {O(n)}
(g₁₇,l1_v4), X₂: X₂ {O(n)}
(g₁₉,l2_v2), X₀: 2⋅X₀+3 {O(n)}
(g₁₉,l2_v2), X₁: 2⋅X₁ {O(n)}
(g₁₉,l2_v2), X₂: 2⋅X₂ {O(n)}
(g₂₂,l1_v3), X₀: 4⋅X₀+6 {O(n)}
(g₂₂,l1_v3), X₁: 4⋅X₁ {O(n)}
(g₂₂,l1_v3), X₂: 4⋅X₂ {O(n)}
(g₂₂,l1_v5), X₀: 4⋅X₀+6 {O(n)}
(g₂₂,l1_v5), X₁: 4⋅X₁ {O(n)}
(g₂₂,l1_v5), X₂: 4⋅X₂ {O(n)}
(g₂₄,l2_v2), X₀: 2⋅X₀+3 {O(n)}
(g₂₄,l2_v2), X₁: 2⋅X₁ {O(n)}
(g₂₄,l2_v2), X₂: 2⋅X₂ {O(n)}
(g₂₆,l2_v3), X₀: X₀ {O(n)}
(g₂₆,l2_v3), X₁: X₁ {O(n)}
(g₂₆,l2_v3), X₂: X₂ {O(n)}
(g₂₉,l1_v3), X₀: 2⋅X₀+1 {O(n)}
(g₂₉,l1_v3), X₁: X₁ {O(n)}
(g₂₉,l1_v3), X₂: X₂ {O(n)}
(g₂₉,l1_v4), X₀: X₀ {O(n)}
(g₂₉,l1_v4), X₁: X₁ {O(n)}
(g₂₉,l1_v4), X₂: X₂ {O(n)}
(g₃₁,l2_v4), X₀: 2⋅X₂+4⋅X₀+6 {O(n)}
(g₃₁,l2_v4), X₁: 2⋅X₁ {O(n)}
(g₃₁,l2_v4), X₂: 2⋅X₂ {O(n)}
(g₃₄,l1_v1), X₀: 4⋅X₂+6⋅X₀+4 {O(n)}
(g₃₄,l1_v1), X₁: 4⋅X₁ {O(n)}
(g₃₄,l1_v1), X₂: 4⋅X₂ {O(n)}
(g₃₄,l1_v6), X₀: 4⋅X₂+6⋅X₀+4 {O(n)}
(g₃₄,l1_v6), X₁: 4⋅X₁ {O(n)}
(g₃₄,l1_v6), X₂: 4⋅X₂ {O(n)}
(g₃₆,l2_v4), X₀: 2⋅X₂+4⋅X₀+6 {O(n)}
(g₃₆,l2_v4), X₁: 2⋅X₁ {O(n)}
(g₃₆,l2_v4), X₂: 2⋅X₂ {O(n)}
(g₃₈,l2_v5), X₀: X₀ {O(n)}
(g₃₈,l2_v5), X₁: X₁ {O(n)}
(g₃₈,l2_v5), X₂: X₂ {O(n)}
(g₄₁,l1_v1), X₀: X₀+1 {O(n)}
(g₄₁,l1_v1), X₁: X₁ {O(n)}
(g₄₁,l1_v1), X₂: X₂ {O(n)}
(g₄₁,l1_v2), X₀: X₀ {O(n)}
(g₄₁,l1_v2), X₁: X₁ {O(n)}
(g₄₁,l1_v2), X₂: X₂ {O(n)}