Preprocessing
Eliminate variables [X₄] that do not contribute to the problem
Found invariant 1+X₂ ≤ X₃ for location h
Probabilistic Analysis
Probabilistic Program after Preprocessing
Start: f
Program_Vars: X₀, X₁, X₂, X₃, X₄
Temp_Vars:
Locations: f, g, h
Transitions:
g₀:f(X₀,X₁,X₂,X₃,X₄) -{0}> t₁:g(X₀,X₁,X₂,X₃,X₄) :|:
g₂:g(X₀,X₁,X₂,X₃,X₄) -{0}> t₃:h(X₀,X₁,X₂,X₃,X₄) :|: 1+X₂ ≤ X₃
g₄:h(X₀,X₁,X₂,X₃,X₄) → [1/4]:t₅:g(2+X₀,X₁,2+X₂,X₃,X₄) :+: [1/4]:t₆:g(X₀,2+X₁,2+X₂,X₃,X₄) :+: [1/4]:t₇:g(X₀-1,X₁,X₂-1,X₃,X₄) :+: [1/4]:t₈:g(X₀,X₁-1,X₂-1,X₃,X₄) :|: 1 ≤ X₀ ∧ 1 ≤ X₁ ∧ 1+X₂ ≤ X₃
g₉:h(X₀,X₁,X₂,X₃,X₄) → [1/4]:t₁₀:g(2+X₀,X₁,2+X₂,X₃,X₄) :+: [1/4]:t₁₁:g(X₀,1+X₁,X₂-1,X₃,X₄) :+: [1/4]:t₁₂:g(X₀-1,X₁,X₂-1,X₃,X₄) :+: [1/4]:t₁₃:g(X₀,X₁-2,2+X₂,X₃,X₄) :|: 1 ≤ X₀ ∧ 1+X₁ ≤ 0 ∧ 1+X₂ ≤ X₃
g₁₄:h(X₀,X₁,X₂,X₃,X₄) → [1/4]:t₁₅:g(2+X₀,X₁,2+X₂,X₃,X₄) :+: [1/4]:t₁₆:g(X₀,1+X₁,1+X₂,X₃,X₄) :+: [1/4]:t₁₇:g(X₀-1,X₁,X₂-1,X₃,X₄) :+: [1/4]:t₁₈:g(X₀,X₁-1,1+X₂,X₃,X₄) :|: 1 ≤ X₀ ∧ 0 ≤ X₁ ∧ X₁ ≤ 0 ∧ 1+X₂ ≤ X₃
g₁₉:h(X₀,X₁,X₂,X₃,X₄) → [1/4]:t₂₀:g(1+X₀,X₁,X₂-1,X₃,X₄) :+: [1/4]:t₂₁:g(X₀,2+X₁,2+X₂,X₃,X₄) :+: [1/4]:t₂₂:g(X₀-2,X₁,2+X₂,X₃,X₄) :+: [1/4]:t₂₃:g(X₀,X₁-1,X₂-1,X₃,X₄) :|: 1+X₀ ≤ 0 ∧ 1 ≤ X₁ ∧ 1+X₂ ≤ X₃
g₂₄:h(X₀,X₁,X₂,X₃,X₄) → [1/4]:t₂₅:g(1+X₀,X₁,X₂-1,X₃,X₄) :+: [1/4]:t₂₆:g(X₀,1+X₁,X₂-1,X₃,X₄) :+: [1/4]:t₂₇:g(X₀-2,X₁,2+X₂,X₃,X₄) :+: [1/4]:t₂₈:g(X₀,X₁-2,2+X₂,X₃,X₄) :|: 1+X₀ ≤ 0 ∧ 1+X₁ ≤ 0 ∧ 1+X₂ ≤ X₃
g₂₉:h(X₀,X₁,X₂,X₃,X₄) → [1/4]:t₃₀:g(1+X₀,X₁,X₂-1,X₃,X₄) :+: [1/4]:t₃₁:g(X₀,1+X₁,1+X₂,X₃,X₄) :+: [1/4]:t₃₂:g(X₀-2,X₁,2+X₂,X₃,X₄) :+: [1/4]:t₃₃:g(X₀,X₁-1,1+X₂,X₃,X₄) :|: 1+X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0 ∧ 1+X₂ ≤ X₃
g₃₄:h(X₀,X₁,X₂,X₃,X₄) → [1/4]:t₃₅:g(1+X₀,X₁,1+X₂,X₃,X₄) :+: [1/4]:t₃₆:g(X₀,2+X₁,2+X₂,X₃,X₄) :+: [1/4]:t₃₇:g(X₀-1,X₁,1+X₂,X₃,X₄) :+: [1/4]:t₃₈:g(X₀,X₁-1,X₂-1,X₃,X₄) :|: 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 1+X₂ ≤ X₃
g₃₉:h(X₀,X₁,X₂,X₃,X₄) → [1/4]:t₄₀:g(1+X₀,X₁,1+X₂,X₃,X₄) :+: [1/4]:t₄₁:g(X₀,1+X₁,X₂-1,X₃,X₄) :+: [1/4]:t₄₂:g(X₀-1,X₁,1+X₂,X₃,X₄) :+: [1/4]:t₄₃:g(X₀,X₁-2,2+X₂,X₃,X₄) :|: 1+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 1+X₂ ≤ X₃
g₄₄:h(X₀,X₁,X₂,X₃,X₄) → [1/4]:t₄₅:g(1+X₀,X₁,1+X₂,X₃,X₄) :+: [1/4]:t₄₆:g(X₀,1+X₁,1+X₂,X₃,X₄) :+: [1/4]:t₄₇:g(X₀-1,X₁,1+X₂,X₃,X₄) :+: [1/4]:t₄₈:g(X₀,X₁-1,1+X₂,X₃,X₄) :|: 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0 ∧ 1+X₂ ≤ X₃
Show Graph
G
f
f
g
g
f->g
p = 1
t₁ ∈ g₀
{0}
h
h
g->h
p = 1
t₃ ∈ g₂
τ = 1+X₂ ≤ X₃
{0}
h->g
p = 1/4
t₅ ∈ g₄
η (X₀) = 2+X₀
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1 ≤ X₁
h->g
p = 1/4
t₆ ∈ g₄
η (X₁) = 2+X₁
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1 ≤ X₁
h->g
p = 1/4
t₇ ∈ g₄
η (X₀) = X₀-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1 ≤ X₁
h->g
p = 1/4
t₈ ∈ g₄
η (X₁) = X₁-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1 ≤ X₁
h->g
p = 1/4
t₁₀ ∈ g₉
η (X₀) = 2+X₀
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₁₁ ∈ g₉
η (X₁) = 1+X₁
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₁₂ ∈ g₉
η (X₀) = X₀-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₁₃ ∈ g₉
η (X₁) = X₁-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₁₅ ∈ g₁₄
η (X₀) = 2+X₀
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₁₆ ∈ g₁₄
η (X₁) = 1+X₁
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₁₇ ∈ g₁₄
η (X₀) = X₀-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₁₈ ∈ g₁₄
η (X₁) = X₁-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₂₀ ∈ g₁₉
η (X₀) = 1+X₀
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1 ≤ X₁
h->g
p = 1/4
t₂₁ ∈ g₁₉
η (X₁) = 2+X₁
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1 ≤ X₁
h->g
p = 1/4
t₂₂ ∈ g₁₉
η (X₀) = X₀-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1 ≤ X₁
h->g
p = 1/4
t₂₃ ∈ g₁₉
η (X₁) = X₁-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1 ≤ X₁
h->g
p = 1/4
t₂₅ ∈ g₂₄
η (X₀) = 1+X₀
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₂₆ ∈ g₂₄
η (X₁) = 1+X₁
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₂₇ ∈ g₂₄
η (X₀) = X₀-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₂₈ ∈ g₂₄
η (X₁) = X₁-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₃₀ ∈ g₂₉
η (X₀) = 1+X₀
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₃₁ ∈ g₂₉
η (X₁) = 1+X₁
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₃₂ ∈ g₂₉
η (X₀) = X₀-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₃₃ ∈ g₂₉
η (X₁) = X₁-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₃₅ ∈ g₃₄
η (X₀) = 1+X₀
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₃₆ ∈ g₃₄
η (X₁) = 2+X₁
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₃₇ ∈ g₃₄
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₃₈ ∈ g₃₄
η (X₁) = X₁-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₄₀ ∈ g₃₉
η (X₀) = 1+X₀
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₄₁ ∈ g₃₉
η (X₁) = 1+X₁
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₄₂ ∈ g₃₉
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₄₃ ∈ g₃₉
η (X₁) = X₁-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₄₅ ∈ g₄₄
η (X₀) = 1+X₀
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₄₆ ∈ g₄₄
η (X₁) = 1+X₁
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₄₇ ∈ g₄₄
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₄₈ ∈ g₄₄
η (X₁) = X₁-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 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₂: 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}
Sizebounds
(g₀,g), X₀: X₀ {O(n)}
(g₀,g), X₁: X₁ {O(n)}
(g₀,g), X₂: X₂ {O(n)}
(g₀,g), X₃: X₃ {O(n)}
(g₀,g), X₄: X₄ {O(n)}
Run probabilistic analysis on SCC: [f]
Run classical analysis on SCC: [g; h]
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}
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}
Sizebounds
(g₀,g), X₀: X₀ {O(n)}
(g₀,g), X₁: X₁ {O(n)}
(g₀,g), X₂: X₂ {O(n)}
(g₀,g), X₃: X₃ {O(n)}
(g₀,g), X₄: X₄ {O(n)}
(g₂,h), X₃: X₃ {O(n)}
(g₂,h), X₄: X₄ {O(n)}
(g₄,g), X₃: 4⋅X₃ {O(n)}
(g₄,g), X₄: 4⋅X₄ {O(n)}
(g₉,g), X₃: 4⋅X₃ {O(n)}
(g₉,g), X₄: 4⋅X₄ {O(n)}
(g₁₄,g), X₁: 2 {O(1)}
(g₁₄,g), X₃: 4⋅X₃ {O(n)}
(g₁₄,g), X₄: 4⋅X₄ {O(n)}
(g₁₉,g), X₃: 4⋅X₃ {O(n)}
(g₁₉,g), X₄: 4⋅X₄ {O(n)}
(g₂₄,g), X₃: 4⋅X₃ {O(n)}
(g₂₄,g), X₄: 4⋅X₄ {O(n)}
(g₂₉,g), X₁: 2 {O(1)}
(g₂₉,g), X₃: 4⋅X₃ {O(n)}
(g₂₉,g), X₄: 4⋅X₄ {O(n)}
(g₃₄,g), X₀: 2 {O(1)}
(g₃₄,g), X₃: 4⋅X₃ {O(n)}
(g₃₄,g), X₄: 4⋅X₄ {O(n)}
(g₃₉,g), X₀: 2 {O(1)}
(g₃₉,g), X₃: 4⋅X₃ {O(n)}
(g₃₉,g), X₄: 4⋅X₄ {O(n)}
(g₄₄,g), X₀: 2 {O(1)}
(g₄₄,g), X₁: 2 {O(1)}
(g₄₄,g), X₃: 4⋅X₃ {O(n)}
(g₄₄,g), X₄: 4⋅X₄ {O(n)}
Run probabilistic analysis on SCC: [g; h]
Plrf for transition g₂:g(X₀,X₁,X₂,X₃,X₄) -{0}> t₃:h(X₀,X₁,X₂,X₃,X₄) :|: 1+X₂ ≤ X₃:
new bound:
2⋅X₂+2⋅X₃+2 {O(n)}
PLRF:
• g: 2+2⋅X₃-2⋅X₂
• h: 1+2⋅X₃-2⋅X₂
Show Graph
G
f
f
g
g
f->g
p = 1
t₁ ∈ g₀
{0}
h
h
g->h
p = 1
t₃ ∈ g₂
τ = 1+X₂ ≤ X₃
{0}
h->g
p = 1/4
t₅ ∈ g₄
η (X₀) = 2+X₀
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1 ≤ X₁
h->g
p = 1/4
t₆ ∈ g₄
η (X₁) = 2+X₁
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1 ≤ X₁
h->g
p = 1/4
t₇ ∈ g₄
η (X₀) = X₀-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1 ≤ X₁
h->g
p = 1/4
t₈ ∈ g₄
η (X₁) = X₁-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1 ≤ X₁
h->g
p = 1/4
t₁₀ ∈ g₉
η (X₀) = 2+X₀
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₁₁ ∈ g₉
η (X₁) = 1+X₁
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₁₂ ∈ g₉
η (X₀) = X₀-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₁₃ ∈ g₉
η (X₁) = X₁-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₁₅ ∈ g₁₄
η (X₀) = 2+X₀
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₁₆ ∈ g₁₄
η (X₁) = 1+X₁
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₁₇ ∈ g₁₄
η (X₀) = X₀-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₁₈ ∈ g₁₄
η (X₁) = X₁-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₂₀ ∈ g₁₉
η (X₀) = 1+X₀
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1 ≤ X₁
h->g
p = 1/4
t₂₁ ∈ g₁₉
η (X₁) = 2+X₁
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1 ≤ X₁
h->g
p = 1/4
t₂₂ ∈ g₁₉
η (X₀) = X₀-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1 ≤ X₁
h->g
p = 1/4
t₂₃ ∈ g₁₉
η (X₁) = X₁-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1 ≤ X₁
h->g
p = 1/4
t₂₅ ∈ g₂₄
η (X₀) = 1+X₀
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₂₆ ∈ g₂₄
η (X₁) = 1+X₁
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₂₇ ∈ g₂₄
η (X₀) = X₀-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₂₈ ∈ g₂₄
η (X₁) = X₁-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₃₀ ∈ g₂₉
η (X₀) = 1+X₀
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₃₁ ∈ g₂₉
η (X₁) = 1+X₁
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₃₂ ∈ g₂₉
η (X₀) = X₀-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₃₃ ∈ g₂₉
η (X₁) = X₁-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₃₅ ∈ g₃₄
η (X₀) = 1+X₀
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₃₆ ∈ g₃₄
η (X₁) = 2+X₁
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₃₇ ∈ g₃₄
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₃₈ ∈ g₃₄
η (X₁) = X₁-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₄₀ ∈ g₃₉
η (X₀) = 1+X₀
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₄₁ ∈ g₃₉
η (X₁) = 1+X₁
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₄₂ ∈ g₃₉
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₄₃ ∈ g₃₉
η (X₁) = X₁-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₄₅ ∈ g₄₄
η (X₀) = 1+X₀
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₄₆ ∈ g₄₄
η (X₁) = 1+X₁
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₄₇ ∈ g₄₄
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₄₈ ∈ g₄₄
η (X₁) = X₁-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
Use expected size bounds for entry point (g₀:f→[t₁:1:g],g)
Use expected size bounds for entry point (g₀:f→[t₁:1:g],g)
Use classical time bound for entry point (g₀:f→[t₁:1:g],g)
Plrf for transition g₄:h(X₀,X₁,X₂,X₃,X₄) → [1/4]:t₅:g(2+X₀,X₁,2+X₂,X₃,X₄) :+: [1/4]:t₆:g(X₀,2+X₁,2+X₂,X₃,X₄) :+: [1/4]:t₇:g(X₀-1,X₁,X₂-1,X₃,X₄) :+: [1/4]:t₈:g(X₀,X₁-1,X₂-1,X₃,X₄) :|: 1 ≤ X₀ ∧ 1 ≤ X₁ ∧ 1+X₂ ≤ X₃:
new bound:
2⋅X₂+2⋅X₃+2 {O(n)}
PLRF:
• g: 2+2⋅X₃-2⋅X₂
• h: 2+2⋅X₃-2⋅X₂
Show Graph
G
f
f
g
g
f->g
p = 1
t₁ ∈ g₀
{0}
h
h
g->h
p = 1
t₃ ∈ g₂
τ = 1+X₂ ≤ X₃
{0}
h->g
p = 1/4
t₅ ∈ g₄
η (X₀) = 2+X₀
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1 ≤ X₁
h->g
p = 1/4
t₆ ∈ g₄
η (X₁) = 2+X₁
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1 ≤ X₁
h->g
p = 1/4
t₇ ∈ g₄
η (X₀) = X₀-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1 ≤ X₁
h->g
p = 1/4
t₈ ∈ g₄
η (X₁) = X₁-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1 ≤ X₁
h->g
p = 1/4
t₁₀ ∈ g₉
η (X₀) = 2+X₀
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₁₁ ∈ g₉
η (X₁) = 1+X₁
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₁₂ ∈ g₉
η (X₀) = X₀-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₁₃ ∈ g₉
η (X₁) = X₁-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₁₅ ∈ g₁₄
η (X₀) = 2+X₀
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₁₆ ∈ g₁₄
η (X₁) = 1+X₁
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₁₇ ∈ g₁₄
η (X₀) = X₀-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₁₈ ∈ g₁₄
η (X₁) = X₁-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₂₀ ∈ g₁₉
η (X₀) = 1+X₀
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1 ≤ X₁
h->g
p = 1/4
t₂₁ ∈ g₁₉
η (X₁) = 2+X₁
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1 ≤ X₁
h->g
p = 1/4
t₂₂ ∈ g₁₉
η (X₀) = X₀-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1 ≤ X₁
h->g
p = 1/4
t₂₃ ∈ g₁₉
η (X₁) = X₁-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1 ≤ X₁
h->g
p = 1/4
t₂₅ ∈ g₂₄
η (X₀) = 1+X₀
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₂₆ ∈ g₂₄
η (X₁) = 1+X₁
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₂₇ ∈ g₂₄
η (X₀) = X₀-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₂₈ ∈ g₂₄
η (X₁) = X₁-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₃₀ ∈ g₂₉
η (X₀) = 1+X₀
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₃₁ ∈ g₂₉
η (X₁) = 1+X₁
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₃₂ ∈ g₂₉
η (X₀) = X₀-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₃₃ ∈ g₂₉
η (X₁) = X₁-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₃₅ ∈ g₃₄
η (X₀) = 1+X₀
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₃₆ ∈ g₃₄
η (X₁) = 2+X₁
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₃₇ ∈ g₃₄
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₃₈ ∈ g₃₄
η (X₁) = X₁-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₄₀ ∈ g₃₉
η (X₀) = 1+X₀
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₄₁ ∈ g₃₉
η (X₁) = 1+X₁
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₄₂ ∈ g₃₉
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₄₃ ∈ g₃₉
η (X₁) = X₁-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₄₅ ∈ g₄₄
η (X₀) = 1+X₀
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₄₆ ∈ g₄₄
η (X₁) = 1+X₁
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₄₇ ∈ g₄₄
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₄₈ ∈ g₄₄
η (X₁) = X₁-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
Use expected size bounds for entry point (g₀:f→[t₁:1:g],g)
Use expected size bounds for entry point (g₀:f→[t₁:1:g],g)
Use classical time bound for entry point (g₀:f→[t₁:1:g],g)
Plrf for transition g₉:h(X₀,X₁,X₂,X₃,X₄) → [1/4]:t₁₀:g(2+X₀,X₁,2+X₂,X₃,X₄) :+: [1/4]:t₁₁:g(X₀,1+X₁,X₂-1,X₃,X₄) :+: [1/4]:t₁₂:g(X₀-1,X₁,X₂-1,X₃,X₄) :+: [1/4]:t₁₃:g(X₀,X₁-2,2+X₂,X₃,X₄) :|: 1 ≤ X₀ ∧ 1+X₁ ≤ 0 ∧ 1+X₂ ≤ X₃:
new bound:
2⋅X₂+2⋅X₃+2 {O(n)}
PLRF:
• g: 2+2⋅X₃-2⋅X₂
• h: 2+2⋅X₃-2⋅X₂
Show Graph
G
f
f
g
g
f->g
p = 1
t₁ ∈ g₀
{0}
h
h
g->h
p = 1
t₃ ∈ g₂
τ = 1+X₂ ≤ X₃
{0}
h->g
p = 1/4
t₅ ∈ g₄
η (X₀) = 2+X₀
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1 ≤ X₁
h->g
p = 1/4
t₆ ∈ g₄
η (X₁) = 2+X₁
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1 ≤ X₁
h->g
p = 1/4
t₇ ∈ g₄
η (X₀) = X₀-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1 ≤ X₁
h->g
p = 1/4
t₈ ∈ g₄
η (X₁) = X₁-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1 ≤ X₁
h->g
p = 1/4
t₁₀ ∈ g₉
η (X₀) = 2+X₀
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₁₁ ∈ g₉
η (X₁) = 1+X₁
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₁₂ ∈ g₉
η (X₀) = X₀-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₁₃ ∈ g₉
η (X₁) = X₁-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₁₅ ∈ g₁₄
η (X₀) = 2+X₀
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₁₆ ∈ g₁₄
η (X₁) = 1+X₁
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₁₇ ∈ g₁₄
η (X₀) = X₀-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₁₈ ∈ g₁₄
η (X₁) = X₁-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₂₀ ∈ g₁₉
η (X₀) = 1+X₀
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1 ≤ X₁
h->g
p = 1/4
t₂₁ ∈ g₁₉
η (X₁) = 2+X₁
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1 ≤ X₁
h->g
p = 1/4
t₂₂ ∈ g₁₉
η (X₀) = X₀-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1 ≤ X₁
h->g
p = 1/4
t₂₃ ∈ g₁₉
η (X₁) = X₁-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1 ≤ X₁
h->g
p = 1/4
t₂₅ ∈ g₂₄
η (X₀) = 1+X₀
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₂₆ ∈ g₂₄
η (X₁) = 1+X₁
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₂₇ ∈ g₂₄
η (X₀) = X₀-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₂₈ ∈ g₂₄
η (X₁) = X₁-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₃₀ ∈ g₂₉
η (X₀) = 1+X₀
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₃₁ ∈ g₂₉
η (X₁) = 1+X₁
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₃₂ ∈ g₂₉
η (X₀) = X₀-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₃₃ ∈ g₂₉
η (X₁) = X₁-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₃₅ ∈ g₃₄
η (X₀) = 1+X₀
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₃₆ ∈ g₃₄
η (X₁) = 2+X₁
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₃₇ ∈ g₃₄
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₃₈ ∈ g₃₄
η (X₁) = X₁-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₄₀ ∈ g₃₉
η (X₀) = 1+X₀
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₄₁ ∈ g₃₉
η (X₁) = 1+X₁
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₄₂ ∈ g₃₉
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₄₃ ∈ g₃₉
η (X₁) = X₁-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₄₅ ∈ g₄₄
η (X₀) = 1+X₀
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₄₆ ∈ g₄₄
η (X₁) = 1+X₁
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₄₇ ∈ g₄₄
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₄₈ ∈ g₄₄
η (X₁) = X₁-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
Use expected size bounds for entry point (g₀:f→[t₁:1:g],g)
Use expected size bounds for entry point (g₀:f→[t₁:1:g],g)
Use classical time bound for entry point (g₀:f→[t₁:1:g],g)
Plrf for transition g₁₄:h(X₀,X₁,X₂,X₃,X₄) → [1/4]:t₁₅:g(2+X₀,X₁,2+X₂,X₃,X₄) :+: [1/4]:t₁₆:g(X₀,1+X₁,1+X₂,X₃,X₄) :+: [1/4]:t₁₇:g(X₀-1,X₁,X₂-1,X₃,X₄) :+: [1/4]:t₁₈:g(X₀,X₁-1,1+X₂,X₃,X₄) :|: 1 ≤ X₀ ∧ 0 ≤ X₁ ∧ X₁ ≤ 0 ∧ 1+X₂ ≤ X₃:
new bound:
4/3⋅X₂+4/3⋅X₃+4/3 {O(n)}
PLRF:
• g: 4/3+4/3⋅X₃-4/3⋅X₂
• h: 4/3+4/3⋅X₃-4/3⋅X₂
Show Graph
G
f
f
g
g
f->g
p = 1
t₁ ∈ g₀
{0}
h
h
g->h
p = 1
t₃ ∈ g₂
τ = 1+X₂ ≤ X₃
{0}
h->g
p = 1/4
t₅ ∈ g₄
η (X₀) = 2+X₀
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1 ≤ X₁
h->g
p = 1/4
t₆ ∈ g₄
η (X₁) = 2+X₁
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1 ≤ X₁
h->g
p = 1/4
t₇ ∈ g₄
η (X₀) = X₀-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1 ≤ X₁
h->g
p = 1/4
t₈ ∈ g₄
η (X₁) = X₁-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1 ≤ X₁
h->g
p = 1/4
t₁₀ ∈ g₉
η (X₀) = 2+X₀
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₁₁ ∈ g₉
η (X₁) = 1+X₁
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₁₂ ∈ g₉
η (X₀) = X₀-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₁₃ ∈ g₉
η (X₁) = X₁-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₁₅ ∈ g₁₄
η (X₀) = 2+X₀
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₁₆ ∈ g₁₄
η (X₁) = 1+X₁
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₁₇ ∈ g₁₄
η (X₀) = X₀-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₁₈ ∈ g₁₄
η (X₁) = X₁-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₂₀ ∈ g₁₉
η (X₀) = 1+X₀
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1 ≤ X₁
h->g
p = 1/4
t₂₁ ∈ g₁₉
η (X₁) = 2+X₁
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1 ≤ X₁
h->g
p = 1/4
t₂₂ ∈ g₁₉
η (X₀) = X₀-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1 ≤ X₁
h->g
p = 1/4
t₂₃ ∈ g₁₉
η (X₁) = X₁-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1 ≤ X₁
h->g
p = 1/4
t₂₅ ∈ g₂₄
η (X₀) = 1+X₀
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₂₆ ∈ g₂₄
η (X₁) = 1+X₁
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₂₇ ∈ g₂₄
η (X₀) = X₀-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₂₈ ∈ g₂₄
η (X₁) = X₁-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₃₀ ∈ g₂₉
η (X₀) = 1+X₀
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₃₁ ∈ g₂₉
η (X₁) = 1+X₁
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₃₂ ∈ g₂₉
η (X₀) = X₀-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₃₃ ∈ g₂₉
η (X₁) = X₁-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₃₅ ∈ g₃₄
η (X₀) = 1+X₀
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₃₆ ∈ g₃₄
η (X₁) = 2+X₁
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₃₇ ∈ g₃₄
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₃₈ ∈ g₃₄
η (X₁) = X₁-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₄₀ ∈ g₃₉
η (X₀) = 1+X₀
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₄₁ ∈ g₃₉
η (X₁) = 1+X₁
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₄₂ ∈ g₃₉
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₄₃ ∈ g₃₉
η (X₁) = X₁-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₄₅ ∈ g₄₄
η (X₀) = 1+X₀
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₄₆ ∈ g₄₄
η (X₁) = 1+X₁
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₄₇ ∈ g₄₄
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₄₈ ∈ g₄₄
η (X₁) = X₁-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
Use expected size bounds for entry point (g₀:f→[t₁:1:g],g)
Use expected size bounds for entry point (g₀:f→[t₁:1:g],g)
Use classical time bound for entry point (g₀:f→[t₁:1:g],g)
Plrf for transition g₁₉:h(X₀,X₁,X₂,X₃,X₄) → [1/4]:t₂₀:g(1+X₀,X₁,X₂-1,X₃,X₄) :+: [1/4]:t₂₁:g(X₀,2+X₁,2+X₂,X₃,X₄) :+: [1/4]:t₂₂:g(X₀-2,X₁,2+X₂,X₃,X₄) :+: [1/4]:t₂₃:g(X₀,X₁-1,X₂-1,X₃,X₄) :|: 1+X₀ ≤ 0 ∧ 1 ≤ X₁ ∧ 1+X₂ ≤ X₃:
new bound:
2⋅X₂+2⋅X₃+2 {O(n)}
PLRF:
• g: 2+2⋅X₃-2⋅X₂
• h: 2+2⋅X₃-2⋅X₂
Show Graph
G
f
f
g
g
f->g
p = 1
t₁ ∈ g₀
{0}
h
h
g->h
p = 1
t₃ ∈ g₂
τ = 1+X₂ ≤ X₃
{0}
h->g
p = 1/4
t₅ ∈ g₄
η (X₀) = 2+X₀
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1 ≤ X₁
h->g
p = 1/4
t₆ ∈ g₄
η (X₁) = 2+X₁
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1 ≤ X₁
h->g
p = 1/4
t₇ ∈ g₄
η (X₀) = X₀-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1 ≤ X₁
h->g
p = 1/4
t₈ ∈ g₄
η (X₁) = X₁-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1 ≤ X₁
h->g
p = 1/4
t₁₀ ∈ g₉
η (X₀) = 2+X₀
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₁₁ ∈ g₉
η (X₁) = 1+X₁
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₁₂ ∈ g₉
η (X₀) = X₀-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₁₃ ∈ g₉
η (X₁) = X₁-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₁₅ ∈ g₁₄
η (X₀) = 2+X₀
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₁₆ ∈ g₁₄
η (X₁) = 1+X₁
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₁₇ ∈ g₁₄
η (X₀) = X₀-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₁₈ ∈ g₁₄
η (X₁) = X₁-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₂₀ ∈ g₁₉
η (X₀) = 1+X₀
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1 ≤ X₁
h->g
p = 1/4
t₂₁ ∈ g₁₉
η (X₁) = 2+X₁
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1 ≤ X₁
h->g
p = 1/4
t₂₂ ∈ g₁₉
η (X₀) = X₀-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1 ≤ X₁
h->g
p = 1/4
t₂₃ ∈ g₁₉
η (X₁) = X₁-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1 ≤ X₁
h->g
p = 1/4
t₂₅ ∈ g₂₄
η (X₀) = 1+X₀
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₂₆ ∈ g₂₄
η (X₁) = 1+X₁
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₂₇ ∈ g₂₄
η (X₀) = X₀-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₂₈ ∈ g₂₄
η (X₁) = X₁-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₃₀ ∈ g₂₉
η (X₀) = 1+X₀
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₃₁ ∈ g₂₉
η (X₁) = 1+X₁
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₃₂ ∈ g₂₉
η (X₀) = X₀-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₃₃ ∈ g₂₉
η (X₁) = X₁-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₃₅ ∈ g₃₄
η (X₀) = 1+X₀
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₃₆ ∈ g₃₄
η (X₁) = 2+X₁
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₃₇ ∈ g₃₄
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₃₈ ∈ g₃₄
η (X₁) = X₁-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₄₀ ∈ g₃₉
η (X₀) = 1+X₀
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₄₁ ∈ g₃₉
η (X₁) = 1+X₁
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₄₂ ∈ g₃₉
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₄₃ ∈ g₃₉
η (X₁) = X₁-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₄₅ ∈ g₄₄
η (X₀) = 1+X₀
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₄₆ ∈ g₄₄
η (X₁) = 1+X₁
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₄₇ ∈ g₄₄
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₄₈ ∈ g₄₄
η (X₁) = X₁-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
Use expected size bounds for entry point (g₀:f→[t₁:1:g],g)
Use expected size bounds for entry point (g₀:f→[t₁:1:g],g)
Use classical time bound for entry point (g₀:f→[t₁:1:g],g)
Plrf for transition g₂₄:h(X₀,X₁,X₂,X₃,X₄) → [1/4]:t₂₅:g(1+X₀,X₁,X₂-1,X₃,X₄) :+: [1/4]:t₂₆:g(X₀,1+X₁,X₂-1,X₃,X₄) :+: [1/4]:t₂₇:g(X₀-2,X₁,2+X₂,X₃,X₄) :+: [1/4]:t₂₈:g(X₀,X₁-2,2+X₂,X₃,X₄) :|: 1+X₀ ≤ 0 ∧ 1+X₁ ≤ 0 ∧ 1+X₂ ≤ X₃:
new bound:
2⋅X₂+2⋅X₃+2 {O(n)}
PLRF:
• g: 2+2⋅X₃-2⋅X₂
• h: 2+2⋅X₃-2⋅X₂
Show Graph
G
f
f
g
g
f->g
p = 1
t₁ ∈ g₀
{0}
h
h
g->h
p = 1
t₃ ∈ g₂
τ = 1+X₂ ≤ X₃
{0}
h->g
p = 1/4
t₅ ∈ g₄
η (X₀) = 2+X₀
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1 ≤ X₁
h->g
p = 1/4
t₆ ∈ g₄
η (X₁) = 2+X₁
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1 ≤ X₁
h->g
p = 1/4
t₇ ∈ g₄
η (X₀) = X₀-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1 ≤ X₁
h->g
p = 1/4
t₈ ∈ g₄
η (X₁) = X₁-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1 ≤ X₁
h->g
p = 1/4
t₁₀ ∈ g₉
η (X₀) = 2+X₀
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₁₁ ∈ g₉
η (X₁) = 1+X₁
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₁₂ ∈ g₉
η (X₀) = X₀-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₁₃ ∈ g₉
η (X₁) = X₁-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₁₅ ∈ g₁₄
η (X₀) = 2+X₀
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₁₆ ∈ g₁₄
η (X₁) = 1+X₁
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₁₇ ∈ g₁₄
η (X₀) = X₀-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₁₈ ∈ g₁₄
η (X₁) = X₁-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₂₀ ∈ g₁₉
η (X₀) = 1+X₀
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1 ≤ X₁
h->g
p = 1/4
t₂₁ ∈ g₁₉
η (X₁) = 2+X₁
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1 ≤ X₁
h->g
p = 1/4
t₂₂ ∈ g₁₉
η (X₀) = X₀-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1 ≤ X₁
h->g
p = 1/4
t₂₃ ∈ g₁₉
η (X₁) = X₁-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1 ≤ X₁
h->g
p = 1/4
t₂₅ ∈ g₂₄
η (X₀) = 1+X₀
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₂₆ ∈ g₂₄
η (X₁) = 1+X₁
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₂₇ ∈ g₂₄
η (X₀) = X₀-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₂₈ ∈ g₂₄
η (X₁) = X₁-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₃₀ ∈ g₂₉
η (X₀) = 1+X₀
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₃₁ ∈ g₂₉
η (X₁) = 1+X₁
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₃₂ ∈ g₂₉
η (X₀) = X₀-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₃₃ ∈ g₂₉
η (X₁) = X₁-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₃₅ ∈ g₃₄
η (X₀) = 1+X₀
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₃₆ ∈ g₃₄
η (X₁) = 2+X₁
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₃₇ ∈ g₃₄
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₃₈ ∈ g₃₄
η (X₁) = X₁-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₄₀ ∈ g₃₉
η (X₀) = 1+X₀
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₄₁ ∈ g₃₉
η (X₁) = 1+X₁
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₄₂ ∈ g₃₉
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₄₃ ∈ g₃₉
η (X₁) = X₁-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₄₅ ∈ g₄₄
η (X₀) = 1+X₀
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₄₆ ∈ g₄₄
η (X₁) = 1+X₁
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₄₇ ∈ g₄₄
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₄₈ ∈ g₄₄
η (X₁) = X₁-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
Use expected size bounds for entry point (g₀:f→[t₁:1:g],g)
Use expected size bounds for entry point (g₀:f→[t₁:1:g],g)
Use classical time bound for entry point (g₀:f→[t₁:1:g],g)
Plrf for transition g₂₉:h(X₀,X₁,X₂,X₃,X₄) → [1/4]:t₃₀:g(1+X₀,X₁,X₂-1,X₃,X₄) :+: [1/4]:t₃₁:g(X₀,1+X₁,1+X₂,X₃,X₄) :+: [1/4]:t₃₂:g(X₀-2,X₁,2+X₂,X₃,X₄) :+: [1/4]:t₃₃:g(X₀,X₁-1,1+X₂,X₃,X₄) :|: 1+X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0 ∧ 1+X₂ ≤ X₃:
new bound:
4/3⋅X₂+4/3⋅X₃+4/3 {O(n)}
PLRF:
• g: 4/3+4/3⋅X₃-4/3⋅X₂
• h: 4/3+4/3⋅X₃-4/3⋅X₂
Show Graph
G
f
f
g
g
f->g
p = 1
t₁ ∈ g₀
{0}
h
h
g->h
p = 1
t₃ ∈ g₂
τ = 1+X₂ ≤ X₃
{0}
h->g
p = 1/4
t₅ ∈ g₄
η (X₀) = 2+X₀
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1 ≤ X₁
h->g
p = 1/4
t₆ ∈ g₄
η (X₁) = 2+X₁
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1 ≤ X₁
h->g
p = 1/4
t₇ ∈ g₄
η (X₀) = X₀-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1 ≤ X₁
h->g
p = 1/4
t₈ ∈ g₄
η (X₁) = X₁-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1 ≤ X₁
h->g
p = 1/4
t₁₀ ∈ g₉
η (X₀) = 2+X₀
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₁₁ ∈ g₉
η (X₁) = 1+X₁
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₁₂ ∈ g₉
η (X₀) = X₀-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₁₃ ∈ g₉
η (X₁) = X₁-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₁₅ ∈ g₁₄
η (X₀) = 2+X₀
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₁₆ ∈ g₁₄
η (X₁) = 1+X₁
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₁₇ ∈ g₁₄
η (X₀) = X₀-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₁₈ ∈ g₁₄
η (X₁) = X₁-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₂₀ ∈ g₁₉
η (X₀) = 1+X₀
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1 ≤ X₁
h->g
p = 1/4
t₂₁ ∈ g₁₉
η (X₁) = 2+X₁
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1 ≤ X₁
h->g
p = 1/4
t₂₂ ∈ g₁₉
η (X₀) = X₀-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1 ≤ X₁
h->g
p = 1/4
t₂₃ ∈ g₁₉
η (X₁) = X₁-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1 ≤ X₁
h->g
p = 1/4
t₂₅ ∈ g₂₄
η (X₀) = 1+X₀
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₂₆ ∈ g₂₄
η (X₁) = 1+X₁
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₂₇ ∈ g₂₄
η (X₀) = X₀-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₂₈ ∈ g₂₄
η (X₁) = X₁-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₃₀ ∈ g₂₉
η (X₀) = 1+X₀
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₃₁ ∈ g₂₉
η (X₁) = 1+X₁
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₃₂ ∈ g₂₉
η (X₀) = X₀-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₃₃ ∈ g₂₉
η (X₁) = X₁-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₃₅ ∈ g₃₄
η (X₀) = 1+X₀
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₃₆ ∈ g₃₄
η (X₁) = 2+X₁
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₃₇ ∈ g₃₄
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₃₈ ∈ g₃₄
η (X₁) = X₁-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₄₀ ∈ g₃₉
η (X₀) = 1+X₀
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₄₁ ∈ g₃₉
η (X₁) = 1+X₁
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₄₂ ∈ g₃₉
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₄₃ ∈ g₃₉
η (X₁) = X₁-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₄₅ ∈ g₄₄
η (X₀) = 1+X₀
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₄₆ ∈ g₄₄
η (X₁) = 1+X₁
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₄₇ ∈ g₄₄
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₄₈ ∈ g₄₄
η (X₁) = X₁-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
Use expected size bounds for entry point (g₀:f→[t₁:1:g],g)
Use expected size bounds for entry point (g₀:f→[t₁:1:g],g)
Use classical time bound for entry point (g₀:f→[t₁:1:g],g)
Plrf for transition g₃₄:h(X₀,X₁,X₂,X₃,X₄) → [1/4]:t₃₅:g(1+X₀,X₁,1+X₂,X₃,X₄) :+: [1/4]:t₃₆:g(X₀,2+X₁,2+X₂,X₃,X₄) :+: [1/4]:t₃₇:g(X₀-1,X₁,1+X₂,X₃,X₄) :+: [1/4]:t₃₈:g(X₀,X₁-1,X₂-1,X₃,X₄) :|: 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 1+X₂ ≤ X₃:
new bound:
4/3⋅X₂+4/3⋅X₃+4/3 {O(n)}
PLRF:
• g: 4/3+4/3⋅X₃-4/3⋅X₂
• h: 4/3+4/3⋅X₃-4/3⋅X₂
Show Graph
G
f
f
g
g
f->g
p = 1
t₁ ∈ g₀
{0}
h
h
g->h
p = 1
t₃ ∈ g₂
τ = 1+X₂ ≤ X₃
{0}
h->g
p = 1/4
t₅ ∈ g₄
η (X₀) = 2+X₀
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1 ≤ X₁
h->g
p = 1/4
t₆ ∈ g₄
η (X₁) = 2+X₁
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1 ≤ X₁
h->g
p = 1/4
t₇ ∈ g₄
η (X₀) = X₀-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1 ≤ X₁
h->g
p = 1/4
t₈ ∈ g₄
η (X₁) = X₁-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1 ≤ X₁
h->g
p = 1/4
t₁₀ ∈ g₉
η (X₀) = 2+X₀
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₁₁ ∈ g₉
η (X₁) = 1+X₁
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₁₂ ∈ g₉
η (X₀) = X₀-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₁₃ ∈ g₉
η (X₁) = X₁-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₁₅ ∈ g₁₄
η (X₀) = 2+X₀
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₁₆ ∈ g₁₄
η (X₁) = 1+X₁
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₁₇ ∈ g₁₄
η (X₀) = X₀-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₁₈ ∈ g₁₄
η (X₁) = X₁-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₂₀ ∈ g₁₉
η (X₀) = 1+X₀
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1 ≤ X₁
h->g
p = 1/4
t₂₁ ∈ g₁₉
η (X₁) = 2+X₁
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1 ≤ X₁
h->g
p = 1/4
t₂₂ ∈ g₁₉
η (X₀) = X₀-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1 ≤ X₁
h->g
p = 1/4
t₂₃ ∈ g₁₉
η (X₁) = X₁-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1 ≤ X₁
h->g
p = 1/4
t₂₅ ∈ g₂₄
η (X₀) = 1+X₀
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₂₆ ∈ g₂₄
η (X₁) = 1+X₁
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₂₇ ∈ g₂₄
η (X₀) = X₀-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₂₈ ∈ g₂₄
η (X₁) = X₁-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₃₀ ∈ g₂₉
η (X₀) = 1+X₀
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₃₁ ∈ g₂₉
η (X₁) = 1+X₁
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₃₂ ∈ g₂₉
η (X₀) = X₀-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₃₃ ∈ g₂₉
η (X₁) = X₁-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₃₅ ∈ g₃₄
η (X₀) = 1+X₀
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₃₆ ∈ g₃₄
η (X₁) = 2+X₁
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₃₇ ∈ g₃₄
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₃₈ ∈ g₃₄
η (X₁) = X₁-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₄₀ ∈ g₃₉
η (X₀) = 1+X₀
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₄₁ ∈ g₃₉
η (X₁) = 1+X₁
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₄₂ ∈ g₃₉
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₄₃ ∈ g₃₉
η (X₁) = X₁-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₄₅ ∈ g₄₄
η (X₀) = 1+X₀
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₄₆ ∈ g₄₄
η (X₁) = 1+X₁
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₄₇ ∈ g₄₄
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₄₈ ∈ g₄₄
η (X₁) = X₁-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
Use expected size bounds for entry point (g₀:f→[t₁:1:g],g)
Use expected size bounds for entry point (g₀:f→[t₁:1:g],g)
Use classical time bound for entry point (g₀:f→[t₁:1:g],g)
Plrf for transition g₃₉:h(X₀,X₁,X₂,X₃,X₄) → [1/4]:t₄₀:g(1+X₀,X₁,1+X₂,X₃,X₄) :+: [1/4]:t₄₁:g(X₀,1+X₁,X₂-1,X₃,X₄) :+: [1/4]:t₄₂:g(X₀-1,X₁,1+X₂,X₃,X₄) :+: [1/4]:t₄₃:g(X₀,X₁-2,2+X₂,X₃,X₄) :|: 1+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 1+X₂ ≤ X₃:
new bound:
4/3⋅X₂+4/3⋅X₃+4/3 {O(n)}
PLRF:
• g: 4/3+4/3⋅X₃-4/3⋅X₂
• h: 4/3+4/3⋅X₃-4/3⋅X₂
Show Graph
G
f
f
g
g
f->g
p = 1
t₁ ∈ g₀
{0}
h
h
g->h
p = 1
t₃ ∈ g₂
τ = 1+X₂ ≤ X₃
{0}
h->g
p = 1/4
t₅ ∈ g₄
η (X₀) = 2+X₀
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1 ≤ X₁
h->g
p = 1/4
t₆ ∈ g₄
η (X₁) = 2+X₁
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1 ≤ X₁
h->g
p = 1/4
t₇ ∈ g₄
η (X₀) = X₀-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1 ≤ X₁
h->g
p = 1/4
t₈ ∈ g₄
η (X₁) = X₁-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1 ≤ X₁
h->g
p = 1/4
t₁₀ ∈ g₉
η (X₀) = 2+X₀
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₁₁ ∈ g₉
η (X₁) = 1+X₁
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₁₂ ∈ g₉
η (X₀) = X₀-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₁₃ ∈ g₉
η (X₁) = X₁-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₁₅ ∈ g₁₄
η (X₀) = 2+X₀
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₁₆ ∈ g₁₄
η (X₁) = 1+X₁
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₁₇ ∈ g₁₄
η (X₀) = X₀-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₁₈ ∈ g₁₄
η (X₁) = X₁-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₂₀ ∈ g₁₉
η (X₀) = 1+X₀
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1 ≤ X₁
h->g
p = 1/4
t₂₁ ∈ g₁₉
η (X₁) = 2+X₁
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1 ≤ X₁
h->g
p = 1/4
t₂₂ ∈ g₁₉
η (X₀) = X₀-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1 ≤ X₁
h->g
p = 1/4
t₂₃ ∈ g₁₉
η (X₁) = X₁-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1 ≤ X₁
h->g
p = 1/4
t₂₅ ∈ g₂₄
η (X₀) = 1+X₀
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₂₆ ∈ g₂₄
η (X₁) = 1+X₁
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₂₇ ∈ g₂₄
η (X₀) = X₀-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₂₈ ∈ g₂₄
η (X₁) = X₁-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₃₀ ∈ g₂₉
η (X₀) = 1+X₀
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₃₁ ∈ g₂₉
η (X₁) = 1+X₁
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₃₂ ∈ g₂₉
η (X₀) = X₀-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₃₃ ∈ g₂₉
η (X₁) = X₁-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₃₅ ∈ g₃₄
η (X₀) = 1+X₀
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₃₆ ∈ g₃₄
η (X₁) = 2+X₁
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₃₇ ∈ g₃₄
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₃₈ ∈ g₃₄
η (X₁) = X₁-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₄₀ ∈ g₃₉
η (X₀) = 1+X₀
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₄₁ ∈ g₃₉
η (X₁) = 1+X₁
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₄₂ ∈ g₃₉
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₄₃ ∈ g₃₉
η (X₁) = X₁-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₄₅ ∈ g₄₄
η (X₀) = 1+X₀
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₄₆ ∈ g₄₄
η (X₁) = 1+X₁
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₄₇ ∈ g₄₄
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₄₈ ∈ g₄₄
η (X₁) = X₁-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
Use expected size bounds for entry point (g₀:f→[t₁:1:g],g)
Use expected size bounds for entry point (g₀:f→[t₁:1:g],g)
Use classical time bound for entry point (g₀:f→[t₁:1:g],g)
Plrf for transition g₄₄:h(X₀,X₁,X₂,X₃,X₄) → [1/4]:t₄₅:g(1+X₀,X₁,1+X₂,X₃,X₄) :+: [1/4]:t₄₆:g(X₀,1+X₁,1+X₂,X₃,X₄) :+: [1/4]:t₄₇:g(X₀-1,X₁,1+X₂,X₃,X₄) :+: [1/4]:t₄₈:g(X₀,X₁-1,1+X₂,X₃,X₄) :|: 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0 ∧ 1+X₂ ≤ X₃:
new bound:
X₂+X₃+1 {O(n)}
PLRF:
• g: 1+X₃-X₂
• h: 1+X₃-X₂
Show Graph
G
f
f
g
g
f->g
p = 1
t₁ ∈ g₀
{0}
h
h
g->h
p = 1
t₃ ∈ g₂
τ = 1+X₂ ≤ X₃
{0}
h->g
p = 1/4
t₅ ∈ g₄
η (X₀) = 2+X₀
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1 ≤ X₁
h->g
p = 1/4
t₆ ∈ g₄
η (X₁) = 2+X₁
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1 ≤ X₁
h->g
p = 1/4
t₇ ∈ g₄
η (X₀) = X₀-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1 ≤ X₁
h->g
p = 1/4
t₈ ∈ g₄
η (X₁) = X₁-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1 ≤ X₁
h->g
p = 1/4
t₁₀ ∈ g₉
η (X₀) = 2+X₀
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₁₁ ∈ g₉
η (X₁) = 1+X₁
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₁₂ ∈ g₉
η (X₀) = X₀-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₁₃ ∈ g₉
η (X₁) = X₁-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₁₅ ∈ g₁₄
η (X₀) = 2+X₀
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₁₆ ∈ g₁₄
η (X₁) = 1+X₁
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₁₇ ∈ g₁₄
η (X₀) = X₀-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₁₈ ∈ g₁₄
η (X₁) = X₁-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₀ ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₂₀ ∈ g₁₉
η (X₀) = 1+X₀
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1 ≤ X₁
h->g
p = 1/4
t₂₁ ∈ g₁₉
η (X₁) = 2+X₁
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1 ≤ X₁
h->g
p = 1/4
t₂₂ ∈ g₁₉
η (X₀) = X₀-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1 ≤ X₁
h->g
p = 1/4
t₂₃ ∈ g₁₉
η (X₁) = X₁-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1 ≤ X₁
h->g
p = 1/4
t₂₅ ∈ g₂₄
η (X₀) = 1+X₀
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₂₆ ∈ g₂₄
η (X₁) = 1+X₁
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₂₇ ∈ g₂₄
η (X₀) = X₀-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₂₈ ∈ g₂₄
η (X₁) = X₁-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 1+X₁ ≤ 0
h->g
p = 1/4
t₃₀ ∈ g₂₉
η (X₀) = 1+X₀
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₃₁ ∈ g₂₉
η (X₁) = 1+X₁
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₃₂ ∈ g₂₉
η (X₀) = X₀-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₃₃ ∈ g₂₉
η (X₁) = X₁-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₃₅ ∈ g₃₄
η (X₀) = 1+X₀
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₃₆ ∈ g₃₄
η (X₁) = 2+X₁
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₃₇ ∈ g₃₄
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₃₈ ∈ g₃₄
η (X₁) = X₁-1
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₄₀ ∈ g₃₉
η (X₀) = 1+X₀
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₄₁ ∈ g₃₉
η (X₁) = 1+X₁
η (X₂) = X₂-1
τ = 1+X₂ ≤ X₃ ∧ 1+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₄₂ ∈ g₃₉
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₄₃ ∈ g₃₉
η (X₁) = X₁-2
η (X₂) = 2+X₂
τ = 1+X₂ ≤ X₃ ∧ 1+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
h->g
p = 1/4
t₄₅ ∈ g₄₄
η (X₀) = 1+X₀
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₄₆ ∈ g₄₄
η (X₁) = 1+X₁
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₄₇ ∈ g₄₄
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
h->g
p = 1/4
t₄₈ ∈ g₄₄
η (X₁) = X₁-1
η (X₂) = 1+X₂
τ = 1+X₂ ≤ X₃ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
Use expected size bounds for entry point (g₀:f→[t₁:1:g],g)
Use expected size bounds for entry point (g₀:f→[t₁:1:g],g)
Use classical time bound for entry point (g₀:f→[t₁:1:g],g)
Results of Probabilistic Analysis
All Bounds
Timebounds
Overall timebound:49/3⋅X₂+49/3⋅X₃+52/3 {O(n)}
g₀: 1 {O(1)}
g₂: 2⋅X₂+2⋅X₃+2 {O(n)}
g₄: 2⋅X₂+2⋅X₃+2 {O(n)}
g₉: 2⋅X₂+2⋅X₃+2 {O(n)}
g₁₄: 4/3⋅X₂+4/3⋅X₃+4/3 {O(n)}
g₁₉: 2⋅X₂+2⋅X₃+2 {O(n)}
g₂₄: 2⋅X₂+2⋅X₃+2 {O(n)}
g₂₉: 4/3⋅X₂+4/3⋅X₃+4/3 {O(n)}
g₃₄: 4/3⋅X₂+4/3⋅X₃+4/3 {O(n)}
g₃₉: 4/3⋅X₂+4/3⋅X₃+4/3 {O(n)}
g₄₄: X₂+X₃+1 {O(n)}
Costbounds
Overall costbound: 172/3⋅X₂+172/3⋅X₃+172/3 {O(n)}
g₀: 0 {O(1)}
g₂: 0 {O(1)}
g₄: 8⋅X₂+8⋅X₃+8 {O(n)}
g₉: 8⋅X₂+8⋅X₃+8 {O(n)}
g₁₄: 16/3⋅X₂+16/3⋅X₃+16/3 {O(n)}
g₁₉: 8⋅X₂+8⋅X₃+8 {O(n)}
g₂₄: 8⋅X₂+8⋅X₃+8 {O(n)}
g₂₉: 16/3⋅X₂+16/3⋅X₃+16/3 {O(n)}
g₃₄: 16/3⋅X₂+16/3⋅X₃+16/3 {O(n)}
g₃₉: 16/3⋅X₂+16/3⋅X₃+16/3 {O(n)}
g₄₄: 4⋅X₂+4⋅X₃+4 {O(n)}
Sizebounds
(g₀,g), X₀: X₀ {O(n)}
(g₀,g), X₁: X₁ {O(n)}
(g₀,g), X₂: X₂ {O(n)}
(g₀,g), X₃: X₃ {O(n)}
(g₀,g), X₄: X₄ {O(n)}
(g₂,h), X₀: 43/6⋅X₂+43/6⋅X₃+X₀+43/6 {O(n)}
(g₂,h), X₁: 43/6⋅X₂+43/6⋅X₃+X₁+43/6 {O(n)}
(g₂,h), X₂: 59/3⋅X₃+62/3⋅X₂+59/3 {O(n)}
(g₂,h), X₃: X₃ {O(n)}
(g₂,h), X₄: X₄ {O(n)}
(g₄,g), X₀: 43/6⋅X₂+43/6⋅X₃+X₀+43/6 {O(n)}
(g₄,g), X₁: 43/6⋅X₂+43/6⋅X₃+X₁+43/6 {O(n)}
(g₄,g), X₂: 59/3⋅X₃+62/3⋅X₂+59/3 {O(n)}
(g₄,g), X₃: X₃ {O(n)}
(g₄,g), X₄: X₄ {O(n)}
(g₉,g), X₀: 43/6⋅X₂+43/6⋅X₃+X₀+43/6 {O(n)}
(g₉,g), X₁: 43/6⋅X₂+43/6⋅X₃+X₁+43/6 {O(n)}
(g₉,g), X₂: 59/3⋅X₃+62/3⋅X₂+59/3 {O(n)}
(g₉,g), X₃: X₃ {O(n)}
(g₉,g), X₄: X₄ {O(n)}
(g₁₄,g), X₀: 43/6⋅X₂+43/6⋅X₃+X₀+43/6 {O(n)}
(g₁₄,g), X₁: 2 {O(1)}
(g₁₄,g), X₂: 59/3⋅X₃+62/3⋅X₂+59/3 {O(n)}
(g₁₄,g), X₃: X₃ {O(n)}
(g₁₄,g), X₄: X₄ {O(n)}
(g₁₉,g), X₀: 43/6⋅X₂+43/6⋅X₃+X₀+43/6 {O(n)}
(g₁₉,g), X₁: 43/6⋅X₂+43/6⋅X₃+X₁+43/6 {O(n)}
(g₁₉,g), X₂: 59/3⋅X₃+62/3⋅X₂+59/3 {O(n)}
(g₁₉,g), X₃: X₃ {O(n)}
(g₁₉,g), X₄: X₄ {O(n)}
(g₂₄,g), X₀: 43/6⋅X₂+43/6⋅X₃+X₀+43/6 {O(n)}
(g₂₄,g), X₁: 43/6⋅X₂+43/6⋅X₃+X₁+43/6 {O(n)}
(g₂₄,g), X₂: 59/3⋅X₃+62/3⋅X₂+59/3 {O(n)}
(g₂₄,g), X₃: X₃ {O(n)}
(g₂₄,g), X₄: X₄ {O(n)}
(g₂₉,g), X₀: 43/6⋅X₂+43/6⋅X₃+X₀+43/6 {O(n)}
(g₂₉,g), X₁: 2 {O(1)}
(g₂₉,g), X₂: 59/3⋅X₃+62/3⋅X₂+59/3 {O(n)}
(g₂₉,g), X₃: X₃ {O(n)}
(g₂₉,g), X₄: X₄ {O(n)}
(g₃₄,g), X₀: 2 {O(1)}
(g₃₄,g), X₁: 43/6⋅X₂+43/6⋅X₃+X₁+43/6 {O(n)}
(g₃₄,g), X₂: 59/3⋅X₃+62/3⋅X₂+59/3 {O(n)}
(g₃₄,g), X₃: X₃ {O(n)}
(g₃₄,g), X₄: X₄ {O(n)}
(g₃₉,g), X₀: 2 {O(1)}
(g₃₉,g), X₁: 43/6⋅X₂+43/6⋅X₃+X₁+43/6 {O(n)}
(g₃₉,g), X₂: 59/3⋅X₃+62/3⋅X₂+59/3 {O(n)}
(g₃₉,g), X₃: X₃ {O(n)}
(g₃₉,g), X₄: X₄ {O(n)}
(g₄₄,g), X₀: 2 {O(1)}
(g₄₄,g), X₁: 2 {O(1)}
(g₄₄,g), X₂: 59/3⋅X₃+62/3⋅X₂+59/3 {O(n)}
(g₄₄,g), X₃: X₃ {O(n)}
(g₄₄,g), X₄: X₄ {O(n)}