Preprocessing
Eliminate variables [X₀; X₁; X₂; X₃; X₄; X₅; X₆; X₇] that do not contribute to the problem
Found invariant X₉ ≤ 8 ∧ X₉ ≤ 7+X₈ ∧ 0 ≤ X₉ ∧ 1 ≤ X₈+X₉ ∧ 1 ≤ X₈ for location h
Probabilistic Analysis
Probabilistic Program after Preprocessing
Start: f
Program_Vars: X₀, X₁, X₂, X₃, X₄, X₅, X₆, X₇, X₈, X₉
Temp_Vars:
Locations: f, g, h
Transitions:
g₀:f(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,X₉) -{0}> t₁:g(0,0,0,0,0,0,0,0,X₈,X₉) :|:
g₂:g(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,X₉) -{0}> [1/10]:t₃:h(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,0) :+: [1/10]:t₄:h(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,1) :+: [1/10]:t₅:h(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,2) :+: [1/10]:t₆:h(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,3) :+: [1/10]:t₇:h(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,4) :+: [1/10]:t₈:h(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,5) :+: [1/10]:t₉:h(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,6) :+: [1/10]:t₁₀:h(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,7) :+: [1/5]:t₁₁:h(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,8) :|: 1 ≤ X₈
g₁₂:h(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,X₉) → t₁₃:g(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈-1,X₉) :|: 0 ≤ X₉ ∧ X₉ ≤ 0 ∧ X₉ ≤ 8 ∧ X₉ ≤ 7+X₈ ∧ 1 ≤ X₈ ∧ 1 ≤ X₈+X₉
g₁₄:h(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,X₉) → t₁₅:g(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈-2,X₉) :|: X₉ ≤ 1 ∧ 1 ≤ X₉ ∧ X₉ ≤ 8 ∧ X₉ ≤ 7+X₈ ∧ 1 ≤ X₈ ∧ 1 ≤ X₈+X₉ ∧ 0 ≤ X₉
g₁₆:h(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,X₉) → t₁₇:g(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈-3,X₉) :|: X₉ ≤ 2 ∧ 2 ≤ X₉ ∧ X₉ ≤ 8 ∧ X₉ ≤ 7+X₈ ∧ 1 ≤ X₈ ∧ 1 ≤ X₈+X₉ ∧ 0 ≤ X₉
g₁₈:h(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,X₉) → t₁₉:g(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈-4,X₉) :|: X₉ ≤ 3 ∧ 3 ≤ X₉ ∧ X₉ ≤ 8 ∧ X₉ ≤ 7+X₈ ∧ 1 ≤ X₈ ∧ 1 ≤ X₈+X₉ ∧ 0 ≤ X₉
g₂₀:h(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,X₉) → t₂₁:g(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈-5,X₉) :|: X₉ ≤ 4 ∧ 4 ≤ X₉ ∧ X₉ ≤ 8 ∧ X₉ ≤ 7+X₈ ∧ 1 ≤ X₈ ∧ 1 ≤ X₈+X₉ ∧ 0 ≤ X₉
g₂₂:h(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,X₉) → t₂₃:g(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈-6,X₉) :|: X₉ ≤ 5 ∧ 5 ≤ X₉ ∧ X₉ ≤ 8 ∧ X₉ ≤ 7+X₈ ∧ 1 ≤ X₈ ∧ 1 ≤ X₈+X₉ ∧ 0 ≤ X₉
g₂₄:h(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,X₉) → t₂₅:g(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈-7,X₉) :|: X₉ ≤ 6 ∧ 6 ≤ X₉ ∧ X₉ ≤ 8 ∧ X₉ ≤ 7+X₈ ∧ 1 ≤ X₈ ∧ 1 ≤ X₈+X₉ ∧ 0 ≤ X₉
g₂₆:h(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,X₉) → t₂₇:g(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈-8,X₉) :|: X₉ ≤ 7 ∧ 7 ≤ X₉ ∧ X₉ ≤ 8 ∧ X₉ ≤ 7+X₈ ∧ 1 ≤ X₈ ∧ 1 ≤ X₈+X₉ ∧ 0 ≤ X₉
g₂₈:h(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,X₉) → t₂₉:g(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,X₉) :|: X₉ ≤ 8 ∧ 8 ≤ X₉ ∧ X₉ ≤ 7+X₈ ∧ 1 ≤ X₈ ∧ 1 ≤ X₈+X₉ ∧ 0 ≤ 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}
g₁₆: inf {Infinity}
g₁₈: inf {Infinity}
g₂₀: inf {Infinity}
g₂₂: inf {Infinity}
g₂₄: inf {Infinity}
g₂₆: inf {Infinity}
g₂₈: inf {Infinity}
Costbounds
Overall costbound: inf {Infinity}
g₀: inf {Infinity}
g₂: inf {Infinity}
g₁₂: inf {Infinity}
g₁₄: inf {Infinity}
g₁₆: inf {Infinity}
g₁₈: inf {Infinity}
g₂₀: inf {Infinity}
g₂₂: inf {Infinity}
g₂₄: inf {Infinity}
g₂₆: inf {Infinity}
g₂₈: inf {Infinity}
Sizebounds
(g₀,g), X₀: 0 {O(1)}
(g₀,g), X₁: 0 {O(1)}
(g₀,g), X₂: 0 {O(1)}
(g₀,g), X₃: 0 {O(1)}
(g₀,g), X₄: 0 {O(1)}
(g₀,g), X₅: 0 {O(1)}
(g₀,g), X₆: 0 {O(1)}
(g₀,g), X₇: 0 {O(1)}
(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₃: g(X₈,X₉) -{0}> h(X₈,Temp_Int₄₅₀) :|: 1 ≤ X₈ ∧ Temp_Int₄₅₀ ≤ 0 ∧ 0 ≤ Temp_Int₄₅₀ ∧ 1 ≤ X₈ of depth 1:
new bound:
8⋅X₈+7 {O(n)}
MPRF:
• g: [8⋅X₈-7]
• h: [8⋅X₈+X₉-15]
MPRF for transition t₄: g(X₈,X₉) -{0}> h(X₈,Temp_Int₄₅₁) :|: 1 ≤ X₈ ∧ Temp_Int₄₅₁ ≤ 1 ∧ 1 ≤ Temp_Int₄₅₁ ∧ 1 ≤ X₈ of depth 1:
new bound:
8⋅X₈+7 {O(n)}
MPRF:
• g: [8⋅X₈-7]
• h: [8⋅X₈+X₉-15]
MPRF for transition t₅: g(X₈,X₉) -{0}> h(X₈,Temp_Int₄₅₂) :|: 1 ≤ X₈ ∧ Temp_Int₄₅₂ ≤ 2 ∧ 2 ≤ Temp_Int₄₅₂ ∧ 1 ≤ X₈ of depth 1:
new bound:
8⋅X₈+7 {O(n)}
MPRF:
• g: [8⋅X₈-7]
• h: [8⋅X₈+X₉-15]
MPRF for transition t₆: g(X₈,X₉) -{0}> h(X₈,Temp_Int₄₅₃) :|: 1 ≤ X₈ ∧ Temp_Int₄₅₃ ≤ 3 ∧ 3 ≤ Temp_Int₄₅₃ ∧ 1 ≤ X₈ of depth 1:
new bound:
8⋅X₈+7 {O(n)}
MPRF:
• g: [8⋅X₈-7]
• h: [8⋅X₈+X₉-15]
MPRF for transition t₇: g(X₈,X₉) -{0}> h(X₈,Temp_Int₄₅₄) :|: 1 ≤ X₈ ∧ Temp_Int₄₅₄ ≤ 4 ∧ 4 ≤ Temp_Int₄₅₄ ∧ 1 ≤ X₈ of depth 1:
new bound:
8⋅X₈+7 {O(n)}
MPRF:
• g: [8⋅X₈-7]
• h: [8⋅X₈+X₉-15]
MPRF for transition t₈: g(X₈,X₉) -{0}> h(X₈,Temp_Int₄₅₅) :|: 1 ≤ X₈ ∧ Temp_Int₄₅₅ ≤ 5 ∧ 5 ≤ Temp_Int₄₅₅ ∧ 1 ≤ X₈ of depth 1:
new bound:
8⋅X₈+7 {O(n)}
MPRF:
• g: [8⋅X₈-7]
• h: [8⋅X₈+X₉-15]
MPRF for transition t₉: g(X₈,X₉) -{0}> h(X₈,Temp_Int₄₅₆) :|: 1 ≤ X₈ ∧ Temp_Int₄₅₆ ≤ 6 ∧ 6 ≤ Temp_Int₄₅₆ ∧ 1 ≤ X₈ of depth 1:
new bound:
8⋅X₈+7 {O(n)}
MPRF:
• g: [8⋅X₈-7]
• h: [8⋅X₈+X₉-15]
MPRF for transition t₁₀: g(X₈,X₉) -{0}> h(X₈,Temp_Int₄₅₇) :|: 1 ≤ X₈ ∧ Temp_Int₄₅₇ ≤ 7 ∧ 7 ≤ Temp_Int₄₅₇ ∧ 1 ≤ X₈ of depth 1:
new bound:
8⋅X₈+7 {O(n)}
MPRF:
• g: [8⋅X₈-7]
• h: [8⋅X₈+X₉-15]
MPRF for transition t₁₃: h(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,X₉) → g(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈-1,X₉) :|: X₉ ≤ 8 ∧ X₉ ≤ 7+X₈ ∧ 1 ≤ X₈ ∧ 1 ≤ X₈+X₉ ∧ X₉ ≤ 0 ∧ 0 ≤ X₉ of depth 1:
new bound:
X₈ {O(n)}
MPRF:
• g: [X₈]
• h: [X₈]
MPRF for transition t₁₅: h(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,X₉) → g(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈-2,X₉) :|: X₉ ≤ 8 ∧ X₉ ≤ 7+X₈ ∧ 1 ≤ X₈ ∧ 1 ≤ X₈+X₉ ∧ 0 ≤ X₉ ∧ X₉ ≤ 1 ∧ 1 ≤ X₉ of depth 1:
new bound:
X₈ {O(n)}
MPRF:
• g: [X₈]
• h: [X₈]
MPRF for transition t₁₇: h(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,X₉) → g(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈-3,X₉) :|: X₉ ≤ 8 ∧ X₉ ≤ 7+X₈ ∧ 1 ≤ X₈ ∧ 1 ≤ X₈+X₉ ∧ 0 ≤ X₉ ∧ X₉ ≤ 2 ∧ 2 ≤ X₉ of depth 1:
new bound:
X₈ {O(n)}
MPRF:
• g: [X₈]
• h: [X₈]
MPRF for transition t₁₉: h(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,X₉) → g(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈-4,X₉) :|: X₉ ≤ 8 ∧ X₉ ≤ 7+X₈ ∧ 1 ≤ X₈ ∧ 1 ≤ X₈+X₉ ∧ 0 ≤ X₉ ∧ X₉ ≤ 3 ∧ 3 ≤ X₉ of depth 1:
new bound:
X₈ {O(n)}
MPRF:
• g: [X₈]
• h: [X₈]
MPRF for transition t₂₁: h(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,X₉) → g(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈-5,X₉) :|: X₉ ≤ 8 ∧ X₉ ≤ 7+X₈ ∧ 1 ≤ X₈ ∧ 1 ≤ X₈+X₉ ∧ 0 ≤ X₉ ∧ X₉ ≤ 4 ∧ 4 ≤ X₉ of depth 1:
new bound:
X₈ {O(n)}
MPRF:
• g: [X₈]
• h: [X₈]
MPRF for transition t₂₃: h(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,X₉) → g(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈-6,X₉) :|: X₉ ≤ 8 ∧ X₉ ≤ 7+X₈ ∧ 1 ≤ X₈ ∧ 1 ≤ X₈+X₉ ∧ 0 ≤ X₉ ∧ X₉ ≤ 5 ∧ 5 ≤ X₉ of depth 1:
new bound:
X₈ {O(n)}
MPRF:
• g: [X₈]
• h: [X₈]
MPRF for transition t₂₅: h(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,X₉) → g(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈-7,X₉) :|: X₉ ≤ 8 ∧ X₉ ≤ 7+X₈ ∧ 1 ≤ X₈ ∧ 1 ≤ X₈+X₉ ∧ 0 ≤ X₉ ∧ X₉ ≤ 6 ∧ 6 ≤ X₉ of depth 1:
new bound:
X₈ {O(n)}
MPRF:
• g: [X₈]
• h: [X₈]
MPRF for transition t₂₇: h(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,X₉) → g(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈-8,X₉) :|: X₉ ≤ 8 ∧ X₉ ≤ 7+X₈ ∧ 1 ≤ X₈ ∧ 1 ≤ X₈+X₉ ∧ 0 ≤ X₉ ∧ X₉ ≤ 7 ∧ 7 ≤ X₉ of depth 1:
new bound:
X₈ {O(n)}
MPRF:
• g: [X₈]
• h: [X₈]
Classical Approximation after Lifting Classical Results
All Bounds
Timebounds
Overall timebound:inf {Infinity}
g₀: 1 {O(1)}
g₂: inf {Infinity}
g₁₂: X₈ {O(n)}
g₁₄: X₈ {O(n)}
g₁₆: X₈ {O(n)}
g₁₈: X₈ {O(n)}
g₂₀: X₈ {O(n)}
g₂₂: X₈ {O(n)}
g₂₄: X₈ {O(n)}
g₂₆: X₈ {O(n)}
g₂₈: inf {Infinity}
Costbounds
Overall costbound: inf {Infinity}
g₀: inf {Infinity}
g₂: inf {Infinity}
g₁₂: inf {Infinity}
g₁₄: inf {Infinity}
g₁₆: inf {Infinity}
g₁₈: inf {Infinity}
g₂₀: inf {Infinity}
g₂₂: inf {Infinity}
g₂₄: inf {Infinity}
g₂₆: inf {Infinity}
g₂₈: inf {Infinity}
Sizebounds
(g₀,g), X₀: 0 {O(1)}
(g₀,g), X₁: 0 {O(1)}
(g₀,g), X₂: 0 {O(1)}
(g₀,g), X₃: 0 {O(1)}
(g₀,g), X₄: 0 {O(1)}
(g₀,g), X₅: 0 {O(1)}
(g₀,g), X₆: 0 {O(1)}
(g₀,g), X₇: 0 {O(1)}
(g₀,g), X₈: X₈ {O(n)}
(g₀,g), X₉: X₉ {O(n)}
(g₂,h), X₀: 0 {O(1)}
(g₂,h), X₁: 0 {O(1)}
(g₂,h), X₂: 0 {O(1)}
(g₂,h), X₃: 0 {O(1)}
(g₂,h), X₄: 0 {O(1)}
(g₂,h), X₅: 0 {O(1)}
(g₂,h), X₆: 0 {O(1)}
(g₂,h), X₇: 0 {O(1)}
(g₂,h), X₈: 198⋅X₈ {O(n)}
(g₂,h), X₉: 36 {O(1)}
(g₁₂,g), X₀: 0 {O(1)}
(g₁₂,g), X₁: 0 {O(1)}
(g₁₂,g), X₂: 0 {O(1)}
(g₁₂,g), X₃: 0 {O(1)}
(g₁₂,g), X₄: 0 {O(1)}
(g₁₂,g), X₅: 0 {O(1)}
(g₁₂,g), X₆: 0 {O(1)}
(g₁₂,g), X₇: 0 {O(1)}
(g₁₂,g), X₈: 22⋅X₈ {O(n)}
(g₁₂,g), X₉: 0 {O(1)}
(g₁₄,g), X₀: 0 {O(1)}
(g₁₄,g), X₁: 0 {O(1)}
(g₁₄,g), X₂: 0 {O(1)}
(g₁₄,g), X₃: 0 {O(1)}
(g₁₄,g), X₄: 0 {O(1)}
(g₁₄,g), X₅: 0 {O(1)}
(g₁₄,g), X₆: 0 {O(1)}
(g₁₄,g), X₇: 0 {O(1)}
(g₁₄,g), X₈: 22⋅X₈ {O(n)}
(g₁₄,g), X₉: 1 {O(1)}
(g₁₆,g), X₀: 0 {O(1)}
(g₁₆,g), X₁: 0 {O(1)}
(g₁₆,g), X₂: 0 {O(1)}
(g₁₆,g), X₃: 0 {O(1)}
(g₁₆,g), X₄: 0 {O(1)}
(g₁₆,g), X₅: 0 {O(1)}
(g₁₆,g), X₆: 0 {O(1)}
(g₁₆,g), X₇: 0 {O(1)}
(g₁₆,g), X₈: 22⋅X₈ {O(n)}
(g₁₆,g), X₉: 2 {O(1)}
(g₁₈,g), X₀: 0 {O(1)}
(g₁₈,g), X₁: 0 {O(1)}
(g₁₈,g), X₂: 0 {O(1)}
(g₁₈,g), X₃: 0 {O(1)}
(g₁₈,g), X₄: 0 {O(1)}
(g₁₈,g), X₅: 0 {O(1)}
(g₁₈,g), X₆: 0 {O(1)}
(g₁₈,g), X₇: 0 {O(1)}
(g₁₈,g), X₈: 22⋅X₈ {O(n)}
(g₁₈,g), X₉: 3 {O(1)}
(g₂₀,g), X₀: 0 {O(1)}
(g₂₀,g), X₁: 0 {O(1)}
(g₂₀,g), X₂: 0 {O(1)}
(g₂₀,g), X₃: 0 {O(1)}
(g₂₀,g), X₄: 0 {O(1)}
(g₂₀,g), X₅: 0 {O(1)}
(g₂₀,g), X₆: 0 {O(1)}
(g₂₀,g), X₇: 0 {O(1)}
(g₂₀,g), X₈: 22⋅X₈ {O(n)}
(g₂₀,g), X₉: 4 {O(1)}
(g₂₂,g), X₀: 0 {O(1)}
(g₂₂,g), X₁: 0 {O(1)}
(g₂₂,g), X₂: 0 {O(1)}
(g₂₂,g), X₃: 0 {O(1)}
(g₂₂,g), X₄: 0 {O(1)}
(g₂₂,g), X₅: 0 {O(1)}
(g₂₂,g), X₆: 0 {O(1)}
(g₂₂,g), X₇: 0 {O(1)}
(g₂₂,g), X₈: 22⋅X₈ {O(n)}
(g₂₂,g), X₉: 5 {O(1)}
(g₂₄,g), X₀: 0 {O(1)}
(g₂₄,g), X₁: 0 {O(1)}
(g₂₄,g), X₂: 0 {O(1)}
(g₂₄,g), X₃: 0 {O(1)}
(g₂₄,g), X₄: 0 {O(1)}
(g₂₄,g), X₅: 0 {O(1)}
(g₂₄,g), X₆: 0 {O(1)}
(g₂₄,g), X₇: 0 {O(1)}
(g₂₄,g), X₈: 22⋅X₈ {O(n)}
(g₂₄,g), X₉: 6 {O(1)}
(g₂₆,g), X₀: 0 {O(1)}
(g₂₆,g), X₁: 0 {O(1)}
(g₂₆,g), X₂: 0 {O(1)}
(g₂₆,g), X₃: 0 {O(1)}
(g₂₆,g), X₄: 0 {O(1)}
(g₂₆,g), X₅: 0 {O(1)}
(g₂₆,g), X₆: 0 {O(1)}
(g₂₆,g), X₇: 0 {O(1)}
(g₂₆,g), X₈: 22⋅X₈ {O(n)}
(g₂₆,g), X₉: 7 {O(1)}
(g₂₈,g), X₀: 0 {O(1)}
(g₂₈,g), X₁: 0 {O(1)}
(g₂₈,g), X₂: 0 {O(1)}
(g₂₈,g), X₃: 0 {O(1)}
(g₂₈,g), X₄: 0 {O(1)}
(g₂₈,g), X₅: 0 {O(1)}
(g₂₈,g), X₆: 0 {O(1)}
(g₂₈,g), X₇: 0 {O(1)}
(g₂₈,g), X₈: 22⋅X₈ {O(n)}
(g₂₈,g), X₉: 8 {O(1)}
Run probabilistic analysis on SCC: [g; h]
Plrf for transition g₂:g(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,X₉) -{0}> [1/10]:t₃:h(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,0) :+: [1/10]:t₄:h(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,1) :+: [1/10]:t₅:h(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,2) :+: [1/10]:t₆:h(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,3) :+: [1/10]:t₇:h(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,4) :+: [1/10]:t₈:h(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,5) :+: [1/10]:t₉:h(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,6) :+: [1/10]:t₁₀:h(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,7) :+: [1/5]:t₁₁:h(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,8) :|: 1 ≤ X₈:
new bound:
20/9⋅X₈+140/9 {O(n)}
PLRF:
• g: 140/9+20/9⋅X₈
• h: 40/3+20/9⋅X₈+5/18⋅X₉
Use expected size bounds for entry point (g₀:f→[t₁:1:g],g)
Use classical time bound for entry point (g₀:f→[t₁:1:g],g)
Plrf for transition g₂₈:h(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,X₉) → t₂₉:g(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,X₉) :|: X₉ ≤ 8 ∧ 8 ≤ X₉ ∧ X₉ ≤ 7+X₈ ∧ 1 ≤ X₈ ∧ 1 ≤ X₈+X₉ ∧ 0 ≤ X₉:
new bound:
11/9⋅X₈+77/9 {O(n)}
PLRF:
• g: 77/9+11/9⋅X₈
• h: 22/3+11/9⋅X₈+5/18⋅X₉
Use expected size bounds for entry point (g₀:f→[t₁:1:g],g)
Use classical time bound for entry point (g₀:f→[t₁:1:g],g)
Results of Probabilistic Analysis
All Bounds
Timebounds
Overall timebound:103/9⋅X₈+226/9 {O(n)}
g₀: 1 {O(1)}
g₂: 20/9⋅X₈+140/9 {O(n)}
g₁₂: X₈ {O(n)}
g₁₄: X₈ {O(n)}
g₁₆: X₈ {O(n)}
g₁₈: X₈ {O(n)}
g₂₀: X₈ {O(n)}
g₂₂: X₈ {O(n)}
g₂₄: X₈ {O(n)}
g₂₆: X₈ {O(n)}
g₂₈: 11/9⋅X₈+77/9 {O(n)}
Costbounds
Overall costbound: 83/9⋅X₈+77/9 {O(n)}
g₀: 0 {O(1)}
g₂: 0 {O(1)}
g₁₂: X₈ {O(n)}
g₁₄: X₈ {O(n)}
g₁₆: X₈ {O(n)}
g₁₈: X₈ {O(n)}
g₂₀: X₈ {O(n)}
g₂₂: X₈ {O(n)}
g₂₄: X₈ {O(n)}
g₂₆: X₈ {O(n)}
g₂₈: 11/9⋅X₈+77/9 {O(n)}
Sizebounds
(g₀,g), X₀: 0 {O(1)}
(g₀,g), X₁: 0 {O(1)}
(g₀,g), X₂: 0 {O(1)}
(g₀,g), X₃: 0 {O(1)}
(g₀,g), X₄: 0 {O(1)}
(g₀,g), X₅: 0 {O(1)}
(g₀,g), X₆: 0 {O(1)}
(g₀,g), X₇: 0 {O(1)}
(g₀,g), X₈: X₈ {O(n)}
(g₀,g), X₉: X₉ {O(n)}
(g₂,h), X₀: 0 {O(1)}
(g₂,h), X₁: 0 {O(1)}
(g₂,h), X₂: 0 {O(1)}
(g₂,h), X₃: 0 {O(1)}
(g₂,h), X₄: 0 {O(1)}
(g₂,h), X₅: 0 {O(1)}
(g₂,h), X₆: 0 {O(1)}
(g₂,h), X₇: 0 {O(1)}
(g₂,h), X₈: 34⋅X₈ {O(n)}
(g₂,h), X₉: 36 {O(1)}
(g₁₂,g), X₀: 0 {O(1)}
(g₁₂,g), X₁: 0 {O(1)}
(g₁₂,g), X₂: 0 {O(1)}
(g₁₂,g), X₃: 0 {O(1)}
(g₁₂,g), X₄: 0 {O(1)}
(g₁₂,g), X₅: 0 {O(1)}
(g₁₂,g), X₆: 0 {O(1)}
(g₁₂,g), X₇: 0 {O(1)}
(g₁₂,g), X₈: 22⋅X₈ {O(n)}
(g₁₂,g), X₉: 0 {O(1)}
(g₁₄,g), X₀: 0 {O(1)}
(g₁₄,g), X₁: 0 {O(1)}
(g₁₄,g), X₂: 0 {O(1)}
(g₁₄,g), X₃: 0 {O(1)}
(g₁₄,g), X₄: 0 {O(1)}
(g₁₄,g), X₅: 0 {O(1)}
(g₁₄,g), X₆: 0 {O(1)}
(g₁₄,g), X₇: 0 {O(1)}
(g₁₄,g), X₈: 22⋅X₈ {O(n)}
(g₁₄,g), X₉: 1 {O(1)}
(g₁₆,g), X₀: 0 {O(1)}
(g₁₆,g), X₁: 0 {O(1)}
(g₁₆,g), X₂: 0 {O(1)}
(g₁₆,g), X₃: 0 {O(1)}
(g₁₆,g), X₄: 0 {O(1)}
(g₁₆,g), X₅: 0 {O(1)}
(g₁₆,g), X₆: 0 {O(1)}
(g₁₆,g), X₇: 0 {O(1)}
(g₁₆,g), X₈: 22⋅X₈ {O(n)}
(g₁₆,g), X₉: 2 {O(1)}
(g₁₈,g), X₀: 0 {O(1)}
(g₁₈,g), X₁: 0 {O(1)}
(g₁₈,g), X₂: 0 {O(1)}
(g₁₈,g), X₃: 0 {O(1)}
(g₁₈,g), X₄: 0 {O(1)}
(g₁₈,g), X₅: 0 {O(1)}
(g₁₈,g), X₆: 0 {O(1)}
(g₁₈,g), X₇: 0 {O(1)}
(g₁₈,g), X₈: 22⋅X₈ {O(n)}
(g₁₈,g), X₉: 3 {O(1)}
(g₂₀,g), X₀: 0 {O(1)}
(g₂₀,g), X₁: 0 {O(1)}
(g₂₀,g), X₂: 0 {O(1)}
(g₂₀,g), X₃: 0 {O(1)}
(g₂₀,g), X₄: 0 {O(1)}
(g₂₀,g), X₅: 0 {O(1)}
(g₂₀,g), X₆: 0 {O(1)}
(g₂₀,g), X₇: 0 {O(1)}
(g₂₀,g), X₈: 22⋅X₈ {O(n)}
(g₂₀,g), X₉: 4 {O(1)}
(g₂₂,g), X₀: 0 {O(1)}
(g₂₂,g), X₁: 0 {O(1)}
(g₂₂,g), X₂: 0 {O(1)}
(g₂₂,g), X₃: 0 {O(1)}
(g₂₂,g), X₄: 0 {O(1)}
(g₂₂,g), X₅: 0 {O(1)}
(g₂₂,g), X₆: 0 {O(1)}
(g₂₂,g), X₇: 0 {O(1)}
(g₂₂,g), X₈: 22⋅X₈ {O(n)}
(g₂₂,g), X₉: 5 {O(1)}
(g₂₄,g), X₀: 0 {O(1)}
(g₂₄,g), X₁: 0 {O(1)}
(g₂₄,g), X₂: 0 {O(1)}
(g₂₄,g), X₃: 0 {O(1)}
(g₂₄,g), X₄: 0 {O(1)}
(g₂₄,g), X₅: 0 {O(1)}
(g₂₄,g), X₆: 0 {O(1)}
(g₂₄,g), X₇: 0 {O(1)}
(g₂₄,g), X₈: 22⋅X₈ {O(n)}
(g₂₄,g), X₉: 6 {O(1)}
(g₂₆,g), X₀: 0 {O(1)}
(g₂₆,g), X₁: 0 {O(1)}
(g₂₆,g), X₂: 0 {O(1)}
(g₂₆,g), X₃: 0 {O(1)}
(g₂₆,g), X₄: 0 {O(1)}
(g₂₆,g), X₅: 0 {O(1)}
(g₂₆,g), X₆: 0 {O(1)}
(g₂₆,g), X₇: 0 {O(1)}
(g₂₆,g), X₈: 22⋅X₈ {O(n)}
(g₂₆,g), X₉: 7 {O(1)}
(g₂₈,g), X₀: 0 {O(1)}
(g₂₈,g), X₁: 0 {O(1)}
(g₂₈,g), X₂: 0 {O(1)}
(g₂₈,g), X₃: 0 {O(1)}
(g₂₈,g), X₄: 0 {O(1)}
(g₂₈,g), X₅: 0 {O(1)}
(g₂₈,g), X₆: 0 {O(1)}
(g₂₈,g), X₇: 0 {O(1)}
(g₂₈,g), X₈: 22⋅X₈ {O(n)}
(g₂₈,g), X₉: 8 {O(1)}