Preprocessing
Found invariant 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₀ for location l2
Found invariant 1 ≤ X₁ ∧ 1 ≤ X₀+X₁ ∧ 1+X₀ ≤ X₁ ∧ X₀ ≤ 0 ∧ 0 ≤ X₀ for location l3
Probabilistic Analysis
Probabilistic Program after Preprocessing
Start: l0
Program_Vars: X₀, X₁, X₂
Temp_Vars:
Locations: l0, l1, l2, l3
Transitions:
g₀:l0(X₀,X₁,X₂) → t₁:l1(X₀,X₁,X₂) :|:
g₂:l1(X₀,X₁,X₂) → t₃:l2(X₀,X₁,X₂) :|: 1 ≤ X₀ ∧ X₀ ≤ X₂
g₄:l2(X₀,X₁,X₂) → t₅:l1(3⋅X₀,X₁,2⋅X₂) :|: X₁ ≤ 0 ∧ 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂
g₆:l2(X₀,X₁,X₂) → [1/2]:t₇:l1(X₀-1,X₁,1+X₂) :+: [1/2]:t₈:l1(X₀,X₁,X₂) :|: 1 ≤ X₁ ∧ 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂
g₉:l1(X₀,X₁,X₂) → t₁₀:l3(X₀,X₁,X₂) :|: 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
g₁₁:l3(X₀,X₁,X₂) → t₁₂:l3(X₀,X₁,X₂-1) :|: 1 ≤ X₂ ∧ 1 ≤ X₀+X₁ ∧ 1+X₀ ≤ X₁ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
Show Graph
G
l0
l0
l1
l1
l0->l1
p = 1
t₁ ∈ g₀
l2
l2
l1->l2
p = 1
t₃ ∈ g₂
τ = 1 ≤ X₀ ∧ X₀ ≤ X₂
l3
l3
l1->l3
p = 1
t₁₀ ∈ g₉
τ = 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
l2->l1
p = 1
t₅ ∈ g₄
η (X₀) = 3⋅X₀
η (X₂) = 2⋅X₂
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ X₁ ≤ 0
l2->l1
p = 1/2
t₇ ∈ g₆
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁
l2->l1
p = 1/2
t₈ ∈ g₆
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁
l3->l3
p = 1
t₁₂ ∈ g₁₁
η (X₂) = X₂-1
τ = 1 ≤ X₀+X₁ ∧ 1+X₀ ≤ X₁ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 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}
g₉: 1 {O(1)}
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}
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}
g₉: 1 {O(1)}
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}
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₄,l1), X₁: X₁ {O(n)}
(g₆,l1), X₁: 2⋅X₁ {O(n)}
(g₉,l3), X₀: 0 {O(1)}
(g₉,l3), 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₁₁: inf {Infinity}
g₁₄: 1 {O(1)}
g₁₆: 1 {O(1)}
g₁₈: 1 {O(1)}
g₂₁: 1 {O(1)}
g₂₃: inf {Infinity}
g₂₅: 1 {O(1)}
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}
g₃₉: inf {Infinity}
Sizebounds
(g₀,l1), X₀: X₀ {O(n)}
(g₀,l1), X₁: X₁ {O(n)}
(g₀,l1), X₂: X₂ {O(n)}
(g₉,l3), X₀: 0 {O(1)}
(g₉,l3), X₁: X₁ {O(n)}
(g₉,l3), 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₁₆,l3), X₀: 0 {O(1)}
(g₁₆,l3), X₁: X₁ {O(n)}
(g₁₆,l3), 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₁₁: inf {Infinity}
g₁₄: 1 {O(1)}
g₁₆: 1 {O(1)}
g₁₈: 1 {O(1)}
g₂₁: 2 {O(1)}
g₂₃: inf {Infinity}
g₂₅: 1 {O(1)}
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}
g₃₉: inf {Infinity}
Sizebounds
(g₀,l1), X₀: X₀ {O(n)}
(g₀,l1), X₁: X₁ {O(n)}
(g₀,l1), X₂: X₂ {O(n)}
(g₉,l3), X₀: 0 {O(1)}
(g₉,l3), X₁: X₁ {O(n)}
(g₉,l3), 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₁₆,l3), X₀: 0 {O(1)}
(g₁₆,l3), X₁: X₁ {O(n)}
(g₁₆,l3), X₂: X₂ {O(n)}
(g₁₈,l1_v1), X₀: 3⋅X₀ {O(n)}
(g₁₈,l1_v1), X₁: X₁ {O(n)}
(g₁₈,l1_v1), X₂: 2⋅X₂ {O(n)}
(g₂₁,l1_v2), X₀: 2⋅X₀ {O(n)}
(g₂₁,l1_v2), X₁: 2⋅X₁ {O(n)}
(g₂₁,l1_v2), X₂: 2⋅X₂+1 {O(n)}
(g₂₁,l1_v3), X₀: 2⋅X₀ {O(n)}
(g₂₁,l1_v3), X₁: 2⋅X₁ {O(n)}
(g₂₁,l1_v3), X₂: 2⋅X₂+1 {O(n)}
Run probabilistic analysis on SCC: [l2_v1]
Run classical analysis on SCC: [l1_v1; l2_v4]
TWN: t₃₆: l1_v1→l2_v4
Show Graph
G
l0
l0
l1
l1
l0->l1
t₁
l2_v1
l2_v1
l1->l2_v1
t₁₃
τ = 1 ≤ X₀ ∧ X₀ ≤ X₂
l3
l3
l1->l3
t₁₀
τ = 1 ≤ X₁ ∧ X₀ ≤ 0 ∧ 0 ≤ X₀
l1->l3
t₁₅
τ = 1 ≤ X₁ ∧ X₀ ≤ 0 ∧ 0 ≤ X₀
l1_v1
l1_v1
l2_v4
l2_v4
l1_v1->l2_v4
t₃₆
τ = 1 ≤ X₂ ∧ 3 ≤ X₀ ∧ 0 ≤ X₀ ∧ 2⋅X₀ ≤ 3⋅X₂ ∧ X₁ ≤ 0 ∧ 1 ≤ X₀ ∧ X₀ ≤ X₂
l1_v2
l1_v2
l2_v2
l2_v2
l1_v2->l2_v2
t₂₂
τ = 1 ≤ X₁ ∧ 1 ≤ X₂ ∧ 2+X₀ ≤ X₂ ∧ 0 ≤ X₀ ∧ 2⋅X₀ ≤ 3⋅X₂ ∧ 1 ≤ X₀ ∧ X₀ ≤ X₂
l1_v2->l3
t₂₄
τ = 1 ≤ X₂ ∧ 2+X₀ ≤ X₂ ∧ X₀ ≤ X₂ ∧ 2⋅X₀ ≤ 3⋅X₂ ∧ 1 ≤ X₁ ∧ X₀ ≤ 0 ∧ 0 ≤ X₀
l1_v3
l1_v3
l2_v3
l2_v3
l1_v3->l2_v3
t₃₁
τ = 1 ≤ X₁ ∧ 1 ≤ X₂ ∧ 0 ≤ X₀ ∧ 2⋅X₀ ≤ 3⋅X₂ ∧ 1 ≤ X₀ ∧ X₀ ≤ X₂
l1_v4
l1_v4
l1_v4->l2_v2
t₂₉
τ = 1 ≤ X₁ ∧ 1 ≤ X₂ ∧ 2+X₀ ≤ X₂ ∧ 0 ≤ X₀ ∧ 2⋅X₀ ≤ 3⋅X₂ ∧ 1 ≤ X₀ ∧ X₀ ≤ X₂
l2_v1->l1_v1
t₁₇
η (X₀) = 3⋅X₀
η (X₂) = 2⋅X₂
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ X₁ ≤ 0
l2_v1->l1_v2
t₁₉
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁
l2_v1->l1_v3
t₂₀
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁
l2_v2->l1_v2
t₂₆
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ 2+X₀ ≤ X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁
l2_v2->l1_v4
t₂₇
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ 2+X₀ ≤ X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁
l2_v3->l1_v2
t₃₃
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁
l2_v3->l1_v3
t₃₄
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁
l2_v4->l1_v1
t₃₈
η (X₀) = 3⋅X₀
η (X₂) = 2⋅X₂
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ 3 ≤ X₀ ∧ X₀ ≤ X₂ ∧ X₁ ≤ 0
l3->l3
t₁₂
η (X₂) = X₂-1
τ = 1 ≤ X₀+X₁ ∧ 1+X₀ ≤ X₁ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 1 ≤ X₂
cycle: [t₃₆: l1_v1→l2_v4; t₃₈: l2_v4→l1_v1]
loop: (1 ≤ X₀ ∧ X₀ ≤ X₂ ∧ X₁ ≤ 0,(X₀,X₁,X₂) -> (3⋅X₀,X₁,2⋅X₂)
order: [X₀; X₁; X₂]
closed-form:X₀: X₀ * 3^n
X₁: X₁
X₂: X₂ * 2^n
Termination: true
Formula:
0 ≤ 1 ∧ 1 ≤ 0 ∧ 1+X₀ ≤ 0 ∧ 1+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 1 ∧ 1 ≤ 0 ∧ 1+X₀ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
∨ 0 ≤ 1 ∧ 1 ≤ 0 ∧ 1+X₁ ≤ 0 ∧ 1 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 1 ∧ 1 ≤ 0 ∧ 1+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₂ ∧ X₂ ≤ 0
∨ 0 ≤ 1 ∧ 1 ≤ 0 ∧ 1 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
∨ 0 ≤ 1 ∧ 1 ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0 ∧ 0 ≤ X₂ ∧ X₂ ≤ 0
∨ 1 ≤ 0 ∧ 1+X₀ ≤ 0 ∧ 1+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 1 ≤ 0 ∧ 1+X₀ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
∨ 1 ≤ 0 ∧ 1+X₁ ≤ 0 ∧ 1 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 1 ≤ 0 ∧ 1+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₂ ∧ X₂ ≤ 0
∨ 1 ≤ 0 ∧ 1 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
∨ 1 ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0 ∧ 0 ≤ X₂ ∧ X₂ ≤ 0
∨ 1 ≤ X₀ ∧ 1+X₀ ≤ 0 ∧ 1+X₁ ≤ 0
∨ 1 ≤ X₀ ∧ 1+X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
∨ 1 ≤ X₀ ∧ 1+X₁ ≤ 0 ∧ 1 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 1 ≤ X₀ ∧ 1+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₂ ∧ X₂ ≤ 0
∨ 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
∨ 1 ≤ X₀ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0 ∧ 0 ≤ X₂ ∧ X₂ ≤ 0
Stabilization-Threshold for: X₀ ≤ X₂
alphas_abs: 1+X₂
M: 0
N: 1
Bound: 2⋅X₂+4 {O(n)}
TWN - Lifting for [36: l1_v1->l2_v4; 38: l2_v4->l1_v1] of 2⋅X₂+8 {O(n)}
relevant size-bounds w.r.t. t₁₇: l2_v1→l1_v1:
X₂: 2⋅X₂ {O(n)}
Runtime-bound of t₁₇: 1 {O(1)}
Results in: 4⋅X₂+8 {O(n)}
Classical Approximation after Lifting Classical Results
All Bounds
Timebounds
Overall timebound:inf {Infinity}
g₀: 1 {O(1)}
g₉: 1 {O(1)}
g₁₁: inf {Infinity}
g₁₄: 1 {O(1)}
g₁₆: 1 {O(1)}
g₁₈: 1 {O(1)}
g₂₁: 2 {O(1)}
g₂₃: inf {Infinity}
g₂₅: 1 {O(1)}
g₂₈: inf {Infinity}
g₃₀: inf {Infinity}
g₃₂: inf {Infinity}
g₃₅: inf {Infinity}
g₃₇: 4⋅X₂+8 {O(n)}
g₃₉: 4⋅X₂+8 {O(n)}
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}
g₃₉: inf {Infinity}
Sizebounds
(g₀,l1), X₀: X₀ {O(n)}
(g₀,l1), X₁: X₁ {O(n)}
(g₀,l1), X₂: X₂ {O(n)}
(g₉,l3), X₀: 0 {O(1)}
(g₉,l3), X₁: X₁ {O(n)}
(g₉,l3), 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₁₆,l3), X₀: 0 {O(1)}
(g₁₆,l3), X₁: X₁ {O(n)}
(g₁₆,l3), X₂: X₂ {O(n)}
(g₁₈,l1_v1), X₀: 3⋅X₀ {O(n)}
(g₁₈,l1_v1), X₁: X₁ {O(n)}
(g₁₈,l1_v1), X₂: 2⋅X₂ {O(n)}
(g₂₁,l1_v2), X₀: X₀ {O(n)}
(g₂₁,l1_v2), X₁: X₁ {O(n)}
(g₂₁,l1_v2), X₂: 2⋅X₂+1 {O(n)}
(g₂₁,l1_v3), X₀: X₀ {O(n)}
(g₂₁,l1_v3), X₁: X₁ {O(n)}
(g₂₁,l1_v3), X₂: X₂ {O(n)}
(g₃₇,l2_v4), X₀: 3⋅3^(4⋅X₂+8)⋅X₀ {O(EXP)}
(g₃₇,l2_v4), X₁: X₁ {O(n)}
(g₃₇,l2_v4), X₂: 2⋅2^(4⋅X₂+8)⋅X₂ {O(EXP)}
(g₃₉,l1_v1), X₀: 3⋅3^(4⋅X₂+8)⋅X₀ {O(EXP)}
(g₃₉,l1_v1), X₁: X₁ {O(n)}
(g₃₉,l1_v1), X₂: 2⋅2^(4⋅X₂+8)⋅X₂ {O(EXP)}
Run probabilistic analysis on SCC: [l1_v1; l2_v4]
Run classical analysis on SCC: [l1_v3; l2_v3]
Classical Approximation after Lifting Classical Results
All Bounds
Timebounds
Overall timebound:inf {Infinity}
g₀: 1 {O(1)}
g₉: 1 {O(1)}
g₁₁: inf {Infinity}
g₁₄: 1 {O(1)}
g₁₆: 1 {O(1)}
g₁₈: 1 {O(1)}
g₂₁: 2 {O(1)}
g₂₃: inf {Infinity}
g₂₅: 1 {O(1)}
g₂₈: inf {Infinity}
g₃₀: inf {Infinity}
g₃₂: inf {Infinity}
g₃₅: inf {Infinity}
g₃₇: 4⋅X₂+8 {O(n)}
g₃₉: 4⋅X₂+8 {O(n)}
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}
g₃₉: inf {Infinity}
Sizebounds
(g₀,l1), X₀: X₀ {O(n)}
(g₀,l1), X₁: X₁ {O(n)}
(g₀,l1), X₂: X₂ {O(n)}
(g₉,l3), X₀: 0 {O(1)}
(g₉,l3), X₁: X₁ {O(n)}
(g₉,l3), 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₁₆,l3), X₀: 0 {O(1)}
(g₁₆,l3), X₁: X₁ {O(n)}
(g₁₆,l3), X₂: X₂ {O(n)}
(g₁₈,l1_v1), X₀: 3⋅X₀ {O(n)}
(g₁₈,l1_v1), X₁: X₁ {O(n)}
(g₁₈,l1_v1), X₂: 2⋅X₂ {O(n)}
(g₂₁,l1_v2), X₀: X₀ {O(n)}
(g₂₁,l1_v2), X₁: X₁ {O(n)}
(g₂₁,l1_v2), X₂: 2⋅X₂+1 {O(n)}
(g₂₁,l1_v3), X₀: X₀ {O(n)}
(g₂₁,l1_v3), X₁: X₁ {O(n)}
(g₂₁,l1_v3), 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_v2), X₀: 2⋅X₀ {O(n)}
(g₃₅,l1_v2), X₁: 2⋅X₁ {O(n)}
(g₃₅,l1_v2), X₂: 2⋅X₂+1 {O(n)}
(g₃₅,l1_v3), X₀: 2⋅X₀ {O(n)}
(g₃₅,l1_v3), X₁: 2⋅X₁ {O(n)}
(g₃₅,l1_v3), X₂: 2⋅X₂+1 {O(n)}
(g₃₇,l2_v4), X₀: 3⋅3^(4⋅X₂+8)⋅X₀ {O(EXP)}
(g₃₇,l2_v4), X₁: X₁ {O(n)}
(g₃₇,l2_v4), X₂: 2⋅2^(4⋅X₂+8)⋅X₂ {O(EXP)}
(g₃₉,l1_v1), X₀: 3⋅3^(4⋅X₂+8)⋅X₀ {O(EXP)}
(g₃₉,l1_v1), X₁: X₁ {O(n)}
(g₃₉,l1_v1), X₂: 2⋅2^(4⋅X₂+8)⋅X₂ {O(EXP)}
Run probabilistic analysis on SCC: [l1_v3; l2_v3]
Plrf for transition g₃₂:l1_v3(X₀,X₁,X₂) → t₃₁:l2_v3(X₀,X₁,X₂) :|: 1 ≤ X₀ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁ ∧ 1 ≤ X₂ ∧ 0 ≤ X₀ ∧ 2⋅X₀ ≤ 3⋅X₂:
new bound:
X₁+1 {O(n)}
PLRF:
• l1_v2: X₁-1
• l1_v3: 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₁₄
τ = 1 ≤ X₀ ∧ X₀ ≤ X₂
l3
l3
l1->l3
p = 1
t₁₀ ∈ g₉
τ = 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
l1->l3
p = 1
t₁₅ ∈ g₁₆
τ = 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
l1_v1
l1_v1
l2_v4
l2_v4
l1_v1->l2_v4
p = 1
t₃₆ ∈ g₃₇
τ = 1 ≤ X₂ ∧ 3 ≤ X₀ ∧ 0 ≤ X₀ ∧ 2⋅X₀ ≤ 3⋅X₂ ∧ X₁ ≤ 0 ∧ 1 ≤ X₀ ∧ X₀ ≤ X₂
l1_v2
l1_v2
l2_v2
l2_v2
l1_v2->l2_v2
p = 1
t₂₂ ∈ g₂₃
τ = 1 ≤ X₁ ∧ 1 ≤ X₂ ∧ 2+X₀ ≤ X₂ ∧ 0 ≤ X₀ ∧ 2⋅X₀ ≤ 3⋅X₂ ∧ 1 ≤ X₀ ∧ X₀ ≤ X₂
l1_v2->l3
p = 1
t₂₄ ∈ g₂₅
τ = 1 ≤ X₂ ∧ 2+X₀ ≤ X₂ ∧ X₀ ≤ X₂ ∧ 2⋅X₀ ≤ 3⋅X₂ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
l1_v3
l1_v3
l2_v3
l2_v3
l1_v3->l2_v3
p = 1
t₃₁ ∈ g₃₂
τ = 1 ≤ X₁ ∧ 1 ≤ X₂ ∧ 0 ≤ X₀ ∧ 2⋅X₀ ≤ 3⋅X₂ ∧ 1 ≤ X₀ ∧ X₀ ≤ X₂
l1_v4
l1_v4
l1_v4->l2_v2
p = 1
t₂₉ ∈ g₃₀
τ = 1 ≤ X₁ ∧ 1 ≤ X₂ ∧ 2+X₀ ≤ X₂ ∧ 0 ≤ X₀ ∧ 2⋅X₀ ≤ 3⋅X₂ ∧ 1 ≤ X₀ ∧ X₀ ≤ X₂
l2_v1->l1_v1
p = 1
t₁₇ ∈ g₁₈
η (X₀) = 3⋅X₀
η (X₂) = 2⋅X₂
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ X₁ ≤ 0
l2_v1->l1_v2
p = 1/2
t₁₉ ∈ g₂₁
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁
l2_v1->l1_v3
p = 1/2
t₂₀ ∈ g₂₁
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁
l2_v2->l1_v2
p = 1/2
t₂₆ ∈ g₂₈
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ 2+X₀ ≤ X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁
l2_v2->l1_v4
p = 1/2
t₂₇ ∈ g₂₈
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ 2+X₀ ≤ X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁
l2_v3->l1_v2
p = 1/2
t₃₃ ∈ g₃₅
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁
l2_v3->l1_v3
p = 1/2
t₃₄ ∈ g₃₅
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁
l2_v4->l1_v1
p = 1
t₃₈ ∈ g₃₉
η (X₀) = 3⋅X₀
η (X₂) = 2⋅X₂
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ 3 ≤ X₀ ∧ X₀ ≤ X₂ ∧ X₁ ≤ 0
l3->l3
p = 1
t₁₂ ∈ g₁₁
η (X₂) = X₂-1
τ = 1 ≤ X₀+X₁ ∧ 1+X₀ ≤ X₁ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 1 ≤ X₂
Use expected size bounds for entry point (g₂₁:l2_v1→[t₁₉:1/2:l1_v2; t₂₀:1/2:l1_v3],l1_v3)
Use classical time bound for entry point (g₂₁:l2_v1→[t₁₉:1/2:l1_v2; t₂₀:1/2:l1_v3],l1_v3)
Plrf for transition g₃₅:l2_v3(X₀,X₁,X₂) → [1/2]:t₃₃:l1_v2(X₀-1,X₁,1+X₂) :+: [1/2]:t₃₄:l1_v3(X₀,X₁,X₂) :|: 1 ≤ X₁ ∧ 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂:
new bound:
2⋅X₂ {O(n)}
PLRF:
• l1_v2: 0
• l1_v3: 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₁₄
τ = 1 ≤ X₀ ∧ X₀ ≤ X₂
l3
l3
l1->l3
p = 1
t₁₀ ∈ g₉
τ = 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
l1->l3
p = 1
t₁₅ ∈ g₁₆
τ = 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
l1_v1
l1_v1
l2_v4
l2_v4
l1_v1->l2_v4
p = 1
t₃₆ ∈ g₃₇
τ = 1 ≤ X₂ ∧ 3 ≤ X₀ ∧ 0 ≤ X₀ ∧ 2⋅X₀ ≤ 3⋅X₂ ∧ X₁ ≤ 0 ∧ 1 ≤ X₀ ∧ X₀ ≤ X₂
l1_v2
l1_v2
l2_v2
l2_v2
l1_v2->l2_v2
p = 1
t₂₂ ∈ g₂₃
τ = 1 ≤ X₁ ∧ 1 ≤ X₂ ∧ 2+X₀ ≤ X₂ ∧ 0 ≤ X₀ ∧ 2⋅X₀ ≤ 3⋅X₂ ∧ 1 ≤ X₀ ∧ X₀ ≤ X₂
l1_v2->l3
p = 1
t₂₄ ∈ g₂₅
τ = 1 ≤ X₂ ∧ 2+X₀ ≤ X₂ ∧ X₀ ≤ X₂ ∧ 2⋅X₀ ≤ 3⋅X₂ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
l1_v3
l1_v3
l2_v3
l2_v3
l1_v3->l2_v3
p = 1
t₃₁ ∈ g₃₂
τ = 1 ≤ X₁ ∧ 1 ≤ X₂ ∧ 0 ≤ X₀ ∧ 2⋅X₀ ≤ 3⋅X₂ ∧ 1 ≤ X₀ ∧ X₀ ≤ X₂
l1_v4
l1_v4
l1_v4->l2_v2
p = 1
t₂₉ ∈ g₃₀
τ = 1 ≤ X₁ ∧ 1 ≤ X₂ ∧ 2+X₀ ≤ X₂ ∧ 0 ≤ X₀ ∧ 2⋅X₀ ≤ 3⋅X₂ ∧ 1 ≤ X₀ ∧ X₀ ≤ X₂
l2_v1->l1_v1
p = 1
t₁₇ ∈ g₁₈
η (X₀) = 3⋅X₀
η (X₂) = 2⋅X₂
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ X₁ ≤ 0
l2_v1->l1_v2
p = 1/2
t₁₉ ∈ g₂₁
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁
l2_v1->l1_v3
p = 1/2
t₂₀ ∈ g₂₁
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁
l2_v2->l1_v2
p = 1/2
t₂₆ ∈ g₂₈
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ 2+X₀ ≤ X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁
l2_v2->l1_v4
p = 1/2
t₂₇ ∈ g₂₈
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ 2+X₀ ≤ X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁
l2_v3->l1_v2
p = 1/2
t₃₃ ∈ g₃₅
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁
l2_v3->l1_v3
p = 1/2
t₃₄ ∈ g₃₅
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁
l2_v4->l1_v1
p = 1
t₃₈ ∈ g₃₉
η (X₀) = 3⋅X₀
η (X₂) = 2⋅X₂
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ 3 ≤ X₀ ∧ X₀ ≤ X₂ ∧ X₁ ≤ 0
l3->l3
p = 1
t₁₂ ∈ g₁₁
η (X₂) = X₂-1
τ = 1 ≤ X₀+X₁ ∧ 1+X₀ ≤ X₁ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 1 ≤ X₂
Use expected size bounds for entry point (g₂₁:l2_v1→[t₁₉:1/2:l1_v2; t₂₀:1/2:l1_v3],l1_v3)
Use classical time bound for entry point (g₂₁:l2_v1→[t₁₉:1/2:l1_v2; t₂₀:1/2:l1_v3],l1_v3)
Run classical analysis on SCC: [l1_v2; l1_v4; l2_v2]
MPRF for transition t₂₂: l1_v2(X₀,X₁,X₂) → l2_v2(X₀,X₁,X₂) :|: 1 ≤ X₁ ∧ 1 ≤ X₂ ∧ 2+X₀ ≤ X₂ ∧ 0 ≤ X₀ ∧ 2⋅X₀ ≤ 3⋅X₂ ∧ 1 ≤ X₀ ∧ X₀ ≤ X₂ of depth 1:
new bound:
2⋅X₀+2 {O(n)}
MPRF:
• l1_v2: [1+X₀]
• l1_v4: [X₀]
• l2_v2: [X₀]
Show Graph
G
l0
l0
l1
l1
l0->l1
t₁
l2_v1
l2_v1
l1->l2_v1
t₁₃
τ = 1 ≤ X₀ ∧ X₀ ≤ X₂
l3
l3
l1->l3
t₁₀
τ = 1 ≤ X₁ ∧ X₀ ≤ 0 ∧ 0 ≤ X₀
l1->l3
t₁₅
τ = 1 ≤ X₁ ∧ X₀ ≤ 0 ∧ 0 ≤ X₀
l1_v1
l1_v1
l2_v4
l2_v4
l1_v1->l2_v4
t₃₆
τ = 1 ≤ X₂ ∧ 3 ≤ X₀ ∧ 0 ≤ X₀ ∧ 2⋅X₀ ≤ 3⋅X₂ ∧ X₁ ≤ 0 ∧ 1 ≤ X₀ ∧ X₀ ≤ X₂
l1_v2
l1_v2
l2_v2
l2_v2
l1_v2->l2_v2
t₂₂
τ = 1 ≤ X₁ ∧ 1 ≤ X₂ ∧ 2+X₀ ≤ X₂ ∧ 0 ≤ X₀ ∧ 2⋅X₀ ≤ 3⋅X₂ ∧ 1 ≤ X₀ ∧ X₀ ≤ X₂
l1_v2->l3
t₂₄
τ = 1 ≤ X₂ ∧ 2+X₀ ≤ X₂ ∧ X₀ ≤ X₂ ∧ 2⋅X₀ ≤ 3⋅X₂ ∧ 1 ≤ X₁ ∧ X₀ ≤ 0 ∧ 0 ≤ X₀
l1_v3
l1_v3
l2_v3
l2_v3
l1_v3->l2_v3
t₃₁
τ = 1 ≤ X₁ ∧ 1 ≤ X₂ ∧ 0 ≤ X₀ ∧ 2⋅X₀ ≤ 3⋅X₂ ∧ 1 ≤ X₀ ∧ X₀ ≤ X₂
l1_v4
l1_v4
l1_v4->l2_v2
t₂₉
τ = 1 ≤ X₁ ∧ 1 ≤ X₂ ∧ 2+X₀ ≤ X₂ ∧ 0 ≤ X₀ ∧ 2⋅X₀ ≤ 3⋅X₂ ∧ 1 ≤ X₀ ∧ X₀ ≤ X₂
l2_v1->l1_v1
t₁₇
η (X₀) = 3⋅X₀
η (X₂) = 2⋅X₂
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ X₁ ≤ 0
l2_v1->l1_v2
t₁₉
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁
l2_v1->l1_v3
t₂₀
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁
l2_v2->l1_v2
t₂₆
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ 2+X₀ ≤ X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁
l2_v2->l1_v4
t₂₇
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ 2+X₀ ≤ X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁
l2_v3->l1_v2
t₃₃
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁
l2_v3->l1_v3
t₃₄
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁
l2_v4->l1_v1
t₃₈
η (X₀) = 3⋅X₀
η (X₂) = 2⋅X₂
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ 3 ≤ X₀ ∧ X₀ ≤ X₂ ∧ X₁ ≤ 0
l3->l3
t₁₂
η (X₂) = X₂-1
τ = 1 ≤ X₀+X₁ ∧ 1+X₀ ≤ X₁ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 1 ≤ X₂
MPRF for transition t₂₆: l2_v2(X₀,X₁,X₂) → l1_v2(X₀-1,X₁,1+X₂) :|: 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ 2+X₀ ≤ X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁ of depth 1:
new bound:
2⋅X₀ {O(n)}
MPRF:
• l1_v2: [X₀]
• l1_v4: [X₀]
• l2_v2: [X₀]
Show Graph
G
l0
l0
l1
l1
l0->l1
t₁
l2_v1
l2_v1
l1->l2_v1
t₁₃
τ = 1 ≤ X₀ ∧ X₀ ≤ X₂
l3
l3
l1->l3
t₁₀
τ = 1 ≤ X₁ ∧ X₀ ≤ 0 ∧ 0 ≤ X₀
l1->l3
t₁₅
τ = 1 ≤ X₁ ∧ X₀ ≤ 0 ∧ 0 ≤ X₀
l1_v1
l1_v1
l2_v4
l2_v4
l1_v1->l2_v4
t₃₆
τ = 1 ≤ X₂ ∧ 3 ≤ X₀ ∧ 0 ≤ X₀ ∧ 2⋅X₀ ≤ 3⋅X₂ ∧ X₁ ≤ 0 ∧ 1 ≤ X₀ ∧ X₀ ≤ X₂
l1_v2
l1_v2
l2_v2
l2_v2
l1_v2->l2_v2
t₂₂
τ = 1 ≤ X₁ ∧ 1 ≤ X₂ ∧ 2+X₀ ≤ X₂ ∧ 0 ≤ X₀ ∧ 2⋅X₀ ≤ 3⋅X₂ ∧ 1 ≤ X₀ ∧ X₀ ≤ X₂
l1_v2->l3
t₂₄
τ = 1 ≤ X₂ ∧ 2+X₀ ≤ X₂ ∧ X₀ ≤ X₂ ∧ 2⋅X₀ ≤ 3⋅X₂ ∧ 1 ≤ X₁ ∧ X₀ ≤ 0 ∧ 0 ≤ X₀
l1_v3
l1_v3
l2_v3
l2_v3
l1_v3->l2_v3
t₃₁
τ = 1 ≤ X₁ ∧ 1 ≤ X₂ ∧ 0 ≤ X₀ ∧ 2⋅X₀ ≤ 3⋅X₂ ∧ 1 ≤ X₀ ∧ X₀ ≤ X₂
l1_v4
l1_v4
l1_v4->l2_v2
t₂₉
τ = 1 ≤ X₁ ∧ 1 ≤ X₂ ∧ 2+X₀ ≤ X₂ ∧ 0 ≤ X₀ ∧ 2⋅X₀ ≤ 3⋅X₂ ∧ 1 ≤ X₀ ∧ X₀ ≤ X₂
l2_v1->l1_v1
t₁₇
η (X₀) = 3⋅X₀
η (X₂) = 2⋅X₂
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ X₁ ≤ 0
l2_v1->l1_v2
t₁₉
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁
l2_v1->l1_v3
t₂₀
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁
l2_v2->l1_v2
t₂₆
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ 2+X₀ ≤ X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁
l2_v2->l1_v4
t₂₇
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ 2+X₀ ≤ X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁
l2_v3->l1_v2
t₃₃
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁
l2_v3->l1_v3
t₃₄
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁
l2_v4->l1_v1
t₃₈
η (X₀) = 3⋅X₀
η (X₂) = 2⋅X₂
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ 3 ≤ X₀ ∧ X₀ ≤ X₂ ∧ X₁ ≤ 0
l3->l3
t₁₂
η (X₂) = X₂-1
τ = 1 ≤ X₀+X₁ ∧ 1+X₀ ≤ X₁ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 1 ≤ X₂
Classical Approximation after Lifting Classical Results
All Bounds
Timebounds
Overall timebound:inf {Infinity}
g₀: 1 {O(1)}
g₉: 1 {O(1)}
g₁₁: inf {Infinity}
g₁₄: 1 {O(1)}
g₁₆: 1 {O(1)}
g₁₈: 1 {O(1)}
g₂₁: 2 {O(1)}
g₂₃: 2⋅X₀+2 {O(n)}
g₂₅: 1 {O(1)}
g₂₈: inf {Infinity}
g₃₀: inf {Infinity}
g₃₂: X₁+1 {O(n)}
g₃₅: 2⋅X₂ {O(n)}
g₃₇: 4⋅X₂+8 {O(n)}
g₃₉: 4⋅X₂+8 {O(n)}
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}
g₃₉: inf {Infinity}
Sizebounds
(g₀,l1), X₀: X₀ {O(n)}
(g₀,l1), X₁: X₁ {O(n)}
(g₀,l1), X₂: X₂ {O(n)}
(g₉,l3), X₀: 0 {O(1)}
(g₉,l3), X₁: X₁ {O(n)}
(g₉,l3), 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₁₆,l3), X₀: 0 {O(1)}
(g₁₆,l3), X₁: X₁ {O(n)}
(g₁₆,l3), X₂: X₂ {O(n)}
(g₁₈,l1_v1), X₀: 3⋅X₀ {O(n)}
(g₁₈,l1_v1), X₁: X₁ {O(n)}
(g₁₈,l1_v1), X₂: 2⋅X₂ {O(n)}
(g₂₁,l1_v2), X₀: X₀ {O(n)}
(g₂₁,l1_v2), X₁: X₁ {O(n)}
(g₂₁,l1_v2), X₂: 2⋅X₂+1 {O(n)}
(g₂₁,l1_v3), X₀: X₀ {O(n)}
(g₂₁,l1_v3), X₁: X₁ {O(n)}
(g₂₁,l1_v3), X₂: X₂ {O(n)}
(g₂₃,l2_v2), X₀: 2⋅X₀ {O(n)}
(g₂₃,l2_v2), X₁: 2⋅X₁ {O(n)}
(g₂₃,l2_v2), X₂: 2⋅X₀+2⋅X₂+2 {O(n)}
(g₂₅,l3), X₀: 0 {O(1)}
(g₂₅,l3), X₁: 4⋅X₁ {O(n)}
(g₂₅,l3), X₂: 2⋅X₀+4⋅X₂+4 {O(n)}
(g₂₈,l1_v2), X₀: 4⋅X₀ {O(n)}
(g₂₈,l1_v2), X₁: 4⋅X₁ {O(n)}
(g₂₈,l1_v2), X₂: 4⋅X₀+4⋅X₂+4 {O(n)}
(g₂₈,l1_v4), X₀: 4⋅X₀ {O(n)}
(g₂₈,l1_v4), X₁: 4⋅X₁ {O(n)}
(g₂₈,l1_v4), X₂: 4⋅X₀+4⋅X₂+4 {O(n)}
(g₃₀,l2_v2), X₀: 2⋅X₀ {O(n)}
(g₃₀,l2_v2), X₁: 2⋅X₁ {O(n)}
(g₃₀,l2_v2), X₂: 2⋅X₀+2⋅X₂+2 {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_v2), X₀: X₀ {O(n)}
(g₃₅,l1_v2), X₁: X₁ {O(n)}
(g₃₅,l1_v2), X₂: 2⋅X₂ {O(n)}
(g₃₅,l1_v3), X₀: X₀ {O(n)}
(g₃₅,l1_v3), X₁: X₁ {O(n)}
(g₃₅,l1_v3), X₂: 2⋅X₂ {O(n)}
(g₃₇,l2_v4), X₀: 3⋅3^(4⋅X₂+8)⋅X₀ {O(EXP)}
(g₃₇,l2_v4), X₁: X₁ {O(n)}
(g₃₇,l2_v4), X₂: 2⋅2^(4⋅X₂+8)⋅X₂ {O(EXP)}
(g₃₉,l1_v1), X₀: 3⋅3^(4⋅X₂+8)⋅X₀ {O(EXP)}
(g₃₉,l1_v1), X₁: X₁ {O(n)}
(g₃₉,l1_v1), X₂: 2⋅2^(4⋅X₂+8)⋅X₂ {O(EXP)}
Run probabilistic analysis on SCC: [l1_v2; l1_v4; l2_v2]
Plrf for transition g₂₈:l2_v2(X₀,X₁,X₂) → [1/2]:t₂₆:l1_v2(X₀-1,X₁,1+X₂) :+: [1/2]:t₂₇:l1_v4(X₀,X₁,X₂) :|: 1 ≤ X₁ ∧ 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ 2+X₀ ≤ X₂ ∧ X₀ ≤ X₂:
new bound:
4⋅X₀ {O(n)}
PLRF:
• l1_v2: 2⋅X₀
• l1_v4: 2⋅X₀
• l2_v2: 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₁₄
τ = 1 ≤ X₀ ∧ X₀ ≤ X₂
l3
l3
l1->l3
p = 1
t₁₀ ∈ g₉
τ = 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
l1->l3
p = 1
t₁₅ ∈ g₁₆
τ = 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
l1_v1
l1_v1
l2_v4
l2_v4
l1_v1->l2_v4
p = 1
t₃₆ ∈ g₃₇
τ = 1 ≤ X₂ ∧ 3 ≤ X₀ ∧ 0 ≤ X₀ ∧ 2⋅X₀ ≤ 3⋅X₂ ∧ X₁ ≤ 0 ∧ 1 ≤ X₀ ∧ X₀ ≤ X₂
l1_v2
l1_v2
l2_v2
l2_v2
l1_v2->l2_v2
p = 1
t₂₂ ∈ g₂₃
τ = 1 ≤ X₁ ∧ 1 ≤ X₂ ∧ 2+X₀ ≤ X₂ ∧ 0 ≤ X₀ ∧ 2⋅X₀ ≤ 3⋅X₂ ∧ 1 ≤ X₀ ∧ X₀ ≤ X₂
l1_v2->l3
p = 1
t₂₄ ∈ g₂₅
τ = 1 ≤ X₂ ∧ 2+X₀ ≤ X₂ ∧ X₀ ≤ X₂ ∧ 2⋅X₀ ≤ 3⋅X₂ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
l1_v3
l1_v3
l2_v3
l2_v3
l1_v3->l2_v3
p = 1
t₃₁ ∈ g₃₂
τ = 1 ≤ X₁ ∧ 1 ≤ X₂ ∧ 0 ≤ X₀ ∧ 2⋅X₀ ≤ 3⋅X₂ ∧ 1 ≤ X₀ ∧ X₀ ≤ X₂
l1_v4
l1_v4
l1_v4->l2_v2
p = 1
t₂₉ ∈ g₃₀
τ = 1 ≤ X₁ ∧ 1 ≤ X₂ ∧ 2+X₀ ≤ X₂ ∧ 0 ≤ X₀ ∧ 2⋅X₀ ≤ 3⋅X₂ ∧ 1 ≤ X₀ ∧ X₀ ≤ X₂
l2_v1->l1_v1
p = 1
t₁₇ ∈ g₁₈
η (X₀) = 3⋅X₀
η (X₂) = 2⋅X₂
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ X₁ ≤ 0
l2_v1->l1_v2
p = 1/2
t₁₉ ∈ g₂₁
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁
l2_v1->l1_v3
p = 1/2
t₂₀ ∈ g₂₁
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁
l2_v2->l1_v2
p = 1/2
t₂₆ ∈ g₂₈
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ 2+X₀ ≤ X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁
l2_v2->l1_v4
p = 1/2
t₂₇ ∈ g₂₈
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ 2+X₀ ≤ X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁
l2_v3->l1_v2
p = 1/2
t₃₃ ∈ g₃₅
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁
l2_v3->l1_v3
p = 1/2
t₃₄ ∈ g₃₅
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁
l2_v4->l1_v1
p = 1
t₃₈ ∈ g₃₉
η (X₀) = 3⋅X₀
η (X₂) = 2⋅X₂
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ 3 ≤ X₀ ∧ X₀ ≤ X₂ ∧ X₁ ≤ 0
l3->l3
p = 1
t₁₂ ∈ g₁₁
η (X₂) = X₂-1
τ = 1 ≤ X₀+X₁ ∧ 1+X₀ ≤ X₁ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 1 ≤ X₂
Use expected size bounds for entry point (g₂₁:l2_v1→[t₁₉:1/2:l1_v2; t₂₀:1/2:l1_v3],l1_v2)
Use classical time bound for entry point (g₂₁:l2_v1→[t₁₉:1/2:l1_v2; t₂₀:1/2:l1_v3],l1_v2)
Use expected size bounds for entry point (g₃₅:l2_v3→[t₃₃:1/2:l1_v2; t₃₄:1/2:l1_v3],l1_v2)
Use classical time bound for entry point (g₃₅:l2_v3→[t₃₃:1/2:l1_v2; t₃₄:1/2:l1_v3],l1_v2)
Plrf for transition g₃₀:l1_v4(X₀,X₁,X₂) → t₂₉:l2_v2(X₀,X₁,X₂) :|: 1 ≤ X₀ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁ ∧ 1 ≤ X₂ ∧ 2+X₀ ≤ X₂ ∧ 0 ≤ X₀ ∧ 2⋅X₀ ≤ 3⋅X₂:
new bound:
2⋅X₀ {O(n)}
PLRF:
• l1_v2: X₀
• l1_v4: 1+X₀
• l2_v2: 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₁₄
τ = 1 ≤ X₀ ∧ X₀ ≤ X₂
l3
l3
l1->l3
p = 1
t₁₀ ∈ g₉
τ = 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
l1->l3
p = 1
t₁₅ ∈ g₁₆
τ = 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
l1_v1
l1_v1
l2_v4
l2_v4
l1_v1->l2_v4
p = 1
t₃₆ ∈ g₃₇
τ = 1 ≤ X₂ ∧ 3 ≤ X₀ ∧ 0 ≤ X₀ ∧ 2⋅X₀ ≤ 3⋅X₂ ∧ X₁ ≤ 0 ∧ 1 ≤ X₀ ∧ X₀ ≤ X₂
l1_v2
l1_v2
l2_v2
l2_v2
l1_v2->l2_v2
p = 1
t₂₂ ∈ g₂₃
τ = 1 ≤ X₁ ∧ 1 ≤ X₂ ∧ 2+X₀ ≤ X₂ ∧ 0 ≤ X₀ ∧ 2⋅X₀ ≤ 3⋅X₂ ∧ 1 ≤ X₀ ∧ X₀ ≤ X₂
l1_v2->l3
p = 1
t₂₄ ∈ g₂₅
τ = 1 ≤ X₂ ∧ 2+X₀ ≤ X₂ ∧ X₀ ≤ X₂ ∧ 2⋅X₀ ≤ 3⋅X₂ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
l1_v3
l1_v3
l2_v3
l2_v3
l1_v3->l2_v3
p = 1
t₃₁ ∈ g₃₂
τ = 1 ≤ X₁ ∧ 1 ≤ X₂ ∧ 0 ≤ X₀ ∧ 2⋅X₀ ≤ 3⋅X₂ ∧ 1 ≤ X₀ ∧ X₀ ≤ X₂
l1_v4
l1_v4
l1_v4->l2_v2
p = 1
t₂₉ ∈ g₃₀
τ = 1 ≤ X₁ ∧ 1 ≤ X₂ ∧ 2+X₀ ≤ X₂ ∧ 0 ≤ X₀ ∧ 2⋅X₀ ≤ 3⋅X₂ ∧ 1 ≤ X₀ ∧ X₀ ≤ X₂
l2_v1->l1_v1
p = 1
t₁₇ ∈ g₁₈
η (X₀) = 3⋅X₀
η (X₂) = 2⋅X₂
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ X₁ ≤ 0
l2_v1->l1_v2
p = 1/2
t₁₉ ∈ g₂₁
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁
l2_v1->l1_v3
p = 1/2
t₂₀ ∈ g₂₁
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁
l2_v2->l1_v2
p = 1/2
t₂₆ ∈ g₂₈
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ 2+X₀ ≤ X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁
l2_v2->l1_v4
p = 1/2
t₂₇ ∈ g₂₈
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ 2+X₀ ≤ X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁
l2_v3->l1_v2
p = 1/2
t₃₃ ∈ g₃₅
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁
l2_v3->l1_v3
p = 1/2
t₃₄ ∈ g₃₅
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁
l2_v4->l1_v1
p = 1
t₃₈ ∈ g₃₉
η (X₀) = 3⋅X₀
η (X₂) = 2⋅X₂
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ 3 ≤ X₀ ∧ X₀ ≤ X₂ ∧ X₁ ≤ 0
l3->l3
p = 1
t₁₂ ∈ g₁₁
η (X₂) = X₂-1
τ = 1 ≤ X₀+X₁ ∧ 1+X₀ ≤ X₁ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 1 ≤ X₂
Use expected size bounds for entry point (g₂₁:l2_v1→[t₁₉:1/2:l1_v2; t₂₀:1/2:l1_v3],l1_v2)
Use classical time bound for entry point (g₂₁:l2_v1→[t₁₉:1/2:l1_v2; t₂₀:1/2:l1_v3],l1_v2)
Use expected size bounds for entry point (g₃₅:l2_v3→[t₃₃:1/2:l1_v2; t₃₄:1/2:l1_v3],l1_v2)
Use classical time bound for entry point (g₃₅:l2_v3→[t₃₃:1/2:l1_v2; t₃₄:1/2:l1_v3],l1_v2)
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, l2_v1, l2_v2, l2_v3, l2_v4, l3
Transitions:
g₀:l0(X₀,X₁,X₂) → t₁:l1(X₀,X₁,X₂) :|:
g₉:l1(X₀,X₁,X₂) → t₁₀:l3(X₀,X₁,X₂) :|: 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
g₁₁:l3(X₀,X₁,X₂) → t₁₂:l3(X₀,X₁,X₂-1) :|: 1 ≤ X₂ ∧ 1 ≤ X₀+X₁ ∧ 1+X₀ ≤ X₁ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
g₁₄:l1(X₀,X₁,X₂) → t₁₃:l2_v1(X₀,X₁,X₂) :|: 1 ≤ X₀ ∧ X₀ ≤ X₂
g₁₆:l1(X₀,X₁,X₂) → t₁₅:l3(X₀,X₁,X₂) :|: 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
g₁₈:l2_v1(X₀,X₁,X₂) → t₁₇:l1_v1(3⋅X₀,X₁,2⋅X₂) :|: X₁ ≤ 0 ∧ 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂
g₂₁:l2_v1(X₀,X₁,X₂) → [1/2]:t₁₉:l1_v2(X₀-1,X₁,1+X₂) :+: [1/2]:t₂₀:l1_v3(X₀,X₁,X₂) :|: 1 ≤ X₁ ∧ 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂
g₂₃:l1_v2(X₀,X₁,X₂) → t₂₂:l2_v2(X₀,X₁,X₂) :|: 1 ≤ X₀ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁ ∧ 1 ≤ X₂ ∧ 2+X₀ ≤ X₂ ∧ 0 ≤ X₀ ∧ 2⋅X₀ ≤ 3⋅X₂
g₂₅:l1_v2(X₀,X₁,X₂) → t₂₄:l3(X₀,X₁,X₂) :|: 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 1 ≤ X₂ ∧ 2+X₀ ≤ X₂ ∧ X₀ ≤ X₂ ∧ 2⋅X₀ ≤ 3⋅X₂
g₂₈:l2_v2(X₀,X₁,X₂) → [1/2]:t₂₆:l1_v2(X₀-1,X₁,1+X₂) :+: [1/2]:t₂₇:l1_v4(X₀,X₁,X₂) :|: 1 ≤ X₁ ∧ 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ 2+X₀ ≤ X₂ ∧ X₀ ≤ X₂
g₃₀:l1_v4(X₀,X₁,X₂) → t₂₉:l2_v2(X₀,X₁,X₂) :|: 1 ≤ X₀ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁ ∧ 1 ≤ X₂ ∧ 2+X₀ ≤ X₂ ∧ 0 ≤ X₀ ∧ 2⋅X₀ ≤ 3⋅X₂
g₃₂:l1_v3(X₀,X₁,X₂) → t₃₁:l2_v3(X₀,X₁,X₂) :|: 1 ≤ X₀ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁ ∧ 1 ≤ X₂ ∧ 0 ≤ X₀ ∧ 2⋅X₀ ≤ 3⋅X₂
g₃₅:l2_v3(X₀,X₁,X₂) → [1/2]:t₃₃:l1_v2(X₀-1,X₁,1+X₂) :+: [1/2]:t₃₄:l1_v3(X₀,X₁,X₂) :|: 1 ≤ X₁ ∧ 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂
g₃₇:l1_v1(X₀,X₁,X₂) → t₃₆:l2_v4(X₀,X₁,X₂) :|: 1 ≤ X₀ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₂ ∧ 3 ≤ X₀ ∧ 0 ≤ X₀ ∧ 2⋅X₀ ≤ 3⋅X₂ ∧ X₁ ≤ 0
g₃₉:l2_v4(X₀,X₁,X₂) → t₃₈:l1_v1(3⋅X₀,X₁,2⋅X₂) :|: X₁ ≤ 0 ∧ 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ 3 ≤ X₀ ∧ X₀ ≤ X₂
Show Graph
G
l0
l0
l1
l1
l0->l1
t₁ ∈ g₀
l2_v1
l2_v1
l1->l2_v1
t₁₃ ∈ g₁₄
τ = 1 ≤ X₀ ∧ X₀ ≤ X₂
l3
l3
l1->l3
t₁₀ ∈ g₉
τ = 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
l1->l3
t₁₅ ∈ g₁₆
τ = 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
l1_v1
l1_v1
l2_v4
l2_v4
l1_v1->l2_v4
t₃₆ ∈ g₃₇
τ = 1 ≤ X₂ ∧ 3 ≤ X₀ ∧ 0 ≤ X₀ ∧ 2⋅X₀ ≤ 3⋅X₂ ∧ X₁ ≤ 0 ∧ 1 ≤ X₀ ∧ X₀ ≤ X₂
l1_v2
l1_v2
l2_v2
l2_v2
l1_v2->l2_v2
t₂₂ ∈ g₂₃
τ = 1 ≤ X₁ ∧ 1 ≤ X₂ ∧ 2+X₀ ≤ X₂ ∧ 0 ≤ X₀ ∧ 2⋅X₀ ≤ 3⋅X₂ ∧ 1 ≤ X₀ ∧ X₀ ≤ X₂
l1_v2->l3
t₂₄ ∈ g₂₅
τ = 1 ≤ X₂ ∧ 2+X₀ ≤ X₂ ∧ X₀ ≤ X₂ ∧ 2⋅X₀ ≤ 3⋅X₂ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
l1_v3
l1_v3
l2_v3
l2_v3
l1_v3->l2_v3
t₃₁ ∈ g₃₂
τ = 1 ≤ X₁ ∧ 1 ≤ X₂ ∧ 0 ≤ X₀ ∧ 2⋅X₀ ≤ 3⋅X₂ ∧ 1 ≤ X₀ ∧ X₀ ≤ X₂
l1_v4
l1_v4
l1_v4->l2_v2
t₂₉ ∈ g₃₀
τ = 1 ≤ X₁ ∧ 1 ≤ X₂ ∧ 2+X₀ ≤ X₂ ∧ 0 ≤ X₀ ∧ 2⋅X₀ ≤ 3⋅X₂ ∧ 1 ≤ X₀ ∧ X₀ ≤ X₂
l2_v1->l1_v1
t₁₇ ∈ g₁₈
η (X₀) = 3⋅X₀
η (X₂) = 2⋅X₂
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ X₁ ≤ 0
l2_v1->l1_v2
t₁₉ ∈ g₂₁
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁
l2_v1->l1_v3
t₂₀ ∈ g₂₁
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁
l2_v2->l1_v2
t₂₆ ∈ g₂₈
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ 2+X₀ ≤ X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁
l2_v2->l1_v4
t₂₇ ∈ g₂₈
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ 2+X₀ ≤ X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁
l2_v3->l1_v2
t₃₃ ∈ g₃₅
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁
l2_v3->l1_v3
t₃₄ ∈ g₃₅
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁
l2_v4->l1_v1
t₃₈ ∈ g₃₉
η (X₀) = 3⋅X₀
η (X₂) = 2⋅X₂
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ 3 ≤ X₀ ∧ X₀ ≤ X₂ ∧ X₁ ≤ 0
l3->l3
t₁₂ ∈ g₁₁
η (X₂) = X₂-1
τ = 1 ≤ X₀+X₁ ∧ 1+X₀ ≤ X₁ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 1 ≤ X₂
Run classical analysis on SCC: [l3]
MPRF for transition t₁₂: l3(X₀,X₁,X₂) → l3(X₀,X₁,X₂-1) :|: 1 ≤ X₀+X₁ ∧ 1+X₀ ≤ X₁ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 1 ≤ X₂ of depth 1:
new bound:
2⋅X₀+6⋅X₂+4 {O(n)}
MPRF:
• l3: [X₂]
Show Graph
G
l0
l0
l1
l1
l0->l1
t₁
l2_v1
l2_v1
l1->l2_v1
t₁₃
τ = 1 ≤ X₀ ∧ X₀ ≤ X₂
l3
l3
l1->l3
t₁₀
τ = 1 ≤ X₁ ∧ X₀ ≤ 0 ∧ 0 ≤ X₀
l1->l3
t₁₅
τ = 1 ≤ X₁ ∧ X₀ ≤ 0 ∧ 0 ≤ X₀
l1_v1
l1_v1
l2_v4
l2_v4
l1_v1->l2_v4
t₃₆
τ = 1 ≤ X₂ ∧ 3 ≤ X₀ ∧ 0 ≤ X₀ ∧ 2⋅X₀ ≤ 3⋅X₂ ∧ X₁ ≤ 0 ∧ 1 ≤ X₀ ∧ X₀ ≤ X₂
l1_v2
l1_v2
l2_v2
l2_v2
l1_v2->l2_v2
t₂₂
τ = 1 ≤ X₁ ∧ 1 ≤ X₂ ∧ 2+X₀ ≤ X₂ ∧ 0 ≤ X₀ ∧ 2⋅X₀ ≤ 3⋅X₂ ∧ 1 ≤ X₀ ∧ X₀ ≤ X₂
l1_v2->l3
t₂₄
τ = 1 ≤ X₂ ∧ 2+X₀ ≤ X₂ ∧ X₀ ≤ X₂ ∧ 2⋅X₀ ≤ 3⋅X₂ ∧ 1 ≤ X₁ ∧ X₀ ≤ 0 ∧ 0 ≤ X₀
l1_v3
l1_v3
l2_v3
l2_v3
l1_v3->l2_v3
t₃₁
τ = 1 ≤ X₁ ∧ 1 ≤ X₂ ∧ 0 ≤ X₀ ∧ 2⋅X₀ ≤ 3⋅X₂ ∧ 1 ≤ X₀ ∧ X₀ ≤ X₂
l1_v4
l1_v4
l1_v4->l2_v2
t₂₉
τ = 1 ≤ X₁ ∧ 1 ≤ X₂ ∧ 2+X₀ ≤ X₂ ∧ 0 ≤ X₀ ∧ 2⋅X₀ ≤ 3⋅X₂ ∧ 1 ≤ X₀ ∧ X₀ ≤ X₂
l2_v1->l1_v1
t₁₇
η (X₀) = 3⋅X₀
η (X₂) = 2⋅X₂
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ X₁ ≤ 0
l2_v1->l1_v2
t₁₉
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁
l2_v1->l1_v3
t₂₀
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁
l2_v2->l1_v2
t₂₆
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ 2+X₀ ≤ X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁
l2_v2->l1_v4
t₂₇
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ 2+X₀ ≤ X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁
l2_v3->l1_v2
t₃₃
η (X₀) = X₀-1
η (X₂) = 1+X₂
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁
l2_v3->l1_v3
t₃₄
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁
l2_v4->l1_v1
t₃₈
η (X₀) = 3⋅X₀
η (X₂) = 2⋅X₂
τ = 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ 3 ≤ X₀ ∧ X₀ ≤ X₂ ∧ X₁ ≤ 0
l3->l3
t₁₂
η (X₂) = X₂-1
τ = 1 ≤ X₀+X₁ ∧ 1+X₀ ≤ X₁ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 1 ≤ X₂
Classical Approximation after Lifting Classical Results
All Bounds
Timebounds
Overall timebound:10⋅X₀+16⋅X₂+X₁+31 {O(n)}
g₀: 1 {O(1)}
g₉: 1 {O(1)}
g₁₁: 2⋅X₀+6⋅X₂+4 {O(n)}
g₁₄: 1 {O(1)}
g₁₆: 1 {O(1)}
g₁₈: 1 {O(1)}
g₂₁: 2 {O(1)}
g₂₃: 2⋅X₀+2 {O(n)}
g₂₅: 1 {O(1)}
g₂₈: 4⋅X₀ {O(n)}
g₃₀: 2⋅X₀ {O(n)}
g₃₂: X₁+1 {O(n)}
g₃₅: 2⋅X₂ {O(n)}
g₃₇: 4⋅X₂+8 {O(n)}
g₃₉: 4⋅X₂+8 {O(n)}
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}
g₃₉: inf {Infinity}
Sizebounds
(g₀,l1), X₀: X₀ {O(n)}
(g₀,l1), X₁: X₁ {O(n)}
(g₀,l1), X₂: X₂ {O(n)}
(g₉,l3), X₀: 0 {O(1)}
(g₉,l3), X₁: X₁ {O(n)}
(g₉,l3), X₂: X₂ {O(n)}
(g₁₁,l3), X₀: 0 {O(1)}
(g₁₁,l3), X₁: 6⋅X₁ {O(n)}
(g₁₁,l3), X₂: 2⋅X₀+6⋅X₂+4 {O(n)}
(g₁₄,l2_v1), X₀: X₀ {O(n)}
(g₁₄,l2_v1), X₁: X₁ {O(n)}
(g₁₄,l2_v1), X₂: X₂ {O(n)}
(g₁₆,l3), X₀: 0 {O(1)}
(g₁₆,l3), X₁: X₁ {O(n)}
(g₁₆,l3), X₂: X₂ {O(n)}
(g₁₈,l1_v1), X₀: 3⋅X₀ {O(n)}
(g₁₈,l1_v1), X₁: X₁ {O(n)}
(g₁₈,l1_v1), X₂: 2⋅X₂ {O(n)}
(g₂₁,l1_v2), X₀: X₀ {O(n)}
(g₂₁,l1_v2), X₁: X₁ {O(n)}
(g₂₁,l1_v2), X₂: 2⋅X₂+1 {O(n)}
(g₂₁,l1_v3), X₀: X₀ {O(n)}
(g₂₁,l1_v3), X₁: X₁ {O(n)}
(g₂₁,l1_v3), X₂: X₂ {O(n)}
(g₂₃,l2_v2), X₀: 2⋅X₀ {O(n)}
(g₂₃,l2_v2), X₁: 2⋅X₁ {O(n)}
(g₂₃,l2_v2), X₂: 2⋅X₀+2⋅X₂+2 {O(n)}
(g₂₅,l3), X₀: 0 {O(1)}
(g₂₅,l3), X₁: 4⋅X₁ {O(n)}
(g₂₅,l3), X₂: 2⋅X₀+4⋅X₂+4 {O(n)}
(g₂₈,l1_v2), X₀: 4⋅X₀ {O(n)}
(g₂₈,l1_v2), X₁: 4⋅X₁ {O(n)}
(g₂₈,l1_v2), X₂: 4⋅X₀+4⋅X₂+4 {O(n)}
(g₂₈,l1_v4), X₀: 4⋅X₀ {O(n)}
(g₂₈,l1_v4), X₁: 4⋅X₁ {O(n)}
(g₂₈,l1_v4), X₂: 4⋅X₀+4⋅X₂+4 {O(n)}
(g₃₀,l2_v2), X₀: 2⋅X₀ {O(n)}
(g₃₀,l2_v2), X₁: 2⋅X₁ {O(n)}
(g₃₀,l2_v2), X₂: 2⋅X₀+2⋅X₂+2 {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_v2), X₀: X₀ {O(n)}
(g₃₅,l1_v2), X₁: X₁ {O(n)}
(g₃₅,l1_v2), X₂: 2⋅X₂ {O(n)}
(g₃₅,l1_v3), X₀: X₀ {O(n)}
(g₃₅,l1_v3), X₁: X₁ {O(n)}
(g₃₅,l1_v3), X₂: X₂ {O(n)}
(g₃₇,l2_v4), X₀: 3⋅3^(4⋅X₂+8)⋅X₀ {O(EXP)}
(g₃₇,l2_v4), X₁: X₁ {O(n)}
(g₃₇,l2_v4), X₂: 2⋅2^(4⋅X₂+8)⋅X₂ {O(EXP)}
(g₃₉,l1_v1), X₀: 3⋅3^(4⋅X₂+8)⋅X₀ {O(EXP)}
(g₃₉,l1_v1), X₁: X₁ {O(n)}
(g₃₉,l1_v1), X₂: 2⋅2^(4⋅X₂+8)⋅X₂ {O(EXP)}
Run probabilistic analysis on SCC: [l3]
Results of Probabilistic Analysis
All Bounds
Timebounds
Overall timebound:10⋅X₀+16⋅X₂+X₁+31 {O(n)}
g₀: 1 {O(1)}
g₉: 1 {O(1)}
g₁₁: 2⋅X₀+6⋅X₂+4 {O(n)}
g₁₄: 1 {O(1)}
g₁₆: 1 {O(1)}
g₁₈: 1 {O(1)}
g₂₁: 2 {O(1)}
g₂₃: 2⋅X₀+2 {O(n)}
g₂₅: 1 {O(1)}
g₂₈: 4⋅X₀ {O(n)}
g₃₀: 2⋅X₀ {O(n)}
g₃₂: X₁+1 {O(n)}
g₃₅: 2⋅X₂ {O(n)}
g₃₇: 4⋅X₂+8 {O(n)}
g₃₉: 4⋅X₂+8 {O(n)}
Costbounds
Overall costbound: 14⋅X₀+18⋅X₂+X₁+33 {O(n)}
g₀: 1 {O(1)}
g₉: 1 {O(1)}
g₁₁: 2⋅X₀+6⋅X₂+4 {O(n)}
g₁₄: 1 {O(1)}
g₁₆: 1 {O(1)}
g₁₈: 1 {O(1)}
g₂₁: 4 {O(1)}
g₂₃: 2⋅X₀+2 {O(n)}
g₂₅: 1 {O(1)}
g₂₈: 8⋅X₀ {O(n)}
g₃₀: 2⋅X₀ {O(n)}
g₃₂: X₁+1 {O(n)}
g₃₅: 4⋅X₂ {O(n)}
g₃₇: 4⋅X₂+8 {O(n)}
g₃₉: 4⋅X₂+8 {O(n)}
Sizebounds
(g₀,l1), X₀: X₀ {O(n)}
(g₀,l1), X₁: X₁ {O(n)}
(g₀,l1), X₂: X₂ {O(n)}
(g₉,l3), X₀: 0 {O(1)}
(g₉,l3), X₁: X₁ {O(n)}
(g₉,l3), X₂: X₂ {O(n)}
(g₁₁,l3), X₀: 0 {O(1)}
(g₁₁,l3), X₁: 6⋅X₁ {O(n)}
(g₁₁,l3), X₂: 2⋅X₀+6⋅X₂+4 {O(n)}
(g₁₄,l2_v1), X₀: X₀ {O(n)}
(g₁₄,l2_v1), X₁: X₁ {O(n)}
(g₁₄,l2_v1), X₂: X₂ {O(n)}
(g₁₆,l3), X₀: 0 {O(1)}
(g₁₆,l3), X₁: X₁ {O(n)}
(g₁₆,l3), X₂: X₂ {O(n)}
(g₁₈,l1_v1), X₀: 3⋅X₀ {O(n)}
(g₁₈,l1_v1), X₁: X₁ {O(n)}
(g₁₈,l1_v1), X₂: 2⋅X₂ {O(n)}
(g₂₁,l1_v2), X₀: X₀ {O(n)}
(g₂₁,l1_v2), X₁: X₁ {O(n)}
(g₂₁,l1_v2), X₂: 2⋅X₂+1 {O(n)}
(g₂₁,l1_v3), X₀: X₀ {O(n)}
(g₂₁,l1_v3), X₁: X₁ {O(n)}
(g₂₁,l1_v3), X₂: X₂ {O(n)}
(g₂₃,l2_v2), X₀: 2⋅X₀ {O(n)}
(g₂₃,l2_v2), X₁: 2⋅X₁ {O(n)}
(g₂₃,l2_v2), X₂: 2⋅X₀+2⋅X₂+2 {O(n)}
(g₂₅,l3), X₀: 0 {O(1)}
(g₂₅,l3), X₁: 4⋅X₁ {O(n)}
(g₂₅,l3), X₂: 2⋅X₀+4⋅X₂+4 {O(n)}
(g₂₈,l1_v2), X₀: 4⋅X₀ {O(n)}
(g₂₈,l1_v2), X₁: 4⋅X₁ {O(n)}
(g₂₈,l1_v2), X₂: 4⋅X₀+4⋅X₂+4 {O(n)}
(g₂₈,l1_v4), X₀: 4⋅X₀ {O(n)}
(g₂₈,l1_v4), X₁: 4⋅X₁ {O(n)}
(g₂₈,l1_v4), X₂: 4⋅X₀+4⋅X₂+4 {O(n)}
(g₃₀,l2_v2), X₀: 2⋅X₀ {O(n)}
(g₃₀,l2_v2), X₁: 2⋅X₁ {O(n)}
(g₃₀,l2_v2), X₂: 2⋅X₀+2⋅X₂+2 {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_v2), X₀: X₀ {O(n)}
(g₃₅,l1_v2), X₁: X₁ {O(n)}
(g₃₅,l1_v2), X₂: 2⋅X₂ {O(n)}
(g₃₅,l1_v3), X₀: X₀ {O(n)}
(g₃₅,l1_v3), X₁: X₁ {O(n)}
(g₃₅,l1_v3), X₂: X₂ {O(n)}
(g₃₇,l2_v4), X₀: 3⋅3^(4⋅X₂+8)⋅X₀ {O(EXP)}
(g₃₇,l2_v4), X₁: X₁ {O(n)}
(g₃₇,l2_v4), X₂: 2⋅2^(4⋅X₂+8)⋅X₂ {O(EXP)}
(g₃₉,l1_v1), X₀: 3⋅3^(4⋅X₂+8)⋅X₀ {O(EXP)}
(g₃₉,l1_v1), X₁: X₁ {O(n)}
(g₃₉,l1_v1), X₂: 2⋅2^(4⋅X₂+8)⋅X₂ {O(EXP)}