Preprocessing
Found invariant 3+X₀ ≤ X₃ for location h
Probabilistic Analysis
Probabilistic Program after Preprocessing
Start: f
Program_Vars: X₀, X₁, X₂, X₃
Temp_Vars:
Locations: f, g, h
Transitions:
g₀:f(X₀,X₁,X₂,X₃) -{0}> t₁:g(X₀,X₁,X₂,X₃) :|:
g₂:g(X₀,X₁,X₂,X₃) -{0}> t₃:h(X₀,X₁,X₂,X₃) :|: 3+X₀ ≤ X₃
g₄:h(X₀,X₁,X₂,X₃) → [1/2]:t₅:g(X₀,1+X₁,X₂,X₃) :+: [1/2]:t₆:g(X₀,X₁,X₂,X₃) :|: 1+X₁ ≤ X₂ ∧ 3+X₀ ≤ X₃
g₇:h(X₀,X₁,X₂,X₃) → [1/4]:t₈:g(X₀,X₁,X₂,X₃) :+: [1/4]:t₉:g(1+X₀,X₁,X₂,X₃) :+: [1/4]:t₁₀:g(2+X₀,X₁,X₂,X₃) :+: [1/4]:t₁₁:g(3+X₀,X₁,X₂,X₃) :|: X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
Show Graph
G
f
f
g
g
f->g
p = 1
t₁ ∈ g₀
{0}
h
h
g->h
p = 1
t₃ ∈ g₂
τ = 3+X₀ ≤ X₃
{0}
h->g
p = 1/2
t₅ ∈ g₄
η (X₁) = 1+X₁
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
h->g
p = 1/2
t₆ ∈ g₄
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
h->g
p = 1/4
t₈ ∈ g₇
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h->g
p = 1/4
t₉ ∈ g₇
η (X₀) = 1+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h->g
p = 1/4
t₁₀ ∈ g₇
η (X₀) = 2+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h->g
p = 1/4
t₁₁ ∈ g₇
η (X₀) = 3+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
Run classical analysis on SCC: [f]
Classical Approximation after Lifting Classical Results
All Bounds
Timebounds
Overall timebound:inf {Infinity}
g₀: 1 {O(1)}
g₂: inf {Infinity}
g₄: inf {Infinity}
g₇: inf {Infinity}
Costbounds
Overall costbound: 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)}
Run probabilistic analysis on SCC: [f]
Run classical analysis on SCC: [g; h]
MPRF for transition t₅: h(X₀,X₁,X₂,X₃) → g(X₀,1+X₁,X₂,X₃) :|: 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂ of depth 1:
new bound:
X₁+X₂ {O(n)}
MPRF:
• g: [X₂-X₁]
• h: [X₂-X₁]
Show Graph
G
f
f
g
g
f->g
t₁
{0}
h
h
g->h
t₃
τ = 3+X₀ ≤ X₃
{0}
h->g
t₅
η (X₁) = 1+X₁
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
h->g
t₆
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
h->g
t₈
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h->g
t₉
η (X₀) = 1+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h->g
t₁₀
η (X₀) = 2+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h->g
t₁₁
η (X₀) = 3+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
MPRF for transition t₉: h(X₀,X₁,X₂,X₃) → g(1+X₀,X₁,X₂,X₃) :|: 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁ of depth 1:
new bound:
X₀+X₃+2 {O(n)}
MPRF:
• g: [X₃-2-X₀]
• h: [X₃-2-X₀]
Show Graph
G
f
f
g
g
f->g
t₁
{0}
h
h
g->h
t₃
τ = 3+X₀ ≤ X₃
{0}
h->g
t₅
η (X₁) = 1+X₁
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
h->g
t₆
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
h->g
t₈
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h->g
t₉
η (X₀) = 1+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h->g
t₁₀
η (X₀) = 2+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h->g
t₁₁
η (X₀) = 3+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
MPRF for transition t₁₀: h(X₀,X₁,X₂,X₃) → g(2+X₀,X₁,X₂,X₃) :|: 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁ of depth 1:
new bound:
X₀+X₃+2 {O(n)}
MPRF:
• g: [X₃-2-X₀]
• h: [X₃-2-X₀]
Show Graph
G
f
f
g
g
f->g
t₁
{0}
h
h
g->h
t₃
τ = 3+X₀ ≤ X₃
{0}
h->g
t₅
η (X₁) = 1+X₁
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
h->g
t₆
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
h->g
t₈
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h->g
t₉
η (X₀) = 1+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h->g
t₁₀
η (X₀) = 2+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h->g
t₁₁
η (X₀) = 3+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
MPRF for transition t₁₁: h(X₀,X₁,X₂,X₃) → g(3+X₀,X₁,X₂,X₃) :|: 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁ of depth 1:
new bound:
X₀+X₃+2 {O(n)}
MPRF:
• g: [X₃-2-X₀]
• h: [X₃-2-X₀]
Show Graph
G
f
f
g
g
f->g
t₁
{0}
h
h
g->h
t₃
τ = 3+X₀ ≤ X₃
{0}
h->g
t₅
η (X₁) = 1+X₁
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
h->g
t₆
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
h->g
t₈
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h->g
t₉
η (X₀) = 1+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h->g
t₁₀
η (X₀) = 2+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h->g
t₁₁
η (X₀) = 3+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
Classical Approximation after Lifting Classical Results
All Bounds
Timebounds
Overall timebound:inf {Infinity}
g₀: 1 {O(1)}
g₂: inf {Infinity}
g₄: inf {Infinity}
g₇: inf {Infinity}
Costbounds
Overall costbound: inf {Infinity}
g₀: inf {Infinity}
g₂: inf {Infinity}
g₄: inf {Infinity}
g₇: inf {Infinity}
Sizebounds
(g₀,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₀: 6⋅X₃+7⋅X₀+12 {O(n)}
(g₂,h), X₁: 2⋅X₁+X₂ {O(n)}
(g₂,h), X₂: X₂ {O(n)}
(g₂,h), X₃: X₃ {O(n)}
(g₄,g), X₀: 12⋅X₃+14⋅X₀+24 {O(n)}
(g₄,g), X₁: 2⋅X₂+4⋅X₁ {O(n)}
(g₄,g), X₂: 2⋅X₂ {O(n)}
(g₄,g), X₃: 2⋅X₃ {O(n)}
(g₇,g), X₀: 24⋅X₃+28⋅X₀+48 {O(n)}
(g₇,g), X₁: 4⋅X₂+8⋅X₁ {O(n)}
(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₇:h(X₀,X₁,X₂,X₃) → [1/4]:t₈:g(X₀,X₁,X₂,X₃) :+: [1/4]:t₉:g(1+X₀,X₁,X₂,X₃) :+: [1/4]:t₁₀:g(2+X₀,X₁,X₂,X₃) :+: [1/4]:t₁₁:g(3+X₀,X₁,X₂,X₃) :|: X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃:
new bound:
2/3⋅X₀+2/3⋅X₃ {O(n)}
PLRF:
• g: 2/3⋅X₃-2/3⋅X₀
• h: 2/3⋅X₃-2/3⋅X₀
Show Graph
G
f
f
g
g
f->g
p = 1
t₁ ∈ g₀
{0}
h
h
g->h
p = 1
t₃ ∈ g₂
τ = 3+X₀ ≤ X₃
{0}
h->g
p = 1/2
t₅ ∈ g₄
η (X₁) = 1+X₁
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
h->g
p = 1/2
t₆ ∈ g₄
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
h->g
p = 1/4
t₈ ∈ g₇
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h->g
p = 1/4
t₉ ∈ g₇
η (X₀) = 1+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h->g
p = 1/4
t₁₀ ∈ g₇
η (X₀) = 2+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h->g
p = 1/4
t₁₁ ∈ g₇
η (X₀) = 3+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
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)
Analysing control-flow refined program
Run classical analysis on SCC: [g]
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₂₃: inf {Infinity}
g₂₈: inf {Infinity}
g₃₀: inf {Infinity}
g₃₂: inf {Infinity}
g₃₄: inf {Infinity}
g₃₆: inf {Infinity}
g₃₈: inf {Infinity}
g₄₁: inf {Infinity}
Costbounds
Overall costbound: inf {Infinity}
g₀: inf {Infinity}
g₁₃: inf {Infinity}
g₁₆: inf {Infinity}
g₂₁: inf {Infinity}
g₂₃: inf {Infinity}
g₂₈: inf {Infinity}
g₃₀: inf {Infinity}
g₃₂: inf {Infinity}
g₃₄: inf {Infinity}
g₃₆: inf {Infinity}
g₃₈: inf {Infinity}
g₄₁: inf {Infinity}
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₁₃,h_v1), X₀: X₀ {O(n)}
(g₁₃,h_v1), X₁: X₁ {O(n)}
(g₁₃,h_v1), X₂: X₂ {O(n)}
(g₁₃,h_v1), X₃: X₃ {O(n)}
Run probabilistic analysis on SCC: [g]
Run classical analysis on SCC: [g_v1; g_v2; h_v1; h_v3]
MPRF for transition t₁₄: h_v1(X₀,X₁,X₂,X₃) → g_v1(X₀,1+X₁,X₂,X₃) :|: 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂ of depth 1:
new bound:
X₁+X₂ {O(n)}
MPRF:
• g_v1: [X₂-X₁]
• g_v2: [X₂-X₁]
• h_v1: [X₂-X₁]
• h_v3: [X₂-X₁]
Show Graph
G
f
f
g
g
f->g
t₁
{0}
h_v1
h_v1
g->h_v1
t₁₂
τ = 3+X₀ ≤ X₃
{0}
g_v1
g_v1
g_v1->h_v1
t₃₅
τ = X₁ ≤ X₂ ∧ 3+X₀ ≤ X₃
{0}
g_v2
g_v2
h_v3
h_v3
g_v2->h_v3
t₃₇
τ = 1+X₁ ≤ X₂ ∧ 3+X₀ ≤ X₃
{0}
g_v3
g_v3
h_v2
h_v2
g_v3->h_v2
t₂₂
τ = X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
g_v4
g_v4
g_v4->h_v2
t₂₉
τ = 2+X₀ ≤ X₃ ∧ X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
g_v5
g_v5
g_v5->h_v2
t₃₁
τ = 1+X₀ ≤ X₃ ∧ X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
g_v6
g_v6
g_v6->h_v2
t₃₃
τ = X₀ ≤ X₃ ∧ X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
h_v1->g_v1
t₁₄
η (X₁) = 1+X₁
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
h_v1->g_v2
t₁₅
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
h_v1->g_v3
t₁₇
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v1->g_v4
t₁₈
η (X₀) = 1+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v1->g_v5
t₁₉
η (X₀) = 2+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v1->g_v6
t₂₀
η (X₀) = 3+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v3
t₂₄
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v4
t₂₅
η (X₀) = 1+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v5
t₂₆
η (X₀) = 2+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v6
t₂₇
η (X₀) = 3+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v3->g_v1
t₃₉
η (X₁) = 1+X₁
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
h_v3->g_v2
t₄₀
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
MPRF for transition t₁₅: h_v1(X₀,X₁,X₂,X₃) → g_v2(X₀,X₁,X₂,X₃) :|: 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂ of depth 1:
new bound:
X₁+X₂+1 {O(n)}
MPRF:
• g_v1: [1+X₂-X₁]
• g_v2: [X₂-X₁]
• h_v1: [1+X₂-X₁]
• h_v3: [X₂-X₁]
Show Graph
G
f
f
g
g
f->g
t₁
{0}
h_v1
h_v1
g->h_v1
t₁₂
τ = 3+X₀ ≤ X₃
{0}
g_v1
g_v1
g_v1->h_v1
t₃₅
τ = X₁ ≤ X₂ ∧ 3+X₀ ≤ X₃
{0}
g_v2
g_v2
h_v3
h_v3
g_v2->h_v3
t₃₇
τ = 1+X₁ ≤ X₂ ∧ 3+X₀ ≤ X₃
{0}
g_v3
g_v3
h_v2
h_v2
g_v3->h_v2
t₂₂
τ = X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
g_v4
g_v4
g_v4->h_v2
t₂₉
τ = 2+X₀ ≤ X₃ ∧ X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
g_v5
g_v5
g_v5->h_v2
t₃₁
τ = 1+X₀ ≤ X₃ ∧ X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
g_v6
g_v6
g_v6->h_v2
t₃₃
τ = X₀ ≤ X₃ ∧ X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
h_v1->g_v1
t₁₄
η (X₁) = 1+X₁
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
h_v1->g_v2
t₁₅
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
h_v1->g_v3
t₁₇
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v1->g_v4
t₁₈
η (X₀) = 1+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v1->g_v5
t₁₉
η (X₀) = 2+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v1->g_v6
t₂₀
η (X₀) = 3+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v3
t₂₄
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v4
t₂₅
η (X₀) = 1+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v5
t₂₆
η (X₀) = 2+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v6
t₂₇
η (X₀) = 3+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v3->g_v1
t₃₉
η (X₁) = 1+X₁
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
h_v3->g_v2
t₄₀
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
MPRF for transition t₃₅: g_v1(X₀,X₁,X₂,X₃) -{0}> h_v1(X₀,X₁,X₂,X₃) :|: X₁ ≤ X₂ ∧ 3+X₀ ≤ X₃ of depth 1:
new bound:
X₁+X₂ {O(n)}
MPRF:
• g_v1: [1+X₂-X₁]
• g_v2: [X₂-X₁]
• h_v1: [X₂-X₁]
• h_v3: [X₂-X₁]
Show Graph
G
f
f
g
g
f->g
t₁
{0}
h_v1
h_v1
g->h_v1
t₁₂
τ = 3+X₀ ≤ X₃
{0}
g_v1
g_v1
g_v1->h_v1
t₃₅
τ = X₁ ≤ X₂ ∧ 3+X₀ ≤ X₃
{0}
g_v2
g_v2
h_v3
h_v3
g_v2->h_v3
t₃₇
τ = 1+X₁ ≤ X₂ ∧ 3+X₀ ≤ X₃
{0}
g_v3
g_v3
h_v2
h_v2
g_v3->h_v2
t₂₂
τ = X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
g_v4
g_v4
g_v4->h_v2
t₂₉
τ = 2+X₀ ≤ X₃ ∧ X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
g_v5
g_v5
g_v5->h_v2
t₃₁
τ = 1+X₀ ≤ X₃ ∧ X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
g_v6
g_v6
g_v6->h_v2
t₃₃
τ = X₀ ≤ X₃ ∧ X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
h_v1->g_v1
t₁₄
η (X₁) = 1+X₁
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
h_v1->g_v2
t₁₅
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
h_v1->g_v3
t₁₇
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v1->g_v4
t₁₈
η (X₀) = 1+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v1->g_v5
t₁₉
η (X₀) = 2+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v1->g_v6
t₂₀
η (X₀) = 3+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v3
t₂₄
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v4
t₂₅
η (X₀) = 1+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v5
t₂₆
η (X₀) = 2+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v6
t₂₇
η (X₀) = 3+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v3->g_v1
t₃₉
η (X₁) = 1+X₁
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
h_v3->g_v2
t₄₀
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
MPRF for transition t₃₉: h_v3(X₀,X₁,X₂,X₃) → g_v1(X₀,1+X₁,X₂,X₃) :|: 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂ of depth 1:
new bound:
X₁+X₂ {O(n)}
MPRF:
• g_v1: [X₂-X₁]
• g_v2: [X₂-X₁]
• h_v1: [X₂-X₁]
• h_v3: [X₂-X₁]
Show Graph
G
f
f
g
g
f->g
t₁
{0}
h_v1
h_v1
g->h_v1
t₁₂
τ = 3+X₀ ≤ X₃
{0}
g_v1
g_v1
g_v1->h_v1
t₃₅
τ = X₁ ≤ X₂ ∧ 3+X₀ ≤ X₃
{0}
g_v2
g_v2
h_v3
h_v3
g_v2->h_v3
t₃₇
τ = 1+X₁ ≤ X₂ ∧ 3+X₀ ≤ X₃
{0}
g_v3
g_v3
h_v2
h_v2
g_v3->h_v2
t₂₂
τ = X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
g_v4
g_v4
g_v4->h_v2
t₂₉
τ = 2+X₀ ≤ X₃ ∧ X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
g_v5
g_v5
g_v5->h_v2
t₃₁
τ = 1+X₀ ≤ X₃ ∧ X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
g_v6
g_v6
g_v6->h_v2
t₃₃
τ = X₀ ≤ X₃ ∧ X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
h_v1->g_v1
t₁₄
η (X₁) = 1+X₁
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
h_v1->g_v2
t₁₅
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
h_v1->g_v3
t₁₇
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v1->g_v4
t₁₈
η (X₀) = 1+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v1->g_v5
t₁₉
η (X₀) = 2+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v1->g_v6
t₂₀
η (X₀) = 3+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v3
t₂₄
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v4
t₂₅
η (X₀) = 1+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v5
t₂₆
η (X₀) = 2+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v6
t₂₇
η (X₀) = 3+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v3->g_v1
t₃₉
η (X₁) = 1+X₁
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
h_v3->g_v2
t₄₀
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
Classical Approximation after Lifting Classical Results
All Bounds
Timebounds
Overall timebound:inf {Infinity}
g₀: 1 {O(1)}
g₁₃: 1 {O(1)}
g₁₆: 2⋅X₁+2⋅X₂+1 {O(n)}
g₂₁: 4 {O(1)}
g₂₃: inf {Infinity}
g₂₈: inf {Infinity}
g₃₀: inf {Infinity}
g₃₂: inf {Infinity}
g₃₄: inf {Infinity}
g₃₆: X₁+X₂ {O(n)}
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}
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₁₃,h_v1), X₀: X₀ {O(n)}
(g₁₃,h_v1), X₁: X₁ {O(n)}
(g₁₃,h_v1), X₂: X₂ {O(n)}
(g₁₃,h_v1), X₃: X₃ {O(n)}
(g₁₆,g_v1), X₀: 2⋅X₀ {O(n)}
(g₁₆,g_v1), X₁: 4⋅X₂+6⋅X₁ {O(n)}
(g₁₆,g_v1), X₂: 2⋅X₂ {O(n)}
(g₁₆,g_v1), X₃: 2⋅X₃ {O(n)}
(g₁₆,g_v2), X₀: 2⋅X₀ {O(n)}
(g₁₆,g_v2), X₁: 4⋅X₂+6⋅X₁ {O(n)}
(g₁₆,g_v2), X₂: 2⋅X₂ {O(n)}
(g₁₆,g_v2), X₃: 2⋅X₃ {O(n)}
(g₂₁,g_v3), X₀: 8⋅X₀+12 {O(n)}
(g₂₁,g_v3), X₁: 16⋅X₁+8⋅X₂ {O(n)}
(g₂₁,g_v3), X₂: 8⋅X₂ {O(n)}
(g₂₁,g_v3), X₃: 8⋅X₃ {O(n)}
(g₂₁,g_v4), X₀: 8⋅X₀+12 {O(n)}
(g₂₁,g_v4), X₁: 16⋅X₁+8⋅X₂ {O(n)}
(g₂₁,g_v4), X₂: 8⋅X₂ {O(n)}
(g₂₁,g_v4), X₃: 8⋅X₃ {O(n)}
(g₂₁,g_v5), X₀: 8⋅X₀+12 {O(n)}
(g₂₁,g_v5), X₁: 16⋅X₁+8⋅X₂ {O(n)}
(g₂₁,g_v5), X₂: 8⋅X₂ {O(n)}
(g₂₁,g_v5), X₃: 8⋅X₃ {O(n)}
(g₂₁,g_v6), X₀: 8⋅X₀+12 {O(n)}
(g₂₁,g_v6), X₁: 16⋅X₁+8⋅X₂ {O(n)}
(g₂₁,g_v6), X₂: 8⋅X₂ {O(n)}
(g₂₁,g_v6), X₃: 8⋅X₃ {O(n)}
(g₃₆,h_v1), X₀: X₀ {O(n)}
(g₃₆,h_v1), X₁: 2⋅X₂+3⋅X₁ {O(n)}
(g₃₆,h_v1), X₂: X₂ {O(n)}
(g₃₆,h_v1), X₃: X₃ {O(n)}
(g₃₈,h_v3), X₀: X₀ {O(n)}
(g₃₈,h_v3), X₁: 2⋅X₂+3⋅X₁ {O(n)}
(g₃₈,h_v3), X₂: X₂ {O(n)}
(g₃₈,h_v3), X₃: X₃ {O(n)}
(g₄₁,g_v1), X₀: 2⋅X₀ {O(n)}
(g₄₁,g_v1), X₁: 4⋅X₂+6⋅X₁ {O(n)}
(g₄₁,g_v1), X₂: 2⋅X₂ {O(n)}
(g₄₁,g_v1), X₃: 2⋅X₃ {O(n)}
(g₄₁,g_v2), X₀: 2⋅X₀ {O(n)}
(g₄₁,g_v2), X₁: 4⋅X₂+6⋅X₁ {O(n)}
(g₄₁,g_v2), X₂: 2⋅X₂ {O(n)}
(g₄₁,g_v2), X₃: 2⋅X₃ {O(n)}
Run probabilistic analysis on SCC: [g_v1; g_v2; h_v1; h_v3]
Plrf for transition g₃₈:g_v2(X₀,X₁,X₂,X₃) -{0}> t₃₇:h_v3(X₀,X₁,X₂,X₃) :|: 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂:
new bound:
X₁+X₂ {O(n)}
PLRF:
• g_v1: X₂-X₁
• g_v2: 1+X₂-X₁
• h_v1: X₂-X₁
• h_v3: X₂-X₁
Show Graph
G
f
f
g
g
f->g
p = 1
t₁ ∈ g₀
{0}
h_v1
h_v1
g->h_v1
p = 1
t₁₂ ∈ g₁₃
τ = 3+X₀ ≤ X₃
{0}
g_v1
g_v1
g_v1->h_v1
p = 1
t₃₅ ∈ g₃₆
τ = X₁ ≤ X₂ ∧ 3+X₀ ≤ X₃
{0}
g_v2
g_v2
h_v3
h_v3
g_v2->h_v3
p = 1
t₃₇ ∈ g₃₈
τ = 1+X₁ ≤ X₂ ∧ 3+X₀ ≤ X₃
{0}
g_v3
g_v3
h_v2
h_v2
g_v3->h_v2
p = 1
t₂₂ ∈ g₂₃
τ = X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
g_v4
g_v4
g_v4->h_v2
p = 1
t₂₉ ∈ g₃₀
τ = 2+X₀ ≤ X₃ ∧ X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
g_v5
g_v5
g_v5->h_v2
p = 1
t₃₁ ∈ g₃₂
τ = 1+X₀ ≤ X₃ ∧ X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
g_v6
g_v6
g_v6->h_v2
p = 1
t₃₃ ∈ g₃₄
τ = X₀ ≤ X₃ ∧ X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
h_v1->g_v1
p = 1/2
t₁₄ ∈ g₁₆
η (X₁) = 1+X₁
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
h_v1->g_v2
p = 1/2
t₁₅ ∈ g₁₆
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
h_v1->g_v3
p = 1/4
t₁₇ ∈ g₂₁
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v1->g_v4
p = 1/4
t₁₈ ∈ g₂₁
η (X₀) = 1+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v1->g_v5
p = 1/4
t₁₉ ∈ g₂₁
η (X₀) = 2+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v1->g_v6
p = 1/4
t₂₀ ∈ g₂₁
η (X₀) = 3+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v3
p = 1/4
t₂₄ ∈ g₂₈
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v4
p = 1/4
t₂₅ ∈ g₂₈
η (X₀) = 1+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v5
p = 1/4
t₂₆ ∈ g₂₈
η (X₀) = 2+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v6
p = 1/4
t₂₇ ∈ g₂₈
η (X₀) = 3+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v3->g_v1
p = 1/2
t₃₉ ∈ g₄₁
η (X₁) = 1+X₁
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
h_v3->g_v2
p = 1/2
t₄₀ ∈ g₄₁
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
Use expected size bounds for entry point (g₁₃:g→[t₁₂:1:h_v1],h_v1)
Use expected size bounds for entry point (g₁₃:g→[t₁₂:1:h_v1],h_v1)
Use classical time bound for entry point (g₁₃:g→[t₁₂:1:h_v1],h_v1)
Plrf for transition g₄₁:h_v3(X₀,X₁,X₂,X₃) → [1/2]:t₃₉:g_v1(X₀,1+X₁,X₂,X₃) :+: [1/2]:t₄₀:g_v2(X₀,X₁,X₂,X₃) :|: 1+X₁ ≤ X₂ ∧ 3+X₀ ≤ X₃:
new bound:
X₁+X₂ {O(n)}
PLRF:
• g_v1: X₂-X₁
• g_v2: 1+X₂-X₁
• h_v1: X₂-X₁
• h_v3: 1+X₂-X₁
Show Graph
G
f
f
g
g
f->g
p = 1
t₁ ∈ g₀
{0}
h_v1
h_v1
g->h_v1
p = 1
t₁₂ ∈ g₁₃
τ = 3+X₀ ≤ X₃
{0}
g_v1
g_v1
g_v1->h_v1
p = 1
t₃₅ ∈ g₃₆
τ = X₁ ≤ X₂ ∧ 3+X₀ ≤ X₃
{0}
g_v2
g_v2
h_v3
h_v3
g_v2->h_v3
p = 1
t₃₇ ∈ g₃₈
τ = 1+X₁ ≤ X₂ ∧ 3+X₀ ≤ X₃
{0}
g_v3
g_v3
h_v2
h_v2
g_v3->h_v2
p = 1
t₂₂ ∈ g₂₃
τ = X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
g_v4
g_v4
g_v4->h_v2
p = 1
t₂₉ ∈ g₃₀
τ = 2+X₀ ≤ X₃ ∧ X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
g_v5
g_v5
g_v5->h_v2
p = 1
t₃₁ ∈ g₃₂
τ = 1+X₀ ≤ X₃ ∧ X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
g_v6
g_v6
g_v6->h_v2
p = 1
t₃₃ ∈ g₃₄
τ = X₀ ≤ X₃ ∧ X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
h_v1->g_v1
p = 1/2
t₁₄ ∈ g₁₆
η (X₁) = 1+X₁
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
h_v1->g_v2
p = 1/2
t₁₅ ∈ g₁₆
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
h_v1->g_v3
p = 1/4
t₁₇ ∈ g₂₁
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v1->g_v4
p = 1/4
t₁₈ ∈ g₂₁
η (X₀) = 1+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v1->g_v5
p = 1/4
t₁₉ ∈ g₂₁
η (X₀) = 2+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v1->g_v6
p = 1/4
t₂₀ ∈ g₂₁
η (X₀) = 3+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v3
p = 1/4
t₂₄ ∈ g₂₈
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v4
p = 1/4
t₂₅ ∈ g₂₈
η (X₀) = 1+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v5
p = 1/4
t₂₆ ∈ g₂₈
η (X₀) = 2+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v6
p = 1/4
t₂₇ ∈ g₂₈
η (X₀) = 3+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v3->g_v1
p = 1/2
t₃₉ ∈ g₄₁
η (X₁) = 1+X₁
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
h_v3->g_v2
p = 1/2
t₄₀ ∈ g₄₁
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
Use expected size bounds for entry point (g₁₃:g→[t₁₂:1:h_v1],h_v1)
Use expected size bounds for entry point (g₁₃:g→[t₁₂:1:h_v1],h_v1)
Use classical time bound for entry point (g₁₃:g→[t₁₂:1:h_v1],h_v1)
Run classical analysis on SCC: [g_v3; g_v4; g_v5; g_v6; h_v2]
MPRF for transition t₂₅: h_v2(X₀,X₁,X₂,X₃) → g_v4(1+X₀,X₁,X₂,X₃) :|: 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁ of depth 1:
new bound:
8⋅X₀+8⋅X₃+16 {O(n)}
MPRF:
• g_v3: [X₃-2-X₀]
• g_v4: [X₃-2-X₀]
• g_v5: [X₃-X₀]
• g_v6: [X₃-X₀]
• h_v2: [X₃-2-X₀]
Show Graph
G
f
f
g
g
f->g
t₁
{0}
h_v1
h_v1
g->h_v1
t₁₂
τ = 3+X₀ ≤ X₃
{0}
g_v1
g_v1
g_v1->h_v1
t₃₅
τ = X₁ ≤ X₂ ∧ 3+X₀ ≤ X₃
{0}
g_v2
g_v2
h_v3
h_v3
g_v2->h_v3
t₃₇
τ = 1+X₁ ≤ X₂ ∧ 3+X₀ ≤ X₃
{0}
g_v3
g_v3
h_v2
h_v2
g_v3->h_v2
t₂₂
τ = X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
g_v4
g_v4
g_v4->h_v2
t₂₉
τ = 2+X₀ ≤ X₃ ∧ X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
g_v5
g_v5
g_v5->h_v2
t₃₁
τ = 1+X₀ ≤ X₃ ∧ X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
g_v6
g_v6
g_v6->h_v2
t₃₃
τ = X₀ ≤ X₃ ∧ X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
h_v1->g_v1
t₁₄
η (X₁) = 1+X₁
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
h_v1->g_v2
t₁₅
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
h_v1->g_v3
t₁₇
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v1->g_v4
t₁₈
η (X₀) = 1+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v1->g_v5
t₁₉
η (X₀) = 2+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v1->g_v6
t₂₀
η (X₀) = 3+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v3
t₂₄
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v4
t₂₅
η (X₀) = 1+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v5
t₂₆
η (X₀) = 2+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v6
t₂₇
η (X₀) = 3+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v3->g_v1
t₃₉
η (X₁) = 1+X₁
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
h_v3->g_v2
t₄₀
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
MPRF for transition t₂₆: h_v2(X₀,X₁,X₂,X₃) → g_v5(2+X₀,X₁,X₂,X₃) :|: 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁ of depth 1:
new bound:
8⋅X₀+8⋅X₃+17 {O(n)}
MPRF:
• g_v3: [X₃-2-X₀]
• g_v4: [X₃-1-X₀]
• g_v5: [X₃-2-X₀]
• g_v6: [X₃-X₀]
• h_v2: [X₃-2-X₀]
Show Graph
G
f
f
g
g
f->g
t₁
{0}
h_v1
h_v1
g->h_v1
t₁₂
τ = 3+X₀ ≤ X₃
{0}
g_v1
g_v1
g_v1->h_v1
t₃₅
τ = X₁ ≤ X₂ ∧ 3+X₀ ≤ X₃
{0}
g_v2
g_v2
h_v3
h_v3
g_v2->h_v3
t₃₇
τ = 1+X₁ ≤ X₂ ∧ 3+X₀ ≤ X₃
{0}
g_v3
g_v3
h_v2
h_v2
g_v3->h_v2
t₂₂
τ = X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
g_v4
g_v4
g_v4->h_v2
t₂₉
τ = 2+X₀ ≤ X₃ ∧ X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
g_v5
g_v5
g_v5->h_v2
t₃₁
τ = 1+X₀ ≤ X₃ ∧ X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
g_v6
g_v6
g_v6->h_v2
t₃₃
τ = X₀ ≤ X₃ ∧ X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
h_v1->g_v1
t₁₄
η (X₁) = 1+X₁
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
h_v1->g_v2
t₁₅
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
h_v1->g_v3
t₁₇
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v1->g_v4
t₁₈
η (X₀) = 1+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v1->g_v5
t₁₉
η (X₀) = 2+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v1->g_v6
t₂₀
η (X₀) = 3+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v3
t₂₄
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v4
t₂₅
η (X₀) = 1+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v5
t₂₆
η (X₀) = 2+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v6
t₂₇
η (X₀) = 3+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v3->g_v1
t₃₉
η (X₁) = 1+X₁
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
h_v3->g_v2
t₄₀
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
MPRF for transition t₂₇: h_v2(X₀,X₁,X₂,X₃) → g_v6(3+X₀,X₁,X₂,X₃) :|: 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁ of depth 1:
new bound:
8⋅X₀+8⋅X₃+17 {O(n)}
MPRF:
• g_v3: [X₃-2-X₀]
• g_v4: [X₃-1-X₀]
• g_v5: [X₃-X₀]
• g_v6: [X₃-2-X₀]
• h_v2: [X₃-2-X₀]
Show Graph
G
f
f
g
g
f->g
t₁
{0}
h_v1
h_v1
g->h_v1
t₁₂
τ = 3+X₀ ≤ X₃
{0}
g_v1
g_v1
g_v1->h_v1
t₃₅
τ = X₁ ≤ X₂ ∧ 3+X₀ ≤ X₃
{0}
g_v2
g_v2
h_v3
h_v3
g_v2->h_v3
t₃₇
τ = 1+X₁ ≤ X₂ ∧ 3+X₀ ≤ X₃
{0}
g_v3
g_v3
h_v2
h_v2
g_v3->h_v2
t₂₂
τ = X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
g_v4
g_v4
g_v4->h_v2
t₂₉
τ = 2+X₀ ≤ X₃ ∧ X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
g_v5
g_v5
g_v5->h_v2
t₃₁
τ = 1+X₀ ≤ X₃ ∧ X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
g_v6
g_v6
g_v6->h_v2
t₃₃
τ = X₀ ≤ X₃ ∧ X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
h_v1->g_v1
t₁₄
η (X₁) = 1+X₁
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
h_v1->g_v2
t₁₅
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
h_v1->g_v3
t₁₇
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v1->g_v4
t₁₈
η (X₀) = 1+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v1->g_v5
t₁₉
η (X₀) = 2+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v1->g_v6
t₂₀
η (X₀) = 3+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v3
t₂₄
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v4
t₂₅
η (X₀) = 1+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v5
t₂₆
η (X₀) = 2+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v6
t₂₇
η (X₀) = 3+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v3->g_v1
t₃₉
η (X₁) = 1+X₁
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
h_v3->g_v2
t₄₀
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
MPRF for transition t₂₉: g_v4(X₀,X₁,X₂,X₃) -{0}> h_v2(X₀,X₁,X₂,X₃) :|: 2+X₀ ≤ X₃ ∧ X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃ of depth 1:
new bound:
8⋅X₀+8⋅X₃+15 {O(n)}
MPRF:
• g_v3: [X₃-2-X₀]
• g_v4: [X₃-1-X₀]
• g_v5: [X₃-X₀]
• g_v6: [X₃-X₀]
• h_v2: [X₃-2-X₀]
Show Graph
G
f
f
g
g
f->g
t₁
{0}
h_v1
h_v1
g->h_v1
t₁₂
τ = 3+X₀ ≤ X₃
{0}
g_v1
g_v1
g_v1->h_v1
t₃₅
τ = X₁ ≤ X₂ ∧ 3+X₀ ≤ X₃
{0}
g_v2
g_v2
h_v3
h_v3
g_v2->h_v3
t₃₇
τ = 1+X₁ ≤ X₂ ∧ 3+X₀ ≤ X₃
{0}
g_v3
g_v3
h_v2
h_v2
g_v3->h_v2
t₂₂
τ = X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
g_v4
g_v4
g_v4->h_v2
t₂₉
τ = 2+X₀ ≤ X₃ ∧ X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
g_v5
g_v5
g_v5->h_v2
t₃₁
τ = 1+X₀ ≤ X₃ ∧ X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
g_v6
g_v6
g_v6->h_v2
t₃₃
τ = X₀ ≤ X₃ ∧ X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
h_v1->g_v1
t₁₄
η (X₁) = 1+X₁
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
h_v1->g_v2
t₁₅
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
h_v1->g_v3
t₁₇
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v1->g_v4
t₁₈
η (X₀) = 1+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v1->g_v5
t₁₉
η (X₀) = 2+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v1->g_v6
t₂₀
η (X₀) = 3+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v3
t₂₄
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v4
t₂₅
η (X₀) = 1+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v5
t₂₆
η (X₀) = 2+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v6
t₂₇
η (X₀) = 3+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v3->g_v1
t₃₉
η (X₁) = 1+X₁
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
h_v3->g_v2
t₄₀
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
MPRF for transition t₃₁: g_v5(X₀,X₁,X₂,X₃) -{0}> h_v2(X₀,X₁,X₂,X₃) :|: 1+X₀ ≤ X₃ ∧ X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃ of depth 1:
new bound:
8⋅X₀+8⋅X₃+18 {O(n)}
MPRF:
• g_v3: [X₃-3-X₀]
• g_v4: [X₃-2-X₀]
• g_v5: [X₃-1-X₀]
• g_v6: [X₃-X₀]
• h_v2: [X₃-3-X₀]
Show Graph
G
f
f
g
g
f->g
t₁
{0}
h_v1
h_v1
g->h_v1
t₁₂
τ = 3+X₀ ≤ X₃
{0}
g_v1
g_v1
g_v1->h_v1
t₃₅
τ = X₁ ≤ X₂ ∧ 3+X₀ ≤ X₃
{0}
g_v2
g_v2
h_v3
h_v3
g_v2->h_v3
t₃₇
τ = 1+X₁ ≤ X₂ ∧ 3+X₀ ≤ X₃
{0}
g_v3
g_v3
h_v2
h_v2
g_v3->h_v2
t₂₂
τ = X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
g_v4
g_v4
g_v4->h_v2
t₂₉
τ = 2+X₀ ≤ X₃ ∧ X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
g_v5
g_v5
g_v5->h_v2
t₃₁
τ = 1+X₀ ≤ X₃ ∧ X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
g_v6
g_v6
g_v6->h_v2
t₃₃
τ = X₀ ≤ X₃ ∧ X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
h_v1->g_v1
t₁₄
η (X₁) = 1+X₁
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
h_v1->g_v2
t₁₅
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
h_v1->g_v3
t₁₇
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v1->g_v4
t₁₈
η (X₀) = 1+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v1->g_v5
t₁₉
η (X₀) = 2+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v1->g_v6
t₂₀
η (X₀) = 3+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v3
t₂₄
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v4
t₂₅
η (X₀) = 1+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v5
t₂₆
η (X₀) = 2+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v6
t₂₇
η (X₀) = 3+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v3->g_v1
t₃₉
η (X₁) = 1+X₁
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
h_v3->g_v2
t₄₀
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
MPRF for transition t₃₃: g_v6(X₀,X₁,X₂,X₃) -{0}> h_v2(X₀,X₁,X₂,X₃) :|: X₀ ≤ X₃ ∧ X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃ of depth 1:
new bound:
8⋅X₀+8⋅X₃+13 {O(n)}
MPRF:
• g_v3: [X₃-X₀]
• g_v4: [X₃-X₀]
• g_v5: [X₃-X₀]
• g_v6: [1+X₃-X₀]
• h_v2: [X₃-X₀]
Show Graph
G
f
f
g
g
f->g
t₁
{0}
h_v1
h_v1
g->h_v1
t₁₂
τ = 3+X₀ ≤ X₃
{0}
g_v1
g_v1
g_v1->h_v1
t₃₅
τ = X₁ ≤ X₂ ∧ 3+X₀ ≤ X₃
{0}
g_v2
g_v2
h_v3
h_v3
g_v2->h_v3
t₃₇
τ = 1+X₁ ≤ X₂ ∧ 3+X₀ ≤ X₃
{0}
g_v3
g_v3
h_v2
h_v2
g_v3->h_v2
t₂₂
τ = X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
g_v4
g_v4
g_v4->h_v2
t₂₉
τ = 2+X₀ ≤ X₃ ∧ X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
g_v5
g_v5
g_v5->h_v2
t₃₁
τ = 1+X₀ ≤ X₃ ∧ X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
g_v6
g_v6
g_v6->h_v2
t₃₃
τ = X₀ ≤ X₃ ∧ X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
h_v1->g_v1
t₁₄
η (X₁) = 1+X₁
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
h_v1->g_v2
t₁₅
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
h_v1->g_v3
t₁₇
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v1->g_v4
t₁₈
η (X₀) = 1+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v1->g_v5
t₁₉
η (X₀) = 2+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v1->g_v6
t₂₀
η (X₀) = 3+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v3
t₂₄
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v4
t₂₅
η (X₀) = 1+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v5
t₂₆
η (X₀) = 2+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v6
t₂₇
η (X₀) = 3+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v3->g_v1
t₃₉
η (X₁) = 1+X₁
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
h_v3->g_v2
t₄₀
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
Classical Approximation after Lifting Classical Results
All Bounds
Timebounds
Overall timebound:inf {Infinity}
g₀: 1 {O(1)}
g₁₃: 1 {O(1)}
g₁₆: 2⋅X₁+2⋅X₂+1 {O(n)}
g₂₁: 4 {O(1)}
g₂₃: inf {Infinity}
g₂₈: inf {Infinity}
g₃₀: 8⋅X₀+8⋅X₃+15 {O(n)}
g₃₂: 8⋅X₀+8⋅X₃+18 {O(n)}
g₃₄: 8⋅X₀+8⋅X₃+13 {O(n)}
g₃₆: X₁+X₂ {O(n)}
g₃₈: X₁+X₂ {O(n)}
g₄₁: X₁+X₂ {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}
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₁₃,h_v1), X₀: X₀ {O(n)}
(g₁₃,h_v1), X₁: X₁ {O(n)}
(g₁₃,h_v1), X₂: X₂ {O(n)}
(g₁₃,h_v1), X₃: X₃ {O(n)}
(g₁₆,g_v1), X₀: X₀ {O(n)}
(g₁₆,g_v1), X₁: 4⋅X₂+6⋅X₁ {O(n)}
(g₁₆,g_v1), X₂: X₂ {O(n)}
(g₁₆,g_v1), X₃: X₃ {O(n)}
(g₁₆,g_v2), X₀: X₀ {O(n)}
(g₁₆,g_v2), X₁: 4⋅X₂+6⋅X₁ {O(n)}
(g₁₆,g_v2), X₂: X₂ {O(n)}
(g₁₆,g_v2), X₃: X₃ {O(n)}
(g₂₁,g_v3), X₀: 2⋅X₀ {O(n)}
(g₂₁,g_v3), X₁: 2⋅X₂+4⋅X₁ {O(n)}
(g₂₁,g_v3), X₂: 8⋅X₂ {O(n)}
(g₂₁,g_v3), X₃: 8⋅X₃ {O(n)}
(g₂₁,g_v4), X₀: 8⋅X₀+12 {O(n)}
(g₂₁,g_v4), X₁: 2⋅X₂+4⋅X₁ {O(n)}
(g₂₁,g_v4), X₂: 8⋅X₂ {O(n)}
(g₂₁,g_v4), X₃: 8⋅X₃ {O(n)}
(g₂₁,g_v5), X₀: 8⋅X₀+12 {O(n)}
(g₂₁,g_v5), X₁: 2⋅X₂+4⋅X₁ {O(n)}
(g₂₁,g_v5), X₂: 8⋅X₂ {O(n)}
(g₂₁,g_v5), X₃: 8⋅X₃ {O(n)}
(g₂₁,g_v6), X₀: 8⋅X₀+12 {O(n)}
(g₂₁,g_v6), X₁: 2⋅X₂+4⋅X₁ {O(n)}
(g₂₁,g_v6), X₂: 8⋅X₂ {O(n)}
(g₂₁,g_v6), X₃: 8⋅X₃ {O(n)}
(g₂₃,h_v2), X₀: 48⋅X₃+56⋅X₀+113 {O(n)}
(g₂₃,h_v2), X₁: 16⋅X₁+8⋅X₂ {O(n)}
(g₂₃,h_v2), X₂: 8⋅X₂ {O(n)}
(g₂₃,h_v2), X₃: 8⋅X₃ {O(n)}
(g₂₈,g_v3), X₀: 192⋅X₃+224⋅X₀+452 {O(n)}
(g₂₈,g_v3), X₁: 32⋅X₂+64⋅X₁ {O(n)}
(g₂₈,g_v3), X₂: 32⋅X₂ {O(n)}
(g₂₈,g_v3), X₃: 32⋅X₃ {O(n)}
(g₂₈,g_v4), X₀: 192⋅X₃+224⋅X₀+452 {O(n)}
(g₂₈,g_v4), X₁: 32⋅X₂+64⋅X₁ {O(n)}
(g₂₈,g_v4), X₂: 32⋅X₂ {O(n)}
(g₂₈,g_v4), X₃: 32⋅X₃ {O(n)}
(g₂₈,g_v5), X₀: 192⋅X₃+224⋅X₀+452 {O(n)}
(g₂₈,g_v5), X₁: 32⋅X₂+64⋅X₁ {O(n)}
(g₂₈,g_v5), X₂: 32⋅X₂ {O(n)}
(g₂₈,g_v5), X₃: 32⋅X₃ {O(n)}
(g₂₈,g_v6), X₀: 192⋅X₃+224⋅X₀+452 {O(n)}
(g₂₈,g_v6), X₁: 32⋅X₂+64⋅X₁ {O(n)}
(g₂₈,g_v6), X₂: 32⋅X₂ {O(n)}
(g₂₈,g_v6), X₃: 32⋅X₃ {O(n)}
(g₃₀,h_v2), X₀: 48⋅X₃+56⋅X₀+113 {O(n)}
(g₃₀,h_v2), X₁: 16⋅X₁+8⋅X₂ {O(n)}
(g₃₀,h_v2), X₂: 8⋅X₂ {O(n)}
(g₃₀,h_v2), X₃: 8⋅X₃ {O(n)}
(g₃₂,h_v2), X₀: 48⋅X₃+56⋅X₀+113 {O(n)}
(g₃₂,h_v2), X₁: 16⋅X₁+8⋅X₂ {O(n)}
(g₃₂,h_v2), X₂: 8⋅X₂ {O(n)}
(g₃₂,h_v2), X₃: 8⋅X₃ {O(n)}
(g₃₄,h_v2), X₀: 48⋅X₃+56⋅X₀+113 {O(n)}
(g₃₄,h_v2), X₁: 16⋅X₁+8⋅X₂ {O(n)}
(g₃₄,h_v2), X₂: 8⋅X₂ {O(n)}
(g₃₄,h_v2), X₃: 8⋅X₃ {O(n)}
(g₃₆,h_v1), X₀: X₀ {O(n)}
(g₃₆,h_v1), X₁: 2⋅X₂+3⋅X₁ {O(n)}
(g₃₆,h_v1), X₂: X₂ {O(n)}
(g₃₆,h_v1), X₃: X₃ {O(n)}
(g₃₈,h_v3), X₀: X₀ {O(n)}
(g₃₈,h_v3), X₁: 2⋅X₂+3⋅X₁ {O(n)}
(g₃₈,h_v3), X₂: X₂ {O(n)}
(g₃₈,h_v3), X₃: X₃ {O(n)}
(g₄₁,g_v1), X₀: X₀ {O(n)}
(g₄₁,g_v1), X₁: 4⋅X₂+6⋅X₁ {O(n)}
(g₄₁,g_v1), X₂: X₂ {O(n)}
(g₄₁,g_v1), X₃: X₃ {O(n)}
(g₄₁,g_v2), X₀: X₀ {O(n)}
(g₄₁,g_v2), X₁: 4⋅X₂+6⋅X₁ {O(n)}
(g₄₁,g_v2), X₂: X₂ {O(n)}
(g₄₁,g_v2), X₃: X₃ {O(n)}
Run probabilistic analysis on SCC: [g_v3; g_v4; g_v5; g_v6; h_v2]
Plrf for transition g₂₃:g_v3(X₀,X₁,X₂,X₃) -{0}> t₂₂:h_v2(X₀,X₁,X₂,X₃) :|: 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁:
new bound:
13/3⋅X₀+16/3⋅X₃+7 {O(n)}
PLRF:
• g_v3: 1+1/6⋅X₃-1/6⋅X₀
• g_v4: 1/6⋅X₃-1/6⋅X₀
• g_v5: 1/6⋅X₃-1/6⋅X₀
• g_v6: 1/6⋅X₃-1/6⋅X₀
• h_v2: 1/6⋅X₃-1/6⋅X₀
Show Graph
G
f
f
g
g
f->g
p = 1
t₁ ∈ g₀
{0}
h_v1
h_v1
g->h_v1
p = 1
t₁₂ ∈ g₁₃
τ = 3+X₀ ≤ X₃
{0}
g_v1
g_v1
g_v1->h_v1
p = 1
t₃₅ ∈ g₃₆
τ = X₁ ≤ X₂ ∧ 3+X₀ ≤ X₃
{0}
g_v2
g_v2
h_v3
h_v3
g_v2->h_v3
p = 1
t₃₇ ∈ g₃₈
τ = 1+X₁ ≤ X₂ ∧ 3+X₀ ≤ X₃
{0}
g_v3
g_v3
h_v2
h_v2
g_v3->h_v2
p = 1
t₂₂ ∈ g₂₃
τ = X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
g_v4
g_v4
g_v4->h_v2
p = 1
t₂₉ ∈ g₃₀
τ = 2+X₀ ≤ X₃ ∧ X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
g_v5
g_v5
g_v5->h_v2
p = 1
t₃₁ ∈ g₃₂
τ = 1+X₀ ≤ X₃ ∧ X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
g_v6
g_v6
g_v6->h_v2
p = 1
t₃₃ ∈ g₃₄
τ = X₀ ≤ X₃ ∧ X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
h_v1->g_v1
p = 1/2
t₁₄ ∈ g₁₆
η (X₁) = 1+X₁
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
h_v1->g_v2
p = 1/2
t₁₅ ∈ g₁₆
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
h_v1->g_v3
p = 1/4
t₁₇ ∈ g₂₁
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v1->g_v4
p = 1/4
t₁₈ ∈ g₂₁
η (X₀) = 1+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v1->g_v5
p = 1/4
t₁₉ ∈ g₂₁
η (X₀) = 2+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v1->g_v6
p = 1/4
t₂₀ ∈ g₂₁
η (X₀) = 3+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v3
p = 1/4
t₂₄ ∈ g₂₈
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v4
p = 1/4
t₂₅ ∈ g₂₈
η (X₀) = 1+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v5
p = 1/4
t₂₆ ∈ g₂₈
η (X₀) = 2+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v6
p = 1/4
t₂₇ ∈ g₂₈
η (X₀) = 3+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v3->g_v1
p = 1/2
t₃₉ ∈ g₄₁
η (X₁) = 1+X₁
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
h_v3->g_v2
p = 1/2
t₄₀ ∈ g₄₁
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
Use expected size bounds for entry point (g₂₁:h_v1→[t₁₇:1/4:g_v3; t₁₈:1/4:g_v4; t₁₉:1/4:g_v5; t₂₀:1/4:g_v6],g_v3)
Use expected size bounds for entry point (g₂₁:h_v1→[t₁₇:1/4:g_v3; t₁₈:1/4:g_v4; t₁₉:1/4:g_v5; t₂₀:1/4:g_v6],g_v3)
Use classical time bound for entry point (g₂₁:h_v1→[t₁₇:1/4:g_v3; t₁₈:1/4:g_v4; t₁₉:1/4:g_v5; t₂₀:1/4:g_v6],g_v3)
Use expected size bounds for entry point (g₂₁:h_v1→[t₁₇:1/4:g_v3; t₁₈:1/4:g_v4; t₁₉:1/4:g_v5; t₂₀:1/4:g_v6],g_v4)
Use expected size bounds for entry point (g₂₁:h_v1→[t₁₇:1/4:g_v3; t₁₈:1/4:g_v4; t₁₉:1/4:g_v5; t₂₀:1/4:g_v6],g_v4)
Use classical time bound for entry point (g₂₁:h_v1→[t₁₇:1/4:g_v3; t₁₈:1/4:g_v4; t₁₉:1/4:g_v5; t₂₀:1/4:g_v6],g_v4)
Use expected size bounds for entry point (g₂₁:h_v1→[t₁₇:1/4:g_v3; t₁₈:1/4:g_v4; t₁₉:1/4:g_v5; t₂₀:1/4:g_v6],g_v5)
Use expected size bounds for entry point (g₂₁:h_v1→[t₁₇:1/4:g_v3; t₁₈:1/4:g_v4; t₁₉:1/4:g_v5; t₂₀:1/4:g_v6],g_v5)
Use classical time bound for entry point (g₂₁:h_v1→[t₁₇:1/4:g_v3; t₁₈:1/4:g_v4; t₁₉:1/4:g_v5; t₂₀:1/4:g_v6],g_v5)
Use expected size bounds for entry point (g₂₁:h_v1→[t₁₇:1/4:g_v3; t₁₈:1/4:g_v4; t₁₉:1/4:g_v5; t₂₀:1/4:g_v6],g_v6)
Use expected size bounds for entry point (g₂₁:h_v1→[t₁₇:1/4:g_v3; t₁₈:1/4:g_v4; t₁₉:1/4:g_v5; t₂₀:1/4:g_v6],g_v6)
Use classical time bound for entry point (g₂₁:h_v1→[t₁₇:1/4:g_v3; t₁₈:1/4:g_v4; t₁₉:1/4:g_v5; t₂₀:1/4:g_v6],g_v6)
Plrf for transition g₂₈:h_v2(X₀,X₁,X₂,X₃) → [1/4]:t₂₄:g_v3(X₀,X₁,X₂,X₃) :+: [1/4]:t₂₅:g_v4(1+X₀,X₁,X₂,X₃) :+: [1/4]:t₂₆:g_v5(2+X₀,X₁,X₂,X₃) :+: [1/4]:t₂₇:g_v6(3+X₀,X₁,X₂,X₃) :|: X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃:
new bound:
52/3⋅X₀+64/3⋅X₃+24 {O(n)}
PLRF:
• g_v3: 2/3⋅X₃-2/3⋅X₀
• g_v4: 2/3⋅X₃-2/3⋅X₀
• g_v5: 2/3⋅X₃-2/3⋅X₀
• g_v6: 2/3⋅X₃-2/3⋅X₀
• h_v2: 2/3⋅X₃-2/3⋅X₀
Show Graph
G
f
f
g
g
f->g
p = 1
t₁ ∈ g₀
{0}
h_v1
h_v1
g->h_v1
p = 1
t₁₂ ∈ g₁₃
τ = 3+X₀ ≤ X₃
{0}
g_v1
g_v1
g_v1->h_v1
p = 1
t₃₅ ∈ g₃₆
τ = X₁ ≤ X₂ ∧ 3+X₀ ≤ X₃
{0}
g_v2
g_v2
h_v3
h_v3
g_v2->h_v3
p = 1
t₃₇ ∈ g₃₈
τ = 1+X₁ ≤ X₂ ∧ 3+X₀ ≤ X₃
{0}
g_v3
g_v3
h_v2
h_v2
g_v3->h_v2
p = 1
t₂₂ ∈ g₂₃
τ = X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
g_v4
g_v4
g_v4->h_v2
p = 1
t₂₉ ∈ g₃₀
τ = 2+X₀ ≤ X₃ ∧ X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
g_v5
g_v5
g_v5->h_v2
p = 1
t₃₁ ∈ g₃₂
τ = 1+X₀ ≤ X₃ ∧ X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
g_v6
g_v6
g_v6->h_v2
p = 1
t₃₃ ∈ g₃₄
τ = X₀ ≤ X₃ ∧ X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
h_v1->g_v1
p = 1/2
t₁₄ ∈ g₁₆
η (X₁) = 1+X₁
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
h_v1->g_v2
p = 1/2
t₁₅ ∈ g₁₆
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
h_v1->g_v3
p = 1/4
t₁₇ ∈ g₂₁
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v1->g_v4
p = 1/4
t₁₈ ∈ g₂₁
η (X₀) = 1+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v1->g_v5
p = 1/4
t₁₉ ∈ g₂₁
η (X₀) = 2+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v1->g_v6
p = 1/4
t₂₀ ∈ g₂₁
η (X₀) = 3+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v3
p = 1/4
t₂₄ ∈ g₂₈
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v4
p = 1/4
t₂₅ ∈ g₂₈
η (X₀) = 1+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v5
p = 1/4
t₂₆ ∈ g₂₈
η (X₀) = 2+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v6
p = 1/4
t₂₇ ∈ g₂₈
η (X₀) = 3+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v3->g_v1
p = 1/2
t₃₉ ∈ g₄₁
η (X₁) = 1+X₁
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
h_v3->g_v2
p = 1/2
t₄₀ ∈ g₄₁
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
Use expected size bounds for entry point (g₂₁:h_v1→[t₁₇:1/4:g_v3; t₁₈:1/4:g_v4; t₁₉:1/4:g_v5; t₂₀:1/4:g_v6],g_v3)
Use expected size bounds for entry point (g₂₁:h_v1→[t₁₇:1/4:g_v3; t₁₈:1/4:g_v4; t₁₉:1/4:g_v5; t₂₀:1/4:g_v6],g_v3)
Use classical time bound for entry point (g₂₁:h_v1→[t₁₇:1/4:g_v3; t₁₈:1/4:g_v4; t₁₉:1/4:g_v5; t₂₀:1/4:g_v6],g_v3)
Use expected size bounds for entry point (g₂₁:h_v1→[t₁₇:1/4:g_v3; t₁₈:1/4:g_v4; t₁₉:1/4:g_v5; t₂₀:1/4:g_v6],g_v4)
Use expected size bounds for entry point (g₂₁:h_v1→[t₁₇:1/4:g_v3; t₁₈:1/4:g_v4; t₁₉:1/4:g_v5; t₂₀:1/4:g_v6],g_v4)
Use classical time bound for entry point (g₂₁:h_v1→[t₁₇:1/4:g_v3; t₁₈:1/4:g_v4; t₁₉:1/4:g_v5; t₂₀:1/4:g_v6],g_v4)
Use expected size bounds for entry point (g₂₁:h_v1→[t₁₇:1/4:g_v3; t₁₈:1/4:g_v4; t₁₉:1/4:g_v5; t₂₀:1/4:g_v6],g_v5)
Use expected size bounds for entry point (g₂₁:h_v1→[t₁₇:1/4:g_v3; t₁₈:1/4:g_v4; t₁₉:1/4:g_v5; t₂₀:1/4:g_v6],g_v5)
Use classical time bound for entry point (g₂₁:h_v1→[t₁₇:1/4:g_v3; t₁₈:1/4:g_v4; t₁₉:1/4:g_v5; t₂₀:1/4:g_v6],g_v5)
Use expected size bounds for entry point (g₂₁:h_v1→[t₁₇:1/4:g_v3; t₁₈:1/4:g_v4; t₁₉:1/4:g_v5; t₂₀:1/4:g_v6],g_v6)
Use expected size bounds for entry point (g₂₁:h_v1→[t₁₇:1/4:g_v3; t₁₈:1/4:g_v4; t₁₉:1/4:g_v5; t₂₀:1/4:g_v6],g_v6)
Use classical time bound for entry point (g₂₁:h_v1→[t₁₇:1/4:g_v3; t₁₈:1/4:g_v4; t₁₉:1/4:g_v5; t₂₀:1/4:g_v6],g_v6)
CFR: Improvement to new bound with the following program:
method: PartialEvaluationProbabilistic new bound:
O(n)
cfr-program:
Start: f
Program_Vars: X₀, X₁, X₂, X₃
Temp_Vars:
Locations: f, g, g_v1, g_v2, g_v3, g_v4, g_v5, g_v6, h_v1, h_v2, h_v3
Transitions:
g₀:f(X₀,X₁,X₂,X₃) -{0}> t₁:g(X₀,X₁,X₂,X₃) :|:
g₁₃:g(X₀,X₁,X₂,X₃) -{0}> t₁₂:h_v1(X₀,X₁,X₂,X₃) :|: 3+X₀ ≤ X₃
g₁₆:h_v1(X₀,X₁,X₂,X₃) → [1/2]:t₁₄:g_v1(X₀,1+X₁,X₂,X₃) :+: [1/2]:t₁₅:g_v2(X₀,X₁,X₂,X₃) :|: 1+X₁ ≤ X₂ ∧ 3+X₀ ≤ X₃
g₂₁:h_v1(X₀,X₁,X₂,X₃) → [1/4]:t₁₇:g_v3(X₀,X₁,X₂,X₃) :+: [1/4]:t₁₈:g_v4(1+X₀,X₁,X₂,X₃) :+: [1/4]:t₁₉:g_v5(2+X₀,X₁,X₂,X₃) :+: [1/4]:t₂₀:g_v6(3+X₀,X₁,X₂,X₃) :|: X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
g₂₃:g_v3(X₀,X₁,X₂,X₃) -{0}> t₂₂:h_v2(X₀,X₁,X₂,X₃) :|: 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
g₂₈:h_v2(X₀,X₁,X₂,X₃) → [1/4]:t₂₄:g_v3(X₀,X₁,X₂,X₃) :+: [1/4]:t₂₅:g_v4(1+X₀,X₁,X₂,X₃) :+: [1/4]:t₂₆:g_v5(2+X₀,X₁,X₂,X₃) :+: [1/4]:t₂₇:g_v6(3+X₀,X₁,X₂,X₃) :|: X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
g₃₀:g_v4(X₀,X₁,X₂,X₃) -{0}> t₂₉:h_v2(X₀,X₁,X₂,X₃) :|: 3+X₀ ≤ X₃ ∧ 2+X₀ ≤ X₃ ∧ X₂ ≤ X₁
g₃₂:g_v5(X₀,X₁,X₂,X₃) -{0}> t₃₁:h_v2(X₀,X₁,X₂,X₃) :|: 3+X₀ ≤ X₃ ∧ 1+X₀ ≤ X₃ ∧ X₂ ≤ X₁
g₃₄:g_v6(X₀,X₁,X₂,X₃) -{0}> t₃₃:h_v2(X₀,X₁,X₂,X₃) :|: 3+X₀ ≤ X₃ ∧ X₀ ≤ X₃ ∧ X₂ ≤ X₁
g₃₆:g_v1(X₀,X₁,X₂,X₃) -{0}> t₃₅:h_v1(X₀,X₁,X₂,X₃) :|: 3+X₀ ≤ X₃ ∧ X₁ ≤ X₂
g₃₈:g_v2(X₀,X₁,X₂,X₃) -{0}> t₃₇:h_v3(X₀,X₁,X₂,X₃) :|: 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
g₄₁:h_v3(X₀,X₁,X₂,X₃) → [1/2]:t₃₉:g_v1(X₀,1+X₁,X₂,X₃) :+: [1/2]:t₄₀:g_v2(X₀,X₁,X₂,X₃) :|: 1+X₁ ≤ X₂ ∧ 3+X₀ ≤ X₃
Show Graph
G
f
f
g
g
f->g
t₁ ∈ g₀
{0}
h_v1
h_v1
g->h_v1
t₁₂ ∈ g₁₃
τ = 3+X₀ ≤ X₃
{0}
g_v1
g_v1
g_v1->h_v1
t₃₅ ∈ g₃₆
τ = X₁ ≤ X₂ ∧ 3+X₀ ≤ X₃
{0}
g_v2
g_v2
h_v3
h_v3
g_v2->h_v3
t₃₇ ∈ g₃₈
τ = 1+X₁ ≤ X₂ ∧ 3+X₀ ≤ X₃
{0}
g_v3
g_v3
h_v2
h_v2
g_v3->h_v2
t₂₂ ∈ g₂₃
τ = X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
g_v4
g_v4
g_v4->h_v2
t₂₉ ∈ g₃₀
τ = 2+X₀ ≤ X₃ ∧ X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
g_v5
g_v5
g_v5->h_v2
t₃₁ ∈ g₃₂
τ = 1+X₀ ≤ X₃ ∧ X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
g_v6
g_v6
g_v6->h_v2
t₃₃ ∈ g₃₄
τ = X₀ ≤ X₃ ∧ X₂ ≤ X₁ ∧ 3+X₀ ≤ X₃
{0}
h_v1->g_v1
t₁₄ ∈ g₁₆
η (X₁) = 1+X₁
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
h_v1->g_v2
t₁₅ ∈ g₁₆
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
h_v1->g_v3
t₁₇ ∈ g₂₁
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v1->g_v4
t₁₈ ∈ g₂₁
η (X₀) = 1+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v1->g_v5
t₁₉ ∈ g₂₁
η (X₀) = 2+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v1->g_v6
t₂₀ ∈ g₂₁
η (X₀) = 3+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v3
t₂₄ ∈ g₂₈
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v4
t₂₅ ∈ g₂₈
η (X₀) = 1+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v5
t₂₆ ∈ g₂₈
η (X₀) = 2+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v2->g_v6
t₂₇ ∈ g₂₈
η (X₀) = 3+X₀
τ = 3+X₀ ≤ X₃ ∧ X₂ ≤ X₁
h_v3->g_v1
t₃₉ ∈ g₄₁
η (X₁) = 1+X₁
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
h_v3->g_v2
t₄₀ ∈ g₄₁
τ = 3+X₀ ≤ X₃ ∧ 1+X₁ ≤ X₂
Results of Probabilistic Analysis
All Bounds
Timebounds
Overall timebound:137/3⋅X₀+152/3⋅X₃+5⋅X₁+5⋅X₂+84 {O(n)}
g₀: 1 {O(1)}
g₁₃: 1 {O(1)}
g₁₆: 2⋅X₁+2⋅X₂+1 {O(n)}
g₂₁: 4 {O(1)}
g₂₃: 13/3⋅X₀+16/3⋅X₃+7 {O(n)}
g₂₈: 52/3⋅X₀+64/3⋅X₃+24 {O(n)}
g₃₀: 8⋅X₀+8⋅X₃+15 {O(n)}
g₃₂: 8⋅X₀+8⋅X₃+18 {O(n)}
g₃₄: 8⋅X₀+8⋅X₃+13 {O(n)}
g₃₆: X₁+X₂ {O(n)}
g₃₈: X₁+X₂ {O(n)}
g₄₁: X₁+X₂ {O(n)}
Costbounds
Overall costbound: 208/3⋅X₀+256/3⋅X₃+6⋅X₁+6⋅X₂+114 {O(n)}
g₀: 0 {O(1)}
g₁₃: 0 {O(1)}
g₁₆: 4⋅X₁+4⋅X₂+2 {O(n)}
g₂₁: 16 {O(1)}
g₂₃: 0 {O(1)}
g₂₈: 208/3⋅X₀+256/3⋅X₃+96 {O(n)}
g₃₀: 0 {O(1)}
g₃₂: 0 {O(1)}
g₃₄: 0 {O(1)}
g₃₆: 0 {O(1)}
g₃₈: 0 {O(1)}
g₄₁: 2⋅X₁+2⋅X₂ {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₁₃,h_v1), X₀: X₀ {O(n)}
(g₁₃,h_v1), X₁: X₁ {O(n)}
(g₁₃,h_v1), X₂: X₂ {O(n)}
(g₁₃,h_v1), X₃: X₃ {O(n)}
(g₁₆,g_v1), X₀: X₀ {O(n)}
(g₁₆,g_v1), X₁: 4⋅X₂+6⋅X₁ {O(n)}
(g₁₆,g_v1), X₂: X₂ {O(n)}
(g₁₆,g_v1), X₃: X₃ {O(n)}
(g₁₆,g_v2), X₀: X₀ {O(n)}
(g₁₆,g_v2), X₁: 4⋅X₂+6⋅X₁ {O(n)}
(g₁₆,g_v2), X₂: X₂ {O(n)}
(g₁₆,g_v2), X₃: X₃ {O(n)}
(g₂₁,g_v3), X₀: 2⋅X₀ {O(n)}
(g₂₁,g_v3), X₁: 2⋅X₂+4⋅X₁ {O(n)}
(g₂₁,g_v3), X₂: 8⋅X₂ {O(n)}
(g₂₁,g_v3), X₃: 8⋅X₃ {O(n)}
(g₂₁,g_v4), X₀: 8⋅X₀+12 {O(n)}
(g₂₁,g_v4), X₁: 2⋅X₂+4⋅X₁ {O(n)}
(g₂₁,g_v4), X₂: 8⋅X₂ {O(n)}
(g₂₁,g_v4), X₃: 8⋅X₃ {O(n)}
(g₂₁,g_v5), X₀: 8⋅X₀+12 {O(n)}
(g₂₁,g_v5), X₁: 2⋅X₂+4⋅X₁ {O(n)}
(g₂₁,g_v5), X₂: 8⋅X₂ {O(n)}
(g₂₁,g_v5), X₃: 8⋅X₃ {O(n)}
(g₂₁,g_v6), X₀: 8⋅X₀+12 {O(n)}
(g₂₁,g_v6), X₁: 2⋅X₂+4⋅X₁ {O(n)}
(g₂₁,g_v6), X₂: 8⋅X₂ {O(n)}
(g₂₁,g_v6), X₃: 8⋅X₃ {O(n)}
(g₂₃,h_v2), X₀: 32⋅X₃+52⋅X₀+72 {O(n)}
(g₂₃,h_v2), X₁: 16⋅X₁+8⋅X₂ {O(n)}
(g₂₃,h_v2), X₂: 8⋅X₂ {O(n)}
(g₂₃,h_v2), X₃: 8⋅X₃ {O(n)}
(g₂₈,g_v3), X₀: 32⋅X₃+52⋅X₀+72 {O(n)}
(g₂₈,g_v3), X₁: 16⋅X₁+8⋅X₂ {O(n)}
(g₂₈,g_v3), X₂: 32⋅X₂ {O(n)}
(g₂₈,g_v3), X₃: 32⋅X₃ {O(n)}
(g₂₈,g_v4), X₀: 32⋅X₃+52⋅X₀+72 {O(n)}
(g₂₈,g_v4), X₁: 16⋅X₁+8⋅X₂ {O(n)}
(g₂₈,g_v4), X₂: 32⋅X₂ {O(n)}
(g₂₈,g_v4), X₃: 32⋅X₃ {O(n)}
(g₂₈,g_v5), X₀: 32⋅X₃+52⋅X₀+72 {O(n)}
(g₂₈,g_v5), X₁: 16⋅X₁+8⋅X₂ {O(n)}
(g₂₈,g_v5), X₂: 32⋅X₂ {O(n)}
(g₂₈,g_v5), X₃: 32⋅X₃ {O(n)}
(g₂₈,g_v6), X₀: 32⋅X₃+52⋅X₀+72 {O(n)}
(g₂₈,g_v6), X₁: 16⋅X₁+8⋅X₂ {O(n)}
(g₂₈,g_v6), X₂: 32⋅X₂ {O(n)}
(g₂₈,g_v6), X₃: 32⋅X₃ {O(n)}
(g₃₀,h_v2), X₀: 32⋅X₃+52⋅X₀+72 {O(n)}
(g₃₀,h_v2), X₁: 16⋅X₁+8⋅X₂ {O(n)}
(g₃₀,h_v2), X₂: 8⋅X₂ {O(n)}
(g₃₀,h_v2), X₃: 8⋅X₃ {O(n)}
(g₃₂,h_v2), X₀: 32⋅X₃+52⋅X₀+72 {O(n)}
(g₃₂,h_v2), X₁: 16⋅X₁+8⋅X₂ {O(n)}
(g₃₂,h_v2), X₂: 8⋅X₂ {O(n)}
(g₃₂,h_v2), X₃: 8⋅X₃ {O(n)}
(g₃₄,h_v2), X₀: 32⋅X₃+52⋅X₀+72 {O(n)}
(g₃₄,h_v2), X₁: 16⋅X₁+8⋅X₂ {O(n)}
(g₃₄,h_v2), X₂: 8⋅X₂ {O(n)}
(g₃₄,h_v2), X₃: 8⋅X₃ {O(n)}
(g₃₆,h_v1), X₀: X₀ {O(n)}
(g₃₆,h_v1), X₁: 2⋅X₂+3⋅X₁ {O(n)}
(g₃₆,h_v1), X₂: X₂ {O(n)}
(g₃₆,h_v1), X₃: X₃ {O(n)}
(g₃₈,h_v3), X₀: X₀ {O(n)}
(g₃₈,h_v3), X₁: 2⋅X₂+3⋅X₁ {O(n)}
(g₃₈,h_v3), X₂: X₂ {O(n)}
(g₃₈,h_v3), X₃: X₃ {O(n)}
(g₄₁,g_v1), X₀: X₀ {O(n)}
(g₄₁,g_v1), X₁: 4⋅X₂+6⋅X₁ {O(n)}
(g₄₁,g_v1), X₂: X₂ {O(n)}
(g₄₁,g_v1), X₃: X₃ {O(n)}
(g₄₁,g_v2), X₀: X₀ {O(n)}
(g₄₁,g_v2), X₁: 4⋅X₂+6⋅X₁ {O(n)}
(g₄₁,g_v2), X₂: X₂ {O(n)}
(g₄₁,g_v2), X₃: X₃ {O(n)}