Preprocessing
Eliminate variables [I; X₀; X₅; X₇] that do not contribute to the problem
Found invariant X₄ ≤ X₁ ∧ 0 ≤ X₄ ∧ 0 ≤ X₁+X₄ ∧ X₃ ≤ X₂ ∧ X₃ ≤ X₁ ∧ X₂ ≤ X₃ ∧ X₂ ≤ X₁ ∧ 0 ≤ X₁ for location f18
Found invariant 0 ≤ X₁ for location f10
Found invariant X₆ ≤ X₃ ∧ X₆ ≤ X₂ ∧ X₆ ≤ X₁ ∧ 1 ≤ X₆ ∧ 1 ≤ X₄+X₆ ∧ 1+X₄ ≤ X₆ ∧ 3 ≤ X₃+X₆ ∧ 3 ≤ X₂+X₆ ∧ 3 ≤ X₁+X₆ ∧ 2+X₄ ≤ X₃ ∧ 2+X₄ ≤ X₂ ∧ 2+X₄ ≤ X₁ ∧ 0 ≤ X₄ ∧ 2 ≤ X₃+X₄ ∧ 2 ≤ X₂+X₄ ∧ 2 ≤ X₁+X₄ ∧ X₃ ≤ X₂ ∧ X₃ ≤ X₁ ∧ 2 ≤ X₃ ∧ 4 ≤ X₂+X₃ ∧ X₂ ≤ X₃ ∧ 4 ≤ X₁+X₃ ∧ X₂ ≤ X₁ ∧ 2 ≤ X₂ ∧ 4 ≤ X₁+X₂ ∧ 2 ≤ X₁ for location f22
Found invariant X₄ ≤ 0 ∧ X₄ ≤ X₁ ∧ 0 ≤ X₄ ∧ 0 ≤ X₁+X₄ ∧ X₃ ≤ X₂ ∧ X₃ ≤ X₁ ∧ X₂ ≤ X₃ ∧ X₂ ≤ X₁ ∧ 0 ≤ X₁ for location f34
Probabilistic Analysis
Probabilistic Program after Preprocessing
Start: f0
Program_Vars: X₀, X₁, X₂, X₃, X₄, X₅, X₆, X₇
Temp_Vars: I
Locations: f0, f10, f18, f22, f34
Transitions:
g₀:f0(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇) → t₁:f10(I,0,X₂,X₃,X₄,X₅,X₆,X₇) :|:
g₂:f10(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇) → t₃:f10(X₀,1+X₁,X₂,X₃,X₄,X₅,X₆,X₇) :|: 1+X₁ ≤ X₂ ∧ 0 ≤ X₁
g₄:f18(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇) → t₅:f22(X₀,X₁,X₂,X₃,X₄,X₄,1+X₄,X₇) :|: 2+X₄ ≤ X₃ ∧ 0 ≤ X₁ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ 0 ≤ X₁+X₄ ∧ X₄ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₂ ≤ X₃ ∧ 0 ≤ X₄
g₆:f22(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇) → [1/2]:t₇:f22(X₀,X₁,X₂,X₃,X₄,X₅,1+X₆,X₇) :+: [1/2]:t₈:f22(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇) :|: 1+X₆ ≤ X₃ ∧ 1 ≤ X₄+X₆ ∧ 1+X₄ ≤ X₆ ∧ 1 ≤ X₆ ∧ 2 ≤ X₁ ∧ 2 ≤ X₁+X₄ ∧ 2+X₄ ≤ X₁ ∧ 2 ≤ X₂ ∧ 2 ≤ X₂+X₄ ∧ 2+X₄ ≤ X₂ ∧ 2 ≤ X₃ ∧ 2 ≤ X₃+X₄ ∧ 2+X₄ ≤ X₃ ∧ 3 ≤ X₁+X₆ ∧ 3 ≤ X₂+X₆ ∧ 3 ≤ X₃+X₆ ∧ 4 ≤ X₁+X₂ ∧ 4 ≤ X₁+X₃ ∧ 4 ≤ X₂+X₃ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ X₆ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₆ ≤ X₂ ∧ X₂ ≤ X₃ ∧ X₆ ≤ X₃ ∧ 0 ≤ X₄
g₉:f22(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇) → [1/2]:t₁₀:f22(X₀,X₁,X₂,X₃,X₄,X₆,1+X₆,X₇) :+: [1/2]:t₁₁:f22(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇) :|: 1+X₆ ≤ X₃ ∧ 1 ≤ X₄+X₆ ∧ 1+X₄ ≤ X₆ ∧ 1 ≤ X₆ ∧ 2 ≤ X₁ ∧ 2 ≤ X₁+X₄ ∧ 2+X₄ ≤ X₁ ∧ 2 ≤ X₂ ∧ 2 ≤ X₂+X₄ ∧ 2+X₄ ≤ X₂ ∧ 2 ≤ X₃ ∧ 2 ≤ X₃+X₄ ∧ 2+X₄ ≤ X₃ ∧ 3 ≤ X₁+X₆ ∧ 3 ≤ X₂+X₆ ∧ 3 ≤ X₃+X₆ ∧ 4 ≤ X₁+X₂ ∧ 4 ≤ X₁+X₃ ∧ 4 ≤ X₂+X₃ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ X₆ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₆ ≤ X₂ ∧ X₂ ≤ X₃ ∧ X₆ ≤ X₃ ∧ 0 ≤ X₄
g₁₂:f22(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇) → t₁₃:f18(X₀,X₁,X₂,X₃,1+X₄,X₅,X₆,I) :|: X₃ ≤ X₆ ∧ 1 ≤ X₄+X₆ ∧ 1+X₄ ≤ X₆ ∧ 1 ≤ X₆ ∧ 2 ≤ X₁ ∧ 2 ≤ X₁+X₄ ∧ 2+X₄ ≤ X₁ ∧ 2 ≤ X₂ ∧ 2 ≤ X₂+X₄ ∧ 2+X₄ ≤ X₂ ∧ 2 ≤ X₃ ∧ 2 ≤ X₃+X₄ ∧ 2+X₄ ≤ X₃ ∧ 3 ≤ X₁+X₆ ∧ 3 ≤ X₂+X₆ ∧ 3 ≤ X₃+X₆ ∧ 4 ≤ X₁+X₂ ∧ 4 ≤ X₁+X₃ ∧ 4 ≤ X₂+X₃ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ X₆ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₆ ≤ X₂ ∧ X₂ ≤ X₃ ∧ X₆ ≤ X₃ ∧ 0 ≤ X₄
g₁₄:f18(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇) → t₁₅:f34(X₀,X₁,X₂,X₃,0,X₅,X₆,X₇) :|: X₃ ≤ 1+X₄ ∧ 0 ≤ X₁ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ 0 ≤ X₁+X₄ ∧ X₄ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₂ ≤ X₃ ∧ 0 ≤ X₄
g₁₆:f10(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇) → t₁₇:f18(X₀,X₁,X₂,X₂,0,X₅,X₆,X₇) :|: X₂ ≤ X₁ ∧ 0 ≤ X₁
Show Graph
G
f0
f0
f10
f10
f0->f10
p = 1
t₁ ∈ g₀
η (X₁) = 0
f10->f10
p = 1
t₃ ∈ g₂
η (X₁) = 1+X₁
τ = 0 ≤ X₁ ∧ 1+X₁ ≤ X₂
f18
f18
f10->f18
p = 1
t₁₇ ∈ g₁₆
η (X₃) = X₂
η (X₄) = 0
τ = 0 ≤ X₁ ∧ X₂ ≤ X₁
f22
f22
f18->f22
p = 1
t₅ ∈ g₄
η (X₅) = X₄
η (X₆) = 1+X₄
τ = 0 ≤ X₁ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ 0 ≤ X₁+X₄ ∧ X₄ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₂ ≤ X₃ ∧ 0 ≤ X₄ ∧ 2+X₄ ≤ X₃
f34
f34
f18->f34
p = 1
t₁₅ ∈ g₁₄
η (X₄) = 0
τ = 0 ≤ X₁ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ 0 ≤ X₁+X₄ ∧ X₄ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₂ ≤ X₃ ∧ 0 ≤ X₄ ∧ X₃ ≤ 1+X₄
f22->f18
p = 1
t₁₃ ∈ g₁₂
η (X₄) = 1+X₄
η (X₇) = I
τ = 1 ≤ X₄+X₆ ∧ 1+X₄ ≤ X₆ ∧ 1 ≤ X₆ ∧ 2 ≤ X₁ ∧ 2 ≤ X₁+X₄ ∧ 2+X₄ ≤ X₁ ∧ 2 ≤ X₂ ∧ 2 ≤ X₂+X₄ ∧ 2+X₄ ≤ X₂ ∧ 2 ≤ X₃ ∧ 2 ≤ X₃+X₄ ∧ 2+X₄ ≤ X₃ ∧ 3 ≤ X₁+X₆ ∧ 3 ≤ X₂+X₆ ∧ 3 ≤ X₃+X₆ ∧ 4 ≤ X₁+X₂ ∧ 4 ≤ X₁+X₃ ∧ 4 ≤ X₂+X₃ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ X₆ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₆ ≤ X₂ ∧ X₂ ≤ X₃ ∧ X₆ ≤ X₃ ∧ 0 ≤ X₄ ∧ X₃ ≤ X₆
f22->f22
p = 1/2
t₇ ∈ g₆
η (X₆) = 1+X₆
τ = 1 ≤ X₄+X₆ ∧ 1+X₄ ≤ X₆ ∧ 1 ≤ X₆ ∧ 2 ≤ X₁ ∧ 2 ≤ X₁+X₄ ∧ 2+X₄ ≤ X₁ ∧ 2 ≤ X₂ ∧ 2 ≤ X₂+X₄ ∧ 2+X₄ ≤ X₂ ∧ 2 ≤ X₃ ∧ 2 ≤ X₃+X₄ ∧ 2+X₄ ≤ X₃ ∧ 3 ≤ X₁+X₆ ∧ 3 ≤ X₂+X₆ ∧ 3 ≤ X₃+X₆ ∧ 4 ≤ X₁+X₂ ∧ 4 ≤ X₁+X₃ ∧ 4 ≤ X₂+X₃ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ X₆ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₆ ≤ X₂ ∧ X₂ ≤ X₃ ∧ X₆ ≤ X₃ ∧ 0 ≤ X₄ ∧ 1+X₆ ≤ X₃
f22->f22
p = 1/2
t₈ ∈ g₆
τ = 1 ≤ X₄+X₆ ∧ 1+X₄ ≤ X₆ ∧ 1 ≤ X₆ ∧ 2 ≤ X₁ ∧ 2 ≤ X₁+X₄ ∧ 2+X₄ ≤ X₁ ∧ 2 ≤ X₂ ∧ 2 ≤ X₂+X₄ ∧ 2+X₄ ≤ X₂ ∧ 2 ≤ X₃ ∧ 2 ≤ X₃+X₄ ∧ 2+X₄ ≤ X₃ ∧ 3 ≤ X₁+X₆ ∧ 3 ≤ X₂+X₆ ∧ 3 ≤ X₃+X₆ ∧ 4 ≤ X₁+X₂ ∧ 4 ≤ X₁+X₃ ∧ 4 ≤ X₂+X₃ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ X₆ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₆ ≤ X₂ ∧ X₂ ≤ X₃ ∧ X₆ ≤ X₃ ∧ 0 ≤ X₄ ∧ 1+X₆ ≤ X₃
f22->f22
p = 1/2
t₁₀ ∈ g₉
η (X₅) = X₆
η (X₆) = 1+X₆
τ = 1 ≤ X₄+X₆ ∧ 1+X₄ ≤ X₆ ∧ 1 ≤ X₆ ∧ 2 ≤ X₁ ∧ 2 ≤ X₁+X₄ ∧ 2+X₄ ≤ X₁ ∧ 2 ≤ X₂ ∧ 2 ≤ X₂+X₄ ∧ 2+X₄ ≤ X₂ ∧ 2 ≤ X₃ ∧ 2 ≤ X₃+X₄ ∧ 2+X₄ ≤ X₃ ∧ 3 ≤ X₁+X₆ ∧ 3 ≤ X₂+X₆ ∧ 3 ≤ X₃+X₆ ∧ 4 ≤ X₁+X₂ ∧ 4 ≤ X₁+X₃ ∧ 4 ≤ X₂+X₃ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ X₆ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₆ ≤ X₂ ∧ X₂ ≤ X₃ ∧ X₆ ≤ X₃ ∧ 0 ≤ X₄ ∧ 1+X₆ ≤ X₃
f22->f22
p = 1/2
t₁₁ ∈ g₉
τ = 1 ≤ X₄+X₆ ∧ 1+X₄ ≤ X₆ ∧ 1 ≤ X₆ ∧ 2 ≤ X₁ ∧ 2 ≤ X₁+X₄ ∧ 2+X₄ ≤ X₁ ∧ 2 ≤ X₂ ∧ 2 ≤ X₂+X₄ ∧ 2+X₄ ≤ X₂ ∧ 2 ≤ X₃ ∧ 2 ≤ X₃+X₄ ∧ 2+X₄ ≤ X₃ ∧ 3 ≤ X₁+X₆ ∧ 3 ≤ X₂+X₆ ∧ 3 ≤ X₃+X₆ ∧ 4 ≤ X₁+X₂ ∧ 4 ≤ X₁+X₃ ∧ 4 ≤ X₂+X₃ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ X₆ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₆ ≤ X₂ ∧ X₂ ≤ X₃ ∧ X₆ ≤ X₃ ∧ 0 ≤ X₄ ∧ 1+X₆ ≤ X₃
Run classical analysis on SCC: [f0]
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₁₄: 1 {O(1)}
g₁₆: 1 {O(1)}
Costbounds
Overall costbound: inf {Infinity}
g₀: inf {Infinity}
g₂: inf {Infinity}
g₄: inf {Infinity}
g₆: inf {Infinity}
g₉: inf {Infinity}
g₁₂: inf {Infinity}
g₁₄: inf {Infinity}
g₁₆: inf {Infinity}
Sizebounds
(g₀,f10), X₁: 0 {O(1)}
(g₀,f10), X₂: X₂ {O(n)}
(g₀,f10), X₃: X₃ {O(n)}
(g₀,f10), X₄: X₄ {O(n)}
(g₀,f10), X₅: X₅ {O(n)}
(g₀,f10), X₆: X₆ {O(n)}
(g₀,f10), X₇: X₇ {O(n)}
Run probabilistic analysis on SCC: [f0]
Run classical analysis on SCC: [f10]
MPRF for transition t₃: f10(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇) → f10(X₀,1+X₁,X₂,X₃,X₄,X₅,X₆,X₇) :|: 0 ≤ X₁ ∧ 1+X₁ ≤ X₂ of depth 1:
new bound:
X₂ {O(n)}
MPRF:
• f10: [X₂-X₁]
Show Graph
G
f0
f0
f10
f10
f0->f10
t₁
η (X₀) = I
η (X₁) = 0
f10->f10
t₃
η (X₁) = 1+X₁
τ = 0 ≤ X₁ ∧ 1+X₁ ≤ X₂
f18
f18
f10->f18
t₁₇
η (X₃) = X₂
η (X₄) = 0
τ = 0 ≤ X₁ ∧ X₂ ≤ X₁
f22
f22
f18->f22
t₅
η (X₅) = X₄
η (X₆) = 1+X₄
τ = 0 ≤ X₁ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ 0 ≤ X₁+X₄ ∧ X₄ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₂ ≤ X₃ ∧ 0 ≤ X₄ ∧ 2+X₄ ≤ X₃
f34
f34
f18->f34
t₁₅
η (X₄) = 0
τ = 0 ≤ X₁ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ 0 ≤ X₁+X₄ ∧ X₄ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₂ ≤ X₃ ∧ 0 ≤ X₄ ∧ X₃ ≤ 1+X₄
f22->f18
t₁₃
η (X₄) = 1+X₄
η (X₇) = I
τ = 1 ≤ X₄+X₆ ∧ 1+X₄ ≤ X₆ ∧ 1 ≤ X₆ ∧ 2 ≤ X₁ ∧ 2 ≤ X₁+X₄ ∧ 2+X₄ ≤ X₁ ∧ 2 ≤ X₂ ∧ 2 ≤ X₂+X₄ ∧ 2+X₄ ≤ X₂ ∧ 2 ≤ X₃ ∧ 2 ≤ X₃+X₄ ∧ 2+X₄ ≤ X₃ ∧ 3 ≤ X₁+X₆ ∧ 3 ≤ X₂+X₆ ∧ 3 ≤ X₃+X₆ ∧ 4 ≤ X₁+X₂ ∧ 4 ≤ X₁+X₃ ∧ 4 ≤ X₂+X₃ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ X₆ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₆ ≤ X₂ ∧ X₂ ≤ X₃ ∧ X₆ ≤ X₃ ∧ 0 ≤ X₄ ∧ X₃ ≤ X₆
f22->f22
t₇
η (X₆) = 1+X₆
τ = 1 ≤ X₄+X₆ ∧ 1+X₄ ≤ X₆ ∧ 1 ≤ X₆ ∧ 2 ≤ X₁ ∧ 2 ≤ X₁+X₄ ∧ 2+X₄ ≤ X₁ ∧ 2 ≤ X₂ ∧ 2 ≤ X₂+X₄ ∧ 2+X₄ ≤ X₂ ∧ 2 ≤ X₃ ∧ 2 ≤ X₃+X₄ ∧ 2+X₄ ≤ X₃ ∧ 3 ≤ X₁+X₆ ∧ 3 ≤ X₂+X₆ ∧ 3 ≤ X₃+X₆ ∧ 4 ≤ X₁+X₂ ∧ 4 ≤ X₁+X₃ ∧ 4 ≤ X₂+X₃ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ X₆ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₆ ≤ X₂ ∧ X₂ ≤ X₃ ∧ X₆ ≤ X₃ ∧ 0 ≤ X₄ ∧ 1+X₆ ≤ X₃
f22->f22
t₈
τ = 1 ≤ X₄+X₆ ∧ 1+X₄ ≤ X₆ ∧ 1 ≤ X₆ ∧ 2 ≤ X₁ ∧ 2 ≤ X₁+X₄ ∧ 2+X₄ ≤ X₁ ∧ 2 ≤ X₂ ∧ 2 ≤ X₂+X₄ ∧ 2+X₄ ≤ X₂ ∧ 2 ≤ X₃ ∧ 2 ≤ X₃+X₄ ∧ 2+X₄ ≤ X₃ ∧ 3 ≤ X₁+X₆ ∧ 3 ≤ X₂+X₆ ∧ 3 ≤ X₃+X₆ ∧ 4 ≤ X₁+X₂ ∧ 4 ≤ X₁+X₃ ∧ 4 ≤ X₂+X₃ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ X₆ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₆ ≤ X₂ ∧ X₂ ≤ X₃ ∧ X₆ ≤ X₃ ∧ 0 ≤ X₄ ∧ 1+X₆ ≤ X₃
f22->f22
t₁₀
η (X₅) = X₆
η (X₆) = 1+X₆
τ = 1 ≤ X₄+X₆ ∧ 1+X₄ ≤ X₆ ∧ 1 ≤ X₆ ∧ 2 ≤ X₁ ∧ 2 ≤ X₁+X₄ ∧ 2+X₄ ≤ X₁ ∧ 2 ≤ X₂ ∧ 2 ≤ X₂+X₄ ∧ 2+X₄ ≤ X₂ ∧ 2 ≤ X₃ ∧ 2 ≤ X₃+X₄ ∧ 2+X₄ ≤ X₃ ∧ 3 ≤ X₁+X₆ ∧ 3 ≤ X₂+X₆ ∧ 3 ≤ X₃+X₆ ∧ 4 ≤ X₁+X₂ ∧ 4 ≤ X₁+X₃ ∧ 4 ≤ X₂+X₃ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ X₆ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₆ ≤ X₂ ∧ X₂ ≤ X₃ ∧ X₆ ≤ X₃ ∧ 0 ≤ X₄ ∧ 1+X₆ ≤ X₃
f22->f22
t₁₁
τ = 1 ≤ X₄+X₆ ∧ 1+X₄ ≤ X₆ ∧ 1 ≤ X₆ ∧ 2 ≤ X₁ ∧ 2 ≤ X₁+X₄ ∧ 2+X₄ ≤ X₁ ∧ 2 ≤ X₂ ∧ 2 ≤ X₂+X₄ ∧ 2+X₄ ≤ X₂ ∧ 2 ≤ X₃ ∧ 2 ≤ X₃+X₄ ∧ 2+X₄ ≤ X₃ ∧ 3 ≤ X₁+X₆ ∧ 3 ≤ X₂+X₆ ∧ 3 ≤ X₃+X₆ ∧ 4 ≤ X₁+X₂ ∧ 4 ≤ X₁+X₃ ∧ 4 ≤ X₂+X₃ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ X₆ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₆ ≤ X₂ ∧ X₂ ≤ X₃ ∧ X₆ ≤ X₃ ∧ 0 ≤ X₄ ∧ 1+X₆ ≤ X₃
Classical Approximation after Lifting Classical Results
All Bounds
Timebounds
Overall timebound:inf {Infinity}
g₀: 1 {O(1)}
g₂: X₂ {O(n)}
g₄: inf {Infinity}
g₆: inf {Infinity}
g₉: inf {Infinity}
g₁₂: inf {Infinity}
g₁₄: 1 {O(1)}
g₁₆: 1 {O(1)}
Costbounds
Overall costbound: inf {Infinity}
g₀: inf {Infinity}
g₂: inf {Infinity}
g₄: inf {Infinity}
g₆: inf {Infinity}
g₉: inf {Infinity}
g₁₂: inf {Infinity}
g₁₄: inf {Infinity}
g₁₆: inf {Infinity}
Sizebounds
(g₀,f10), X₁: 0 {O(1)}
(g₀,f10), X₂: X₂ {O(n)}
(g₀,f10), X₃: X₃ {O(n)}
(g₀,f10), X₄: X₄ {O(n)}
(g₀,f10), X₅: X₅ {O(n)}
(g₀,f10), X₆: X₆ {O(n)}
(g₀,f10), X₇: X₇ {O(n)}
(g₂,f10), X₁: X₂ {O(n)}
(g₂,f10), X₂: X₂ {O(n)}
(g₂,f10), X₃: X₃ {O(n)}
(g₂,f10), X₄: X₄ {O(n)}
(g₂,f10), X₅: X₅ {O(n)}
(g₂,f10), X₆: X₆ {O(n)}
(g₂,f10), X₇: X₇ {O(n)}
(g₁₆,f18), X₁: X₂ {O(n)}
(g₁₆,f18), X₂: 2⋅X₂ {O(n)}
(g₁₆,f18), X₃: 2⋅X₂ {O(n)}
(g₁₆,f18), X₄: 0 {O(1)}
(g₁₆,f18), X₅: 2⋅X₅ {O(n)}
(g₁₆,f18), X₆: 2⋅X₆ {O(n)}
(g₁₆,f18), X₇: 2⋅X₇ {O(n)}
Run probabilistic analysis on SCC: [f10]
Run classical analysis on SCC: [f18; f22]
MPRF for transition t₅: f18(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇) → f22(X₀,X₁,X₂,X₃,X₄,X₄,1+X₄,X₇) :|: 0 ≤ X₁ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ 0 ≤ X₁+X₄ ∧ X₄ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₂ ≤ X₃ ∧ 0 ≤ X₄ ∧ 2+X₄ ≤ X₃ of depth 1:
new bound:
X₂+1 {O(n)}
MPRF:
• f18: [1+X₁-X₄]
• f22: [X₁-X₄]
Show Graph
G
f0
f0
f10
f10
f0->f10
t₁
η (X₀) = I
η (X₁) = 0
f10->f10
t₃
η (X₁) = 1+X₁
τ = 0 ≤ X₁ ∧ 1+X₁ ≤ X₂
f18
f18
f10->f18
t₁₇
η (X₃) = X₂
η (X₄) = 0
τ = 0 ≤ X₁ ∧ X₂ ≤ X₁
f22
f22
f18->f22
t₅
η (X₅) = X₄
η (X₆) = 1+X₄
τ = 0 ≤ X₁ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ 0 ≤ X₁+X₄ ∧ X₄ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₂ ≤ X₃ ∧ 0 ≤ X₄ ∧ 2+X₄ ≤ X₃
f34
f34
f18->f34
t₁₅
η (X₄) = 0
τ = 0 ≤ X₁ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ 0 ≤ X₁+X₄ ∧ X₄ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₂ ≤ X₃ ∧ 0 ≤ X₄ ∧ X₃ ≤ 1+X₄
f22->f18
t₁₃
η (X₄) = 1+X₄
η (X₇) = I
τ = 1 ≤ X₄+X₆ ∧ 1+X₄ ≤ X₆ ∧ 1 ≤ X₆ ∧ 2 ≤ X₁ ∧ 2 ≤ X₁+X₄ ∧ 2+X₄ ≤ X₁ ∧ 2 ≤ X₂ ∧ 2 ≤ X₂+X₄ ∧ 2+X₄ ≤ X₂ ∧ 2 ≤ X₃ ∧ 2 ≤ X₃+X₄ ∧ 2+X₄ ≤ X₃ ∧ 3 ≤ X₁+X₆ ∧ 3 ≤ X₂+X₆ ∧ 3 ≤ X₃+X₆ ∧ 4 ≤ X₁+X₂ ∧ 4 ≤ X₁+X₃ ∧ 4 ≤ X₂+X₃ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ X₆ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₆ ≤ X₂ ∧ X₂ ≤ X₃ ∧ X₆ ≤ X₃ ∧ 0 ≤ X₄ ∧ X₃ ≤ X₆
f22->f22
t₇
η (X₆) = 1+X₆
τ = 1 ≤ X₄+X₆ ∧ 1+X₄ ≤ X₆ ∧ 1 ≤ X₆ ∧ 2 ≤ X₁ ∧ 2 ≤ X₁+X₄ ∧ 2+X₄ ≤ X₁ ∧ 2 ≤ X₂ ∧ 2 ≤ X₂+X₄ ∧ 2+X₄ ≤ X₂ ∧ 2 ≤ X₃ ∧ 2 ≤ X₃+X₄ ∧ 2+X₄ ≤ X₃ ∧ 3 ≤ X₁+X₆ ∧ 3 ≤ X₂+X₆ ∧ 3 ≤ X₃+X₆ ∧ 4 ≤ X₁+X₂ ∧ 4 ≤ X₁+X₃ ∧ 4 ≤ X₂+X₃ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ X₆ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₆ ≤ X₂ ∧ X₂ ≤ X₃ ∧ X₆ ≤ X₃ ∧ 0 ≤ X₄ ∧ 1+X₆ ≤ X₃
f22->f22
t₈
τ = 1 ≤ X₄+X₆ ∧ 1+X₄ ≤ X₆ ∧ 1 ≤ X₆ ∧ 2 ≤ X₁ ∧ 2 ≤ X₁+X₄ ∧ 2+X₄ ≤ X₁ ∧ 2 ≤ X₂ ∧ 2 ≤ X₂+X₄ ∧ 2+X₄ ≤ X₂ ∧ 2 ≤ X₃ ∧ 2 ≤ X₃+X₄ ∧ 2+X₄ ≤ X₃ ∧ 3 ≤ X₁+X₆ ∧ 3 ≤ X₂+X₆ ∧ 3 ≤ X₃+X₆ ∧ 4 ≤ X₁+X₂ ∧ 4 ≤ X₁+X₃ ∧ 4 ≤ X₂+X₃ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ X₆ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₆ ≤ X₂ ∧ X₂ ≤ X₃ ∧ X₆ ≤ X₃ ∧ 0 ≤ X₄ ∧ 1+X₆ ≤ X₃
f22->f22
t₁₀
η (X₅) = X₆
η (X₆) = 1+X₆
τ = 1 ≤ X₄+X₆ ∧ 1+X₄ ≤ X₆ ∧ 1 ≤ X₆ ∧ 2 ≤ X₁ ∧ 2 ≤ X₁+X₄ ∧ 2+X₄ ≤ X₁ ∧ 2 ≤ X₂ ∧ 2 ≤ X₂+X₄ ∧ 2+X₄ ≤ X₂ ∧ 2 ≤ X₃ ∧ 2 ≤ X₃+X₄ ∧ 2+X₄ ≤ X₃ ∧ 3 ≤ X₁+X₆ ∧ 3 ≤ X₂+X₆ ∧ 3 ≤ X₃+X₆ ∧ 4 ≤ X₁+X₂ ∧ 4 ≤ X₁+X₃ ∧ 4 ≤ X₂+X₃ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ X₆ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₆ ≤ X₂ ∧ X₂ ≤ X₃ ∧ X₆ ≤ X₃ ∧ 0 ≤ X₄ ∧ 1+X₆ ≤ X₃
f22->f22
t₁₁
τ = 1 ≤ X₄+X₆ ∧ 1+X₄ ≤ X₆ ∧ 1 ≤ X₆ ∧ 2 ≤ X₁ ∧ 2 ≤ X₁+X₄ ∧ 2+X₄ ≤ X₁ ∧ 2 ≤ X₂ ∧ 2 ≤ X₂+X₄ ∧ 2+X₄ ≤ X₂ ∧ 2 ≤ X₃ ∧ 2 ≤ X₃+X₄ ∧ 2+X₄ ≤ X₃ ∧ 3 ≤ X₁+X₆ ∧ 3 ≤ X₂+X₆ ∧ 3 ≤ X₃+X₆ ∧ 4 ≤ X₁+X₂ ∧ 4 ≤ X₁+X₃ ∧ 4 ≤ X₂+X₃ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ X₆ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₆ ≤ X₂ ∧ X₂ ≤ X₃ ∧ X₆ ≤ X₃ ∧ 0 ≤ X₄ ∧ 1+X₆ ≤ X₃
MPRF for transition t₁₃: f22(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇) → f18(X₀,X₁,X₂,X₃,1+X₄,X₅,X₆,I) :|: 1 ≤ X₄+X₆ ∧ 1+X₄ ≤ X₆ ∧ 1 ≤ X₆ ∧ 2 ≤ X₁ ∧ 2 ≤ X₁+X₄ ∧ 2+X₄ ≤ X₁ ∧ 2 ≤ X₂ ∧ 2 ≤ X₂+X₄ ∧ 2+X₄ ≤ X₂ ∧ 2 ≤ X₃ ∧ 2 ≤ X₃+X₄ ∧ 2+X₄ ≤ X₃ ∧ 3 ≤ X₁+X₆ ∧ 3 ≤ X₂+X₆ ∧ 3 ≤ X₃+X₆ ∧ 4 ≤ X₁+X₂ ∧ 4 ≤ X₁+X₃ ∧ 4 ≤ X₂+X₃ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ X₆ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₆ ≤ X₂ ∧ X₂ ≤ X₃ ∧ X₆ ≤ X₃ ∧ 0 ≤ X₄ ∧ X₃ ≤ X₆ of depth 1:
new bound:
2⋅X₂+1 {O(n)}
MPRF:
• f18: [X₃-1-X₄]
• f22: [X₃-1-X₄]
Show Graph
G
f0
f0
f10
f10
f0->f10
t₁
η (X₀) = I
η (X₁) = 0
f10->f10
t₃
η (X₁) = 1+X₁
τ = 0 ≤ X₁ ∧ 1+X₁ ≤ X₂
f18
f18
f10->f18
t₁₇
η (X₃) = X₂
η (X₄) = 0
τ = 0 ≤ X₁ ∧ X₂ ≤ X₁
f22
f22
f18->f22
t₅
η (X₅) = X₄
η (X₆) = 1+X₄
τ = 0 ≤ X₁ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ 0 ≤ X₁+X₄ ∧ X₄ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₂ ≤ X₃ ∧ 0 ≤ X₄ ∧ 2+X₄ ≤ X₃
f34
f34
f18->f34
t₁₅
η (X₄) = 0
τ = 0 ≤ X₁ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ 0 ≤ X₁+X₄ ∧ X₄ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₂ ≤ X₃ ∧ 0 ≤ X₄ ∧ X₃ ≤ 1+X₄
f22->f18
t₁₃
η (X₄) = 1+X₄
η (X₇) = I
τ = 1 ≤ X₄+X₆ ∧ 1+X₄ ≤ X₆ ∧ 1 ≤ X₆ ∧ 2 ≤ X₁ ∧ 2 ≤ X₁+X₄ ∧ 2+X₄ ≤ X₁ ∧ 2 ≤ X₂ ∧ 2 ≤ X₂+X₄ ∧ 2+X₄ ≤ X₂ ∧ 2 ≤ X₃ ∧ 2 ≤ X₃+X₄ ∧ 2+X₄ ≤ X₃ ∧ 3 ≤ X₁+X₆ ∧ 3 ≤ X₂+X₆ ∧ 3 ≤ X₃+X₆ ∧ 4 ≤ X₁+X₂ ∧ 4 ≤ X₁+X₃ ∧ 4 ≤ X₂+X₃ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ X₆ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₆ ≤ X₂ ∧ X₂ ≤ X₃ ∧ X₆ ≤ X₃ ∧ 0 ≤ X₄ ∧ X₃ ≤ X₆
f22->f22
t₇
η (X₆) = 1+X₆
τ = 1 ≤ X₄+X₆ ∧ 1+X₄ ≤ X₆ ∧ 1 ≤ X₆ ∧ 2 ≤ X₁ ∧ 2 ≤ X₁+X₄ ∧ 2+X₄ ≤ X₁ ∧ 2 ≤ X₂ ∧ 2 ≤ X₂+X₄ ∧ 2+X₄ ≤ X₂ ∧ 2 ≤ X₃ ∧ 2 ≤ X₃+X₄ ∧ 2+X₄ ≤ X₃ ∧ 3 ≤ X₁+X₆ ∧ 3 ≤ X₂+X₆ ∧ 3 ≤ X₃+X₆ ∧ 4 ≤ X₁+X₂ ∧ 4 ≤ X₁+X₃ ∧ 4 ≤ X₂+X₃ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ X₆ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₆ ≤ X₂ ∧ X₂ ≤ X₃ ∧ X₆ ≤ X₃ ∧ 0 ≤ X₄ ∧ 1+X₆ ≤ X₃
f22->f22
t₈
τ = 1 ≤ X₄+X₆ ∧ 1+X₄ ≤ X₆ ∧ 1 ≤ X₆ ∧ 2 ≤ X₁ ∧ 2 ≤ X₁+X₄ ∧ 2+X₄ ≤ X₁ ∧ 2 ≤ X₂ ∧ 2 ≤ X₂+X₄ ∧ 2+X₄ ≤ X₂ ∧ 2 ≤ X₃ ∧ 2 ≤ X₃+X₄ ∧ 2+X₄ ≤ X₃ ∧ 3 ≤ X₁+X₆ ∧ 3 ≤ X₂+X₆ ∧ 3 ≤ X₃+X₆ ∧ 4 ≤ X₁+X₂ ∧ 4 ≤ X₁+X₃ ∧ 4 ≤ X₂+X₃ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ X₆ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₆ ≤ X₂ ∧ X₂ ≤ X₃ ∧ X₆ ≤ X₃ ∧ 0 ≤ X₄ ∧ 1+X₆ ≤ X₃
f22->f22
t₁₀
η (X₅) = X₆
η (X₆) = 1+X₆
τ = 1 ≤ X₄+X₆ ∧ 1+X₄ ≤ X₆ ∧ 1 ≤ X₆ ∧ 2 ≤ X₁ ∧ 2 ≤ X₁+X₄ ∧ 2+X₄ ≤ X₁ ∧ 2 ≤ X₂ ∧ 2 ≤ X₂+X₄ ∧ 2+X₄ ≤ X₂ ∧ 2 ≤ X₃ ∧ 2 ≤ X₃+X₄ ∧ 2+X₄ ≤ X₃ ∧ 3 ≤ X₁+X₆ ∧ 3 ≤ X₂+X₆ ∧ 3 ≤ X₃+X₆ ∧ 4 ≤ X₁+X₂ ∧ 4 ≤ X₁+X₃ ∧ 4 ≤ X₂+X₃ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ X₆ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₆ ≤ X₂ ∧ X₂ ≤ X₃ ∧ X₆ ≤ X₃ ∧ 0 ≤ X₄ ∧ 1+X₆ ≤ X₃
f22->f22
t₁₁
τ = 1 ≤ X₄+X₆ ∧ 1+X₄ ≤ X₆ ∧ 1 ≤ X₆ ∧ 2 ≤ X₁ ∧ 2 ≤ X₁+X₄ ∧ 2+X₄ ≤ X₁ ∧ 2 ≤ X₂ ∧ 2 ≤ X₂+X₄ ∧ 2+X₄ ≤ X₂ ∧ 2 ≤ X₃ ∧ 2 ≤ X₃+X₄ ∧ 2+X₄ ≤ X₃ ∧ 3 ≤ X₁+X₆ ∧ 3 ≤ X₂+X₆ ∧ 3 ≤ X₃+X₆ ∧ 4 ≤ X₁+X₂ ∧ 4 ≤ X₁+X₃ ∧ 4 ≤ X₂+X₃ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ X₆ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₆ ≤ X₂ ∧ X₂ ≤ X₃ ∧ X₆ ≤ X₃ ∧ 0 ≤ X₄ ∧ 1+X₆ ≤ X₃
MPRF for transition t₇: f22(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇) → f22(X₀,X₁,X₂,X₃,X₄,X₅,1+X₆,X₇) :|: 1 ≤ X₄+X₆ ∧ 1+X₄ ≤ X₆ ∧ 1 ≤ X₆ ∧ 2 ≤ X₁ ∧ 2 ≤ X₁+X₄ ∧ 2+X₄ ≤ X₁ ∧ 2 ≤ X₂ ∧ 2 ≤ X₂+X₄ ∧ 2+X₄ ≤ X₂ ∧ 2 ≤ X₃ ∧ 2 ≤ X₃+X₄ ∧ 2+X₄ ≤ X₃ ∧ 3 ≤ X₁+X₆ ∧ 3 ≤ X₂+X₆ ∧ 3 ≤ X₃+X₆ ∧ 4 ≤ X₁+X₂ ∧ 4 ≤ X₁+X₃ ∧ 4 ≤ X₂+X₃ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ X₆ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₆ ≤ X₂ ∧ X₂ ≤ X₃ ∧ X₆ ≤ X₃ ∧ 0 ≤ X₄ ∧ 1+X₆ ≤ X₃ of depth 1:
new bound:
4⋅X₂⋅X₂+4⋅X₂ {O(n^2)}
MPRF:
• f18: [X₂]
• f22: [1+X₂-X₆]
Show Graph
G
f0
f0
f10
f10
f0->f10
t₁
η (X₀) = I
η (X₁) = 0
f10->f10
t₃
η (X₁) = 1+X₁
τ = 0 ≤ X₁ ∧ 1+X₁ ≤ X₂
f18
f18
f10->f18
t₁₇
η (X₃) = X₂
η (X₄) = 0
τ = 0 ≤ X₁ ∧ X₂ ≤ X₁
f22
f22
f18->f22
t₅
η (X₅) = X₄
η (X₆) = 1+X₄
τ = 0 ≤ X₁ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ 0 ≤ X₁+X₄ ∧ X₄ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₂ ≤ X₃ ∧ 0 ≤ X₄ ∧ 2+X₄ ≤ X₃
f34
f34
f18->f34
t₁₅
η (X₄) = 0
τ = 0 ≤ X₁ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ 0 ≤ X₁+X₄ ∧ X₄ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₂ ≤ X₃ ∧ 0 ≤ X₄ ∧ X₃ ≤ 1+X₄
f22->f18
t₁₃
η (X₄) = 1+X₄
η (X₇) = I
τ = 1 ≤ X₄+X₆ ∧ 1+X₄ ≤ X₆ ∧ 1 ≤ X₆ ∧ 2 ≤ X₁ ∧ 2 ≤ X₁+X₄ ∧ 2+X₄ ≤ X₁ ∧ 2 ≤ X₂ ∧ 2 ≤ X₂+X₄ ∧ 2+X₄ ≤ X₂ ∧ 2 ≤ X₃ ∧ 2 ≤ X₃+X₄ ∧ 2+X₄ ≤ X₃ ∧ 3 ≤ X₁+X₆ ∧ 3 ≤ X₂+X₆ ∧ 3 ≤ X₃+X₆ ∧ 4 ≤ X₁+X₂ ∧ 4 ≤ X₁+X₃ ∧ 4 ≤ X₂+X₃ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ X₆ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₆ ≤ X₂ ∧ X₂ ≤ X₃ ∧ X₆ ≤ X₃ ∧ 0 ≤ X₄ ∧ X₃ ≤ X₆
f22->f22
t₇
η (X₆) = 1+X₆
τ = 1 ≤ X₄+X₆ ∧ 1+X₄ ≤ X₆ ∧ 1 ≤ X₆ ∧ 2 ≤ X₁ ∧ 2 ≤ X₁+X₄ ∧ 2+X₄ ≤ X₁ ∧ 2 ≤ X₂ ∧ 2 ≤ X₂+X₄ ∧ 2+X₄ ≤ X₂ ∧ 2 ≤ X₃ ∧ 2 ≤ X₃+X₄ ∧ 2+X₄ ≤ X₃ ∧ 3 ≤ X₁+X₆ ∧ 3 ≤ X₂+X₆ ∧ 3 ≤ X₃+X₆ ∧ 4 ≤ X₁+X₂ ∧ 4 ≤ X₁+X₃ ∧ 4 ≤ X₂+X₃ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ X₆ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₆ ≤ X₂ ∧ X₂ ≤ X₃ ∧ X₆ ≤ X₃ ∧ 0 ≤ X₄ ∧ 1+X₆ ≤ X₃
f22->f22
t₈
τ = 1 ≤ X₄+X₆ ∧ 1+X₄ ≤ X₆ ∧ 1 ≤ X₆ ∧ 2 ≤ X₁ ∧ 2 ≤ X₁+X₄ ∧ 2+X₄ ≤ X₁ ∧ 2 ≤ X₂ ∧ 2 ≤ X₂+X₄ ∧ 2+X₄ ≤ X₂ ∧ 2 ≤ X₃ ∧ 2 ≤ X₃+X₄ ∧ 2+X₄ ≤ X₃ ∧ 3 ≤ X₁+X₆ ∧ 3 ≤ X₂+X₆ ∧ 3 ≤ X₃+X₆ ∧ 4 ≤ X₁+X₂ ∧ 4 ≤ X₁+X₃ ∧ 4 ≤ X₂+X₃ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ X₆ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₆ ≤ X₂ ∧ X₂ ≤ X₃ ∧ X₆ ≤ X₃ ∧ 0 ≤ X₄ ∧ 1+X₆ ≤ X₃
f22->f22
t₁₀
η (X₅) = X₆
η (X₆) = 1+X₆
τ = 1 ≤ X₄+X₆ ∧ 1+X₄ ≤ X₆ ∧ 1 ≤ X₆ ∧ 2 ≤ X₁ ∧ 2 ≤ X₁+X₄ ∧ 2+X₄ ≤ X₁ ∧ 2 ≤ X₂ ∧ 2 ≤ X₂+X₄ ∧ 2+X₄ ≤ X₂ ∧ 2 ≤ X₃ ∧ 2 ≤ X₃+X₄ ∧ 2+X₄ ≤ X₃ ∧ 3 ≤ X₁+X₆ ∧ 3 ≤ X₂+X₆ ∧ 3 ≤ X₃+X₆ ∧ 4 ≤ X₁+X₂ ∧ 4 ≤ X₁+X₃ ∧ 4 ≤ X₂+X₃ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ X₆ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₆ ≤ X₂ ∧ X₂ ≤ X₃ ∧ X₆ ≤ X₃ ∧ 0 ≤ X₄ ∧ 1+X₆ ≤ X₃
f22->f22
t₁₁
τ = 1 ≤ X₄+X₆ ∧ 1+X₄ ≤ X₆ ∧ 1 ≤ X₆ ∧ 2 ≤ X₁ ∧ 2 ≤ X₁+X₄ ∧ 2+X₄ ≤ X₁ ∧ 2 ≤ X₂ ∧ 2 ≤ X₂+X₄ ∧ 2+X₄ ≤ X₂ ∧ 2 ≤ X₃ ∧ 2 ≤ X₃+X₄ ∧ 2+X₄ ≤ X₃ ∧ 3 ≤ X₁+X₆ ∧ 3 ≤ X₂+X₆ ∧ 3 ≤ X₃+X₆ ∧ 4 ≤ X₁+X₂ ∧ 4 ≤ X₁+X₃ ∧ 4 ≤ X₂+X₃ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ X₆ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₆ ≤ X₂ ∧ X₂ ≤ X₃ ∧ X₆ ≤ X₃ ∧ 0 ≤ X₄ ∧ 1+X₆ ≤ X₃
MPRF for transition t₁₀: f22(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇) → f22(X₀,X₁,X₂,X₃,X₄,X₆,1+X₆,X₇) :|: 1 ≤ X₄+X₆ ∧ 1+X₄ ≤ X₆ ∧ 1 ≤ X₆ ∧ 2 ≤ X₁ ∧ 2 ≤ X₁+X₄ ∧ 2+X₄ ≤ X₁ ∧ 2 ≤ X₂ ∧ 2 ≤ X₂+X₄ ∧ 2+X₄ ≤ X₂ ∧ 2 ≤ X₃ ∧ 2 ≤ X₃+X₄ ∧ 2+X₄ ≤ X₃ ∧ 3 ≤ X₁+X₆ ∧ 3 ≤ X₂+X₆ ∧ 3 ≤ X₃+X₆ ∧ 4 ≤ X₁+X₂ ∧ 4 ≤ X₁+X₃ ∧ 4 ≤ X₂+X₃ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ X₆ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₆ ≤ X₂ ∧ X₂ ≤ X₃ ∧ X₆ ≤ X₃ ∧ 0 ≤ X₄ ∧ 1+X₆ ≤ X₃ of depth 1:
new bound:
8⋅X₂⋅X₂+8⋅X₂+1 {O(n^2)}
MPRF:
• f18: [X₂-X₄]
• f22: [1+X₂-X₆]
Show Graph
G
f0
f0
f10
f10
f0->f10
t₁
η (X₀) = I
η (X₁) = 0
f10->f10
t₃
η (X₁) = 1+X₁
τ = 0 ≤ X₁ ∧ 1+X₁ ≤ X₂
f18
f18
f10->f18
t₁₇
η (X₃) = X₂
η (X₄) = 0
τ = 0 ≤ X₁ ∧ X₂ ≤ X₁
f22
f22
f18->f22
t₅
η (X₅) = X₄
η (X₆) = 1+X₄
τ = 0 ≤ X₁ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ 0 ≤ X₁+X₄ ∧ X₄ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₂ ≤ X₃ ∧ 0 ≤ X₄ ∧ 2+X₄ ≤ X₃
f34
f34
f18->f34
t₁₅
η (X₄) = 0
τ = 0 ≤ X₁ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ 0 ≤ X₁+X₄ ∧ X₄ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₂ ≤ X₃ ∧ 0 ≤ X₄ ∧ X₃ ≤ 1+X₄
f22->f18
t₁₃
η (X₄) = 1+X₄
η (X₇) = I
τ = 1 ≤ X₄+X₆ ∧ 1+X₄ ≤ X₆ ∧ 1 ≤ X₆ ∧ 2 ≤ X₁ ∧ 2 ≤ X₁+X₄ ∧ 2+X₄ ≤ X₁ ∧ 2 ≤ X₂ ∧ 2 ≤ X₂+X₄ ∧ 2+X₄ ≤ X₂ ∧ 2 ≤ X₃ ∧ 2 ≤ X₃+X₄ ∧ 2+X₄ ≤ X₃ ∧ 3 ≤ X₁+X₆ ∧ 3 ≤ X₂+X₆ ∧ 3 ≤ X₃+X₆ ∧ 4 ≤ X₁+X₂ ∧ 4 ≤ X₁+X₃ ∧ 4 ≤ X₂+X₃ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ X₆ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₆ ≤ X₂ ∧ X₂ ≤ X₃ ∧ X₆ ≤ X₃ ∧ 0 ≤ X₄ ∧ X₃ ≤ X₆
f22->f22
t₇
η (X₆) = 1+X₆
τ = 1 ≤ X₄+X₆ ∧ 1+X₄ ≤ X₆ ∧ 1 ≤ X₆ ∧ 2 ≤ X₁ ∧ 2 ≤ X₁+X₄ ∧ 2+X₄ ≤ X₁ ∧ 2 ≤ X₂ ∧ 2 ≤ X₂+X₄ ∧ 2+X₄ ≤ X₂ ∧ 2 ≤ X₃ ∧ 2 ≤ X₃+X₄ ∧ 2+X₄ ≤ X₃ ∧ 3 ≤ X₁+X₆ ∧ 3 ≤ X₂+X₆ ∧ 3 ≤ X₃+X₆ ∧ 4 ≤ X₁+X₂ ∧ 4 ≤ X₁+X₃ ∧ 4 ≤ X₂+X₃ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ X₆ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₆ ≤ X₂ ∧ X₂ ≤ X₃ ∧ X₆ ≤ X₃ ∧ 0 ≤ X₄ ∧ 1+X₆ ≤ X₃
f22->f22
t₈
τ = 1 ≤ X₄+X₆ ∧ 1+X₄ ≤ X₆ ∧ 1 ≤ X₆ ∧ 2 ≤ X₁ ∧ 2 ≤ X₁+X₄ ∧ 2+X₄ ≤ X₁ ∧ 2 ≤ X₂ ∧ 2 ≤ X₂+X₄ ∧ 2+X₄ ≤ X₂ ∧ 2 ≤ X₃ ∧ 2 ≤ X₃+X₄ ∧ 2+X₄ ≤ X₃ ∧ 3 ≤ X₁+X₆ ∧ 3 ≤ X₂+X₆ ∧ 3 ≤ X₃+X₆ ∧ 4 ≤ X₁+X₂ ∧ 4 ≤ X₁+X₃ ∧ 4 ≤ X₂+X₃ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ X₆ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₆ ≤ X₂ ∧ X₂ ≤ X₃ ∧ X₆ ≤ X₃ ∧ 0 ≤ X₄ ∧ 1+X₆ ≤ X₃
f22->f22
t₁₀
η (X₅) = X₆
η (X₆) = 1+X₆
τ = 1 ≤ X₄+X₆ ∧ 1+X₄ ≤ X₆ ∧ 1 ≤ X₆ ∧ 2 ≤ X₁ ∧ 2 ≤ X₁+X₄ ∧ 2+X₄ ≤ X₁ ∧ 2 ≤ X₂ ∧ 2 ≤ X₂+X₄ ∧ 2+X₄ ≤ X₂ ∧ 2 ≤ X₃ ∧ 2 ≤ X₃+X₄ ∧ 2+X₄ ≤ X₃ ∧ 3 ≤ X₁+X₆ ∧ 3 ≤ X₂+X₆ ∧ 3 ≤ X₃+X₆ ∧ 4 ≤ X₁+X₂ ∧ 4 ≤ X₁+X₃ ∧ 4 ≤ X₂+X₃ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ X₆ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₆ ≤ X₂ ∧ X₂ ≤ X₃ ∧ X₆ ≤ X₃ ∧ 0 ≤ X₄ ∧ 1+X₆ ≤ X₃
f22->f22
t₁₁
τ = 1 ≤ X₄+X₆ ∧ 1+X₄ ≤ X₆ ∧ 1 ≤ X₆ ∧ 2 ≤ X₁ ∧ 2 ≤ X₁+X₄ ∧ 2+X₄ ≤ X₁ ∧ 2 ≤ X₂ ∧ 2 ≤ X₂+X₄ ∧ 2+X₄ ≤ X₂ ∧ 2 ≤ X₃ ∧ 2 ≤ X₃+X₄ ∧ 2+X₄ ≤ X₃ ∧ 3 ≤ X₁+X₆ ∧ 3 ≤ X₂+X₆ ∧ 3 ≤ X₃+X₆ ∧ 4 ≤ X₁+X₂ ∧ 4 ≤ X₁+X₃ ∧ 4 ≤ X₂+X₃ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ X₆ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₆ ≤ X₂ ∧ X₂ ≤ X₃ ∧ X₆ ≤ X₃ ∧ 0 ≤ X₄ ∧ 1+X₆ ≤ X₃
Classical Approximation after Lifting Classical Results
All Bounds
Timebounds
Overall timebound:inf {Infinity}
g₀: 1 {O(1)}
g₂: X₂ {O(n)}
g₄: X₂+1 {O(n)}
g₆: inf {Infinity}
g₉: inf {Infinity}
g₁₂: 2⋅X₂+1 {O(n)}
g₁₄: 1 {O(1)}
g₁₆: 1 {O(1)}
Costbounds
Overall costbound: inf {Infinity}
g₀: inf {Infinity}
g₂: inf {Infinity}
g₄: inf {Infinity}
g₆: inf {Infinity}
g₉: inf {Infinity}
g₁₂: inf {Infinity}
g₁₄: inf {Infinity}
g₁₆: inf {Infinity}
Sizebounds
(g₀,f10), X₁: 0 {O(1)}
(g₀,f10), X₂: X₂ {O(n)}
(g₀,f10), X₃: X₃ {O(n)}
(g₀,f10), X₄: X₄ {O(n)}
(g₀,f10), X₅: X₅ {O(n)}
(g₀,f10), X₆: X₆ {O(n)}
(g₀,f10), X₇: X₇ {O(n)}
(g₂,f10), X₁: X₂ {O(n)}
(g₂,f10), X₂: X₂ {O(n)}
(g₂,f10), X₃: X₃ {O(n)}
(g₂,f10), X₄: X₄ {O(n)}
(g₂,f10), X₅: X₅ {O(n)}
(g₂,f10), X₆: X₆ {O(n)}
(g₂,f10), X₇: X₇ {O(n)}
(g₄,f22), X₁: X₂ {O(n)}
(g₄,f22), X₂: 2⋅X₂ {O(n)}
(g₄,f22), X₃: 2⋅X₂ {O(n)}
(g₄,f22), X₄: 2⋅X₂+1 {O(n)}
(g₄,f22), X₅: 2⋅X₂+1 {O(n)}
(g₄,f22), X₆: 2⋅X₂+3 {O(n)}
(g₆,f22), X₁: 2⋅X₂ {O(n)}
(g₆,f22), X₂: 4⋅X₂ {O(n)}
(g₆,f22), X₃: 4⋅X₂ {O(n)}
(g₆,f22), X₄: 4⋅X₂+2 {O(n)}
(g₆,f22), X₅: 96⋅X₂⋅X₂+120⋅X₂+40 {O(n^2)}
(g₆,f22), X₆: 24⋅X₂⋅X₂+28⋅X₂+8 {O(n^2)}
(g₉,f22), X₁: 2⋅X₂ {O(n)}
(g₉,f22), X₂: 4⋅X₂ {O(n)}
(g₉,f22), X₃: 4⋅X₂ {O(n)}
(g₉,f22), X₄: 4⋅X₂+2 {O(n)}
(g₉,f22), X₅: 96⋅X₂⋅X₂+118⋅X₂+39 {O(n^2)}
(g₉,f22), X₆: 24⋅X₂⋅X₂+28⋅X₂+8 {O(n^2)}
(g₁₂,f18), X₁: X₂ {O(n)}
(g₁₂,f18), X₂: 2⋅X₂ {O(n)}
(g₁₂,f18), X₃: 2⋅X₂ {O(n)}
(g₁₂,f18), X₄: 2⋅X₂+1 {O(n)}
(g₁₂,f18), X₅: 96⋅X₂⋅X₂+118⋅X₂+39 {O(n^2)}
(g₁₂,f18), X₆: 24⋅X₂⋅X₂+28⋅X₂+8 {O(n^2)}
(g₁₄,f34), X₁: 2⋅X₂ {O(n)}
(g₁₄,f34), X₂: 4⋅X₂ {O(n)}
(g₁₄,f34), X₃: 4⋅X₂ {O(n)}
(g₁₄,f34), X₄: 0 {O(1)}
(g₁₄,f34), X₅: 96⋅X₂⋅X₂+118⋅X₂+2⋅X₅+39 {O(n^2)}
(g₁₄,f34), X₆: 24⋅X₂⋅X₂+2⋅X₆+28⋅X₂+8 {O(n^2)}
(g₁₆,f18), X₁: X₂ {O(n)}
(g₁₆,f18), X₂: 2⋅X₂ {O(n)}
(g₁₆,f18), X₃: 2⋅X₂ {O(n)}
(g₁₆,f18), X₄: 0 {O(1)}
(g₁₆,f18), X₅: 2⋅X₅ {O(n)}
(g₁₆,f18), X₆: 2⋅X₆ {O(n)}
(g₁₆,f18), X₇: 2⋅X₇ {O(n)}
Run probabilistic analysis on SCC: [f18; f22]
Plrf for transition g₆:f22(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇) → [1/2]:t₇:f22(X₀,X₁,X₂,X₃,X₄,X₅,1+X₆,X₇) :+: [1/2]:t₈:f22(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇) :|: 1+X₆ ≤ X₃ ∧ 1 ≤ X₄+X₆ ∧ 1+X₄ ≤ X₆ ∧ 1 ≤ X₆ ∧ 2 ≤ X₁ ∧ 2 ≤ X₁+X₄ ∧ 2+X₄ ≤ X₁ ∧ 2 ≤ X₂ ∧ 2 ≤ X₂+X₄ ∧ 2+X₄ ≤ X₂ ∧ 2 ≤ X₃ ∧ 2 ≤ X₃+X₄ ∧ 2+X₄ ≤ X₃ ∧ 3 ≤ X₁+X₆ ∧ 3 ≤ X₂+X₆ ∧ 3 ≤ X₃+X₆ ∧ 4 ≤ X₁+X₂ ∧ 4 ≤ X₁+X₃ ∧ 4 ≤ X₂+X₃ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ X₆ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₆ ≤ X₂ ∧ X₂ ≤ X₃ ∧ X₆ ≤ X₃ ∧ 0 ≤ X₄:
new bound:
16⋅X₂⋅X₂+16⋅X₂ {O(n^2)}
PLRF:
• f18: 4⋅X₁-2⋅X₂
• f22: 2⋅X₁-2⋅X₆
Show Graph
G
f0
f0
f10
f10
f0->f10
p = 1
t₁ ∈ g₀
η (X₁) = 0
f10->f10
p = 1
t₃ ∈ g₂
η (X₁) = 1+X₁
τ = 0 ≤ X₁ ∧ 1+X₁ ≤ X₂
f18
f18
f10->f18
p = 1
t₁₇ ∈ g₁₆
η (X₃) = X₂
η (X₄) = 0
τ = 0 ≤ X₁ ∧ X₂ ≤ X₁
f22
f22
f18->f22
p = 1
t₅ ∈ g₄
η (X₅) = X₄
η (X₆) = 1+X₄
τ = 0 ≤ X₁ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ 0 ≤ X₁+X₄ ∧ X₄ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₂ ≤ X₃ ∧ 0 ≤ X₄ ∧ 2+X₄ ≤ X₃
f34
f34
f18->f34
p = 1
t₁₅ ∈ g₁₄
η (X₄) = 0
τ = 0 ≤ X₁ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ 0 ≤ X₁+X₄ ∧ X₄ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₂ ≤ X₃ ∧ 0 ≤ X₄ ∧ X₃ ≤ 1+X₄
f22->f18
p = 1
t₁₃ ∈ g₁₂
η (X₄) = 1+X₄
η (X₇) = I
τ = 1 ≤ X₄+X₆ ∧ 1+X₄ ≤ X₆ ∧ 1 ≤ X₆ ∧ 2 ≤ X₁ ∧ 2 ≤ X₁+X₄ ∧ 2+X₄ ≤ X₁ ∧ 2 ≤ X₂ ∧ 2 ≤ X₂+X₄ ∧ 2+X₄ ≤ X₂ ∧ 2 ≤ X₃ ∧ 2 ≤ X₃+X₄ ∧ 2+X₄ ≤ X₃ ∧ 3 ≤ X₁+X₆ ∧ 3 ≤ X₂+X₆ ∧ 3 ≤ X₃+X₆ ∧ 4 ≤ X₁+X₂ ∧ 4 ≤ X₁+X₃ ∧ 4 ≤ X₂+X₃ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ X₆ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₆ ≤ X₂ ∧ X₂ ≤ X₃ ∧ X₆ ≤ X₃ ∧ 0 ≤ X₄ ∧ X₃ ≤ X₆
f22->f22
p = 1/2
t₇ ∈ g₆
η (X₆) = 1+X₆
τ = 1 ≤ X₄+X₆ ∧ 1+X₄ ≤ X₆ ∧ 1 ≤ X₆ ∧ 2 ≤ X₁ ∧ 2 ≤ X₁+X₄ ∧ 2+X₄ ≤ X₁ ∧ 2 ≤ X₂ ∧ 2 ≤ X₂+X₄ ∧ 2+X₄ ≤ X₂ ∧ 2 ≤ X₃ ∧ 2 ≤ X₃+X₄ ∧ 2+X₄ ≤ X₃ ∧ 3 ≤ X₁+X₆ ∧ 3 ≤ X₂+X₆ ∧ 3 ≤ X₃+X₆ ∧ 4 ≤ X₁+X₂ ∧ 4 ≤ X₁+X₃ ∧ 4 ≤ X₂+X₃ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ X₆ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₆ ≤ X₂ ∧ X₂ ≤ X₃ ∧ X₆ ≤ X₃ ∧ 0 ≤ X₄ ∧ 1+X₆ ≤ X₃
f22->f22
p = 1/2
t₈ ∈ g₆
τ = 1 ≤ X₄+X₆ ∧ 1+X₄ ≤ X₆ ∧ 1 ≤ X₆ ∧ 2 ≤ X₁ ∧ 2 ≤ X₁+X₄ ∧ 2+X₄ ≤ X₁ ∧ 2 ≤ X₂ ∧ 2 ≤ X₂+X₄ ∧ 2+X₄ ≤ X₂ ∧ 2 ≤ X₃ ∧ 2 ≤ X₃+X₄ ∧ 2+X₄ ≤ X₃ ∧ 3 ≤ X₁+X₆ ∧ 3 ≤ X₂+X₆ ∧ 3 ≤ X₃+X₆ ∧ 4 ≤ X₁+X₂ ∧ 4 ≤ X₁+X₃ ∧ 4 ≤ X₂+X₃ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ X₆ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₆ ≤ X₂ ∧ X₂ ≤ X₃ ∧ X₆ ≤ X₃ ∧ 0 ≤ X₄ ∧ 1+X₆ ≤ X₃
f22->f22
p = 1/2
t₁₀ ∈ g₉
η (X₅) = X₆
η (X₆) = 1+X₆
τ = 1 ≤ X₄+X₆ ∧ 1+X₄ ≤ X₆ ∧ 1 ≤ X₆ ∧ 2 ≤ X₁ ∧ 2 ≤ X₁+X₄ ∧ 2+X₄ ≤ X₁ ∧ 2 ≤ X₂ ∧ 2 ≤ X₂+X₄ ∧ 2+X₄ ≤ X₂ ∧ 2 ≤ X₃ ∧ 2 ≤ X₃+X₄ ∧ 2+X₄ ≤ X₃ ∧ 3 ≤ X₁+X₆ ∧ 3 ≤ X₂+X₆ ∧ 3 ≤ X₃+X₆ ∧ 4 ≤ X₁+X₂ ∧ 4 ≤ X₁+X₃ ∧ 4 ≤ X₂+X₃ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ X₆ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₆ ≤ X₂ ∧ X₂ ≤ X₃ ∧ X₆ ≤ X₃ ∧ 0 ≤ X₄ ∧ 1+X₆ ≤ X₃
f22->f22
p = 1/2
t₁₁ ∈ g₉
τ = 1 ≤ X₄+X₆ ∧ 1+X₄ ≤ X₆ ∧ 1 ≤ X₆ ∧ 2 ≤ X₁ ∧ 2 ≤ X₁+X₄ ∧ 2+X₄ ≤ X₁ ∧ 2 ≤ X₂ ∧ 2 ≤ X₂+X₄ ∧ 2+X₄ ≤ X₂ ∧ 2 ≤ X₃ ∧ 2 ≤ X₃+X₄ ∧ 2+X₄ ≤ X₃ ∧ 3 ≤ X₁+X₆ ∧ 3 ≤ X₂+X₆ ∧ 3 ≤ X₃+X₆ ∧ 4 ≤ X₁+X₂ ∧ 4 ≤ X₁+X₃ ∧ 4 ≤ X₂+X₃ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ X₆ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₆ ≤ X₂ ∧ X₂ ≤ X₃ ∧ X₆ ≤ X₃ ∧ 0 ≤ X₄ ∧ 1+X₆ ≤ X₃
Use expected size bounds for entry point (g₁₂:f22→[t₁₃:1:f18],f18)
Use expected size bounds for entry point (g₁₂:f22→[t₁₃:1:f18],f18)
Use classical time bound for entry point (g₁₂:f22→[t₁₃:1:f18],f18)
Use expected size bounds for entry point (g₁₆:f10→[t₁₇:1:f18],f18)
Use expected size bounds for entry point (g₁₆:f10→[t₁₇:1:f18],f18)
Use classical time bound for entry point (g₁₆:f10→[t₁₇:1:f18],f18)
Plrf for transition g₉:f22(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇) → [1/2]:t₁₀:f22(X₀,X₁,X₂,X₃,X₄,X₆,1+X₆,X₇) :+: [1/2]:t₁₁:f22(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇) :|: 1+X₆ ≤ X₃ ∧ 1 ≤ X₄+X₆ ∧ 1+X₄ ≤ X₆ ∧ 1 ≤ X₆ ∧ 2 ≤ X₁ ∧ 2 ≤ X₁+X₄ ∧ 2+X₄ ≤ X₁ ∧ 2 ≤ X₂ ∧ 2 ≤ X₂+X₄ ∧ 2+X₄ ≤ X₂ ∧ 2 ≤ X₃ ∧ 2 ≤ X₃+X₄ ∧ 2+X₄ ≤ X₃ ∧ 3 ≤ X₁+X₆ ∧ 3 ≤ X₂+X₆ ∧ 3 ≤ X₃+X₆ ∧ 4 ≤ X₁+X₂ ∧ 4 ≤ X₁+X₃ ∧ 4 ≤ X₂+X₃ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ X₆ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₆ ≤ X₂ ∧ X₂ ≤ X₃ ∧ X₆ ≤ X₃ ∧ 0 ≤ X₄:
new bound:
20⋅X₂⋅X₂+20⋅X₂ {O(n^2)}
PLRF:
• f18: 2⋅X₁+2⋅X₃-2⋅X₂
• f22: 2⋅X₁-2⋅X₆
Show Graph
G
f0
f0
f10
f10
f0->f10
p = 1
t₁ ∈ g₀
η (X₁) = 0
f10->f10
p = 1
t₃ ∈ g₂
η (X₁) = 1+X₁
τ = 0 ≤ X₁ ∧ 1+X₁ ≤ X₂
f18
f18
f10->f18
p = 1
t₁₇ ∈ g₁₆
η (X₃) = X₂
η (X₄) = 0
τ = 0 ≤ X₁ ∧ X₂ ≤ X₁
f22
f22
f18->f22
p = 1
t₅ ∈ g₄
η (X₅) = X₄
η (X₆) = 1+X₄
τ = 0 ≤ X₁ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ 0 ≤ X₁+X₄ ∧ X₄ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₂ ≤ X₃ ∧ 0 ≤ X₄ ∧ 2+X₄ ≤ X₃
f34
f34
f18->f34
p = 1
t₁₅ ∈ g₁₄
η (X₄) = 0
τ = 0 ≤ X₁ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ 0 ≤ X₁+X₄ ∧ X₄ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₂ ≤ X₃ ∧ 0 ≤ X₄ ∧ X₃ ≤ 1+X₄
f22->f18
p = 1
t₁₃ ∈ g₁₂
η (X₄) = 1+X₄
η (X₇) = I
τ = 1 ≤ X₄+X₆ ∧ 1+X₄ ≤ X₆ ∧ 1 ≤ X₆ ∧ 2 ≤ X₁ ∧ 2 ≤ X₁+X₄ ∧ 2+X₄ ≤ X₁ ∧ 2 ≤ X₂ ∧ 2 ≤ X₂+X₄ ∧ 2+X₄ ≤ X₂ ∧ 2 ≤ X₃ ∧ 2 ≤ X₃+X₄ ∧ 2+X₄ ≤ X₃ ∧ 3 ≤ X₁+X₆ ∧ 3 ≤ X₂+X₆ ∧ 3 ≤ X₃+X₆ ∧ 4 ≤ X₁+X₂ ∧ 4 ≤ X₁+X₃ ∧ 4 ≤ X₂+X₃ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ X₆ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₆ ≤ X₂ ∧ X₂ ≤ X₃ ∧ X₆ ≤ X₃ ∧ 0 ≤ X₄ ∧ X₃ ≤ X₆
f22->f22
p = 1/2
t₇ ∈ g₆
η (X₆) = 1+X₆
τ = 1 ≤ X₄+X₆ ∧ 1+X₄ ≤ X₆ ∧ 1 ≤ X₆ ∧ 2 ≤ X₁ ∧ 2 ≤ X₁+X₄ ∧ 2+X₄ ≤ X₁ ∧ 2 ≤ X₂ ∧ 2 ≤ X₂+X₄ ∧ 2+X₄ ≤ X₂ ∧ 2 ≤ X₃ ∧ 2 ≤ X₃+X₄ ∧ 2+X₄ ≤ X₃ ∧ 3 ≤ X₁+X₆ ∧ 3 ≤ X₂+X₆ ∧ 3 ≤ X₃+X₆ ∧ 4 ≤ X₁+X₂ ∧ 4 ≤ X₁+X₃ ∧ 4 ≤ X₂+X₃ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ X₆ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₆ ≤ X₂ ∧ X₂ ≤ X₃ ∧ X₆ ≤ X₃ ∧ 0 ≤ X₄ ∧ 1+X₆ ≤ X₃
f22->f22
p = 1/2
t₈ ∈ g₆
τ = 1 ≤ X₄+X₆ ∧ 1+X₄ ≤ X₆ ∧ 1 ≤ X₆ ∧ 2 ≤ X₁ ∧ 2 ≤ X₁+X₄ ∧ 2+X₄ ≤ X₁ ∧ 2 ≤ X₂ ∧ 2 ≤ X₂+X₄ ∧ 2+X₄ ≤ X₂ ∧ 2 ≤ X₃ ∧ 2 ≤ X₃+X₄ ∧ 2+X₄ ≤ X₃ ∧ 3 ≤ X₁+X₆ ∧ 3 ≤ X₂+X₆ ∧ 3 ≤ X₃+X₆ ∧ 4 ≤ X₁+X₂ ∧ 4 ≤ X₁+X₃ ∧ 4 ≤ X₂+X₃ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ X₆ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₆ ≤ X₂ ∧ X₂ ≤ X₃ ∧ X₆ ≤ X₃ ∧ 0 ≤ X₄ ∧ 1+X₆ ≤ X₃
f22->f22
p = 1/2
t₁₀ ∈ g₉
η (X₅) = X₆
η (X₆) = 1+X₆
τ = 1 ≤ X₄+X₆ ∧ 1+X₄ ≤ X₆ ∧ 1 ≤ X₆ ∧ 2 ≤ X₁ ∧ 2 ≤ X₁+X₄ ∧ 2+X₄ ≤ X₁ ∧ 2 ≤ X₂ ∧ 2 ≤ X₂+X₄ ∧ 2+X₄ ≤ X₂ ∧ 2 ≤ X₃ ∧ 2 ≤ X₃+X₄ ∧ 2+X₄ ≤ X₃ ∧ 3 ≤ X₁+X₆ ∧ 3 ≤ X₂+X₆ ∧ 3 ≤ X₃+X₆ ∧ 4 ≤ X₁+X₂ ∧ 4 ≤ X₁+X₃ ∧ 4 ≤ X₂+X₃ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ X₆ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₆ ≤ X₂ ∧ X₂ ≤ X₃ ∧ X₆ ≤ X₃ ∧ 0 ≤ X₄ ∧ 1+X₆ ≤ X₃
f22->f22
p = 1/2
t₁₁ ∈ g₉
τ = 1 ≤ X₄+X₆ ∧ 1+X₄ ≤ X₆ ∧ 1 ≤ X₆ ∧ 2 ≤ X₁ ∧ 2 ≤ X₁+X₄ ∧ 2+X₄ ≤ X₁ ∧ 2 ≤ X₂ ∧ 2 ≤ X₂+X₄ ∧ 2+X₄ ≤ X₂ ∧ 2 ≤ X₃ ∧ 2 ≤ X₃+X₄ ∧ 2+X₄ ≤ X₃ ∧ 3 ≤ X₁+X₆ ∧ 3 ≤ X₂+X₆ ∧ 3 ≤ X₃+X₆ ∧ 4 ≤ X₁+X₂ ∧ 4 ≤ X₁+X₃ ∧ 4 ≤ X₂+X₃ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ X₆ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₆ ≤ X₂ ∧ X₂ ≤ X₃ ∧ X₆ ≤ X₃ ∧ 0 ≤ X₄ ∧ 1+X₆ ≤ X₃
Use expected size bounds for entry point (g₁₂:f22→[t₁₃:1:f18],f18)
Use expected size bounds for entry point (g₁₂:f22→[t₁₃:1:f18],f18)
Use expected size bounds for entry point (g₁₂:f22→[t₁₃:1:f18],f18)
Use classical time bound for entry point (g₁₂:f22→[t₁₃:1:f18],f18)
Use expected size bounds for entry point (g₁₆:f10→[t₁₇:1:f18],f18)
Use expected size bounds for entry point (g₁₆:f10→[t₁₇:1:f18],f18)
Use expected size bounds for entry point (g₁₆:f10→[t₁₇:1:f18],f18)
Use classical time bound for entry point (g₁₆:f10→[t₁₇:1:f18],f18)
Run classical analysis on SCC: [f34]
Classical Approximation after Lifting Classical Results
All Bounds
Timebounds
Overall timebound:36⋅X₂⋅X₂+40⋅X₂+5 {O(n^2)}
g₀: 1 {O(1)}
g₂: X₂ {O(n)}
g₄: X₂+1 {O(n)}
g₆: 16⋅X₂⋅X₂+16⋅X₂ {O(n^2)}
g₉: 20⋅X₂⋅X₂+20⋅X₂ {O(n^2)}
g₁₂: 2⋅X₂+1 {O(n)}
g₁₄: 1 {O(1)}
g₁₆: 1 {O(1)}
Costbounds
Overall costbound: inf {Infinity}
g₀: inf {Infinity}
g₂: inf {Infinity}
g₄: inf {Infinity}
g₆: inf {Infinity}
g₉: inf {Infinity}
g₁₂: inf {Infinity}
g₁₄: inf {Infinity}
g₁₆: inf {Infinity}
Sizebounds
(g₀,f10), X₁: 0 {O(1)}
(g₀,f10), X₂: X₂ {O(n)}
(g₀,f10), X₃: X₃ {O(n)}
(g₀,f10), X₄: X₄ {O(n)}
(g₀,f10), X₅: X₅ {O(n)}
(g₀,f10), X₆: X₆ {O(n)}
(g₀,f10), X₇: X₇ {O(n)}
(g₂,f10), X₁: X₂ {O(n)}
(g₂,f10), X₂: X₂ {O(n)}
(g₂,f10), X₃: X₃ {O(n)}
(g₂,f10), X₄: X₄ {O(n)}
(g₂,f10), X₅: X₅ {O(n)}
(g₂,f10), X₆: X₆ {O(n)}
(g₂,f10), X₇: X₇ {O(n)}
(g₄,f22), X₁: X₂ {O(n)}
(g₄,f22), X₂: 2⋅X₂ {O(n)}
(g₄,f22), X₃: 2⋅X₂ {O(n)}
(g₄,f22), X₄: 2⋅X₂+1 {O(n)}
(g₄,f22), X₅: 2⋅X₂+1 {O(n)}
(g₄,f22), X₆: 2⋅X₂+3 {O(n)}
(g₆,f22), X₁: X₂ {O(n)}
(g₆,f22), X₂: 4⋅X₂ {O(n)}
(g₆,f22), X₃: 4⋅X₂ {O(n)}
(g₆,f22), X₄: 4⋅X₂+2 {O(n)}
(g₆,f22), X₅: 96⋅X₂⋅X₂+120⋅X₂+40 {O(n^2)}
(g₆,f22), X₆: 24⋅X₂⋅X₂+28⋅X₂+8 {O(n^2)}
(g₉,f22), X₁: X₂ {O(n)}
(g₉,f22), X₂: 4⋅X₂ {O(n)}
(g₉,f22), X₃: 4⋅X₂ {O(n)}
(g₉,f22), X₄: 4⋅X₂+2 {O(n)}
(g₉,f22), X₅: 96⋅X₂⋅X₂+118⋅X₂+39 {O(n^2)}
(g₉,f22), X₆: 24⋅X₂⋅X₂+28⋅X₂+8 {O(n^2)}
(g₁₂,f18), X₁: X₂ {O(n)}
(g₁₂,f18), X₂: 2⋅X₂ {O(n)}
(g₁₂,f18), X₃: 2⋅X₂ {O(n)}
(g₁₂,f18), X₄: 2⋅X₂+1 {O(n)}
(g₁₂,f18), X₅: 96⋅X₂⋅X₂+118⋅X₂+39 {O(n^2)}
(g₁₂,f18), X₆: 24⋅X₂⋅X₂+28⋅X₂+8 {O(n^2)}
(g₁₄,f34), X₁: 2⋅X₂ {O(n)}
(g₁₄,f34), X₂: 4⋅X₂ {O(n)}
(g₁₄,f34), X₃: 4⋅X₂ {O(n)}
(g₁₄,f34), X₄: 0 {O(1)}
(g₁₄,f34), X₅: 96⋅X₂⋅X₂+118⋅X₂+2⋅X₅+39 {O(n^2)}
(g₁₄,f34), X₆: 24⋅X₂⋅X₂+2⋅X₆+28⋅X₂+8 {O(n^2)}
(g₁₆,f18), X₁: X₂ {O(n)}
(g₁₆,f18), X₂: 2⋅X₂ {O(n)}
(g₁₆,f18), X₃: 2⋅X₂ {O(n)}
(g₁₆,f18), X₄: 0 {O(1)}
(g₁₆,f18), X₅: 2⋅X₅ {O(n)}
(g₁₆,f18), X₆: 2⋅X₆ {O(n)}
(g₁₆,f18), X₇: 2⋅X₇ {O(n)}
Run probabilistic analysis on SCC: [f34]
Results of Probabilistic Analysis
All Bounds
Timebounds
Overall timebound:36⋅X₂⋅X₂+40⋅X₂+5 {O(n^2)}
g₀: 1 {O(1)}
g₂: X₂ {O(n)}
g₄: X₂+1 {O(n)}
g₆: 16⋅X₂⋅X₂+16⋅X₂ {O(n^2)}
g₉: 20⋅X₂⋅X₂+20⋅X₂ {O(n^2)}
g₁₂: 2⋅X₂+1 {O(n)}
g₁₄: 1 {O(1)}
g₁₆: 1 {O(1)}
Costbounds
Overall costbound: 72⋅X₂⋅X₂+76⋅X₂+5 {O(n^2)}
g₀: 1 {O(1)}
g₂: X₂ {O(n)}
g₄: X₂+1 {O(n)}
g₆: 32⋅X₂⋅X₂+32⋅X₂ {O(n^2)}
g₉: 40⋅X₂⋅X₂+40⋅X₂ {O(n^2)}
g₁₂: 2⋅X₂+1 {O(n)}
g₁₄: 1 {O(1)}
g₁₆: 1 {O(1)}
Sizebounds
(g₀,f10), X₁: 0 {O(1)}
(g₀,f10), X₂: X₂ {O(n)}
(g₀,f10), X₃: X₃ {O(n)}
(g₀,f10), X₄: X₄ {O(n)}
(g₀,f10), X₅: X₅ {O(n)}
(g₀,f10), X₆: X₆ {O(n)}
(g₀,f10), X₇: X₇ {O(n)}
(g₂,f10), X₁: X₂ {O(n)}
(g₂,f10), X₂: X₂ {O(n)}
(g₂,f10), X₃: X₃ {O(n)}
(g₂,f10), X₄: X₄ {O(n)}
(g₂,f10), X₅: X₅ {O(n)}
(g₂,f10), X₆: X₆ {O(n)}
(g₂,f10), X₇: X₇ {O(n)}
(g₄,f22), X₁: X₂ {O(n)}
(g₄,f22), X₂: 2⋅X₂ {O(n)}
(g₄,f22), X₃: 2⋅X₂ {O(n)}
(g₄,f22), X₄: 2⋅X₂+1 {O(n)}
(g₄,f22), X₅: 2⋅X₂+1 {O(n)}
(g₄,f22), X₆: 2⋅X₂+3 {O(n)}
(g₆,f22), X₁: X₂ {O(n)}
(g₆,f22), X₂: 4⋅X₂ {O(n)}
(g₆,f22), X₃: 4⋅X₂ {O(n)}
(g₆,f22), X₄: 4⋅X₂+2 {O(n)}
(g₆,f22), X₅: 96⋅X₂⋅X₂+120⋅X₂+40 {O(n^2)}
(g₆,f22), X₆: 24⋅X₂⋅X₂+28⋅X₂+8 {O(n^2)}
(g₉,f22), X₁: X₂ {O(n)}
(g₉,f22), X₂: 4⋅X₂ {O(n)}
(g₉,f22), X₃: 4⋅X₂ {O(n)}
(g₉,f22), X₄: 4⋅X₂+2 {O(n)}
(g₉,f22), X₅: 96⋅X₂⋅X₂+118⋅X₂+39 {O(n^2)}
(g₉,f22), X₆: 24⋅X₂⋅X₂+28⋅X₂+8 {O(n^2)}
(g₁₂,f18), X₁: X₂ {O(n)}
(g₁₂,f18), X₂: 2⋅X₂ {O(n)}
(g₁₂,f18), X₃: 2⋅X₂ {O(n)}
(g₁₂,f18), X₄: 2⋅X₂+1 {O(n)}
(g₁₂,f18), X₅: 96⋅X₂⋅X₂+118⋅X₂+39 {O(n^2)}
(g₁₂,f18), X₆: 24⋅X₂⋅X₂+28⋅X₂+8 {O(n^2)}
(g₁₄,f34), X₁: 2⋅X₂ {O(n)}
(g₁₄,f34), X₂: 4⋅X₂ {O(n)}
(g₁₄,f34), X₃: 4⋅X₂ {O(n)}
(g₁₄,f34), X₄: 0 {O(1)}
(g₁₄,f34), X₅: 96⋅X₂⋅X₂+118⋅X₂+2⋅X₅+39 {O(n^2)}
(g₁₄,f34), X₆: 24⋅X₂⋅X₂+2⋅X₆+28⋅X₂+8 {O(n^2)}
(g₁₆,f18), X₁: X₂ {O(n)}
(g₁₆,f18), X₂: 2⋅X₂ {O(n)}
(g₁₆,f18), X₃: 2⋅X₂ {O(n)}
(g₁₆,f18), X₄: 0 {O(1)}
(g₁₆,f18), X₅: 2⋅X₅ {O(n)}
(g₁₆,f18), X₆: 2⋅X₆ {O(n)}
(g₁₆,f18), X₇: 2⋅X₇ {O(n)}