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₁

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₁]

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₄]

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₄]

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₆]

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₆]

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₆

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₆

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)}