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₁ ∧ 0 ≤ X₄ ∧ X₃ ≤ 1+X₄ ∧ X₂ ≤ 1+X₄ ∧ 0 ≤ X₁+X₄ ∧ X₃ ≤ X₂ ∧ X₃ ≤ X₁ ∧ X₂ ≤ X₃ ∧ X₂ ≤ X₁ ∧ 0 ≤ X₁ for location f43

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₄ ≤ 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, f43
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₁₂:f34(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇) → t₁₃:f34(X₀,X₁,X₂,X₃,1+X₄,X₅,X₆,X₇) :|: 2+X₄ ≤ X₃ ∧ 0 ≤ X₁ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ 0 ≤ X₁+X₄ ∧ X₄ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₂ ≤ X₃ ∧ 0 ≤ X₄
g₁₄:f34(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇) → t₁₅:f43(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇) :|: X₃ ≤ 1+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₇) → 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₁₆: 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}
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₁₆: 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}
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:

8⋅X₂⋅X₂+8⋅X₂+1 {O(n^2)}

MPRF:

• f18: [X₂-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:

4⋅X₂⋅X₂+4⋅X₂ {O(n^2)}

MPRF:

• f18: [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₁₂: inf {Infinity}
g₁₄: 1 {O(1)}
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}
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:

4⋅X₂⋅X₂+4⋅X₂ {O(n^2)}

PLRF:

• f18: 2⋅X₁
• f22: 2⋅X₁-2⋅X₆

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 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:

12⋅X₂⋅X₂+12⋅X₂+2 {O(n^2)}

PLRF:

• f18: 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 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)

Run classical analysis on SCC: [f34]

MPRF for transition t₁₃: f34(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇) → f34(X₀,X₁,X₂,X₃,1+X₄,X₅,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:

2⋅X₂+1 {O(n)}

MPRF:

• f34: [1+X₁-X₄]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:16⋅X₂⋅X₂+22⋅X₂+9 {O(n^2)}
g₀: 1 {O(1)}
g₂: X₂ {O(n)}
g₄: X₂+1 {O(n)}
g₆: 4⋅X₂⋅X₂+4⋅X₂ {O(n^2)}
g₉: 12⋅X₂⋅X₂+12⋅X₂+2 {O(n^2)}
g₁₂: 2⋅X₂+1 {O(n)}
g₁₄: 1 {O(1)}
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}
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₁₂,f34), X₁: 2⋅X₂ {O(n)}
(g₁₂,f34), X₂: 4⋅X₂ {O(n)}
(g₁₂,f34), X₃: 4⋅X₂ {O(n)}
(g₁₂,f34), X₄: 2⋅X₂+1 {O(n)}
(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₁₄,f43), X₁: 4⋅X₂ {O(n)}
(g₁₄,f43), X₂: 8⋅X₂ {O(n)}
(g₁₄,f43), X₃: 8⋅X₂ {O(n)}
(g₁₄,f43), X₄: 2⋅X₂+1 {O(n)}
(g₁₄,f43), X₅: 192⋅X₂⋅X₂+236⋅X₂+4⋅X₅+78 {O(n^2)}
(g₁₄,f43), X₆: 48⋅X₂⋅X₂+4⋅X₆+56⋅X₂+16 {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]

Run classical analysis on SCC: [f43]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:16⋅X₂⋅X₂+22⋅X₂+9 {O(n^2)}
g₀: 1 {O(1)}
g₂: X₂ {O(n)}
g₄: X₂+1 {O(n)}
g₆: 4⋅X₂⋅X₂+4⋅X₂ {O(n^2)}
g₉: 12⋅X₂⋅X₂+12⋅X₂+2 {O(n^2)}
g₁₂: 2⋅X₂+1 {O(n)}
g₁₄: 1 {O(1)}
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}
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₁₂,f34), X₁: 2⋅X₂ {O(n)}
(g₁₂,f34), X₂: 4⋅X₂ {O(n)}
(g₁₂,f34), X₃: 4⋅X₂ {O(n)}
(g₁₂,f34), X₄: 2⋅X₂+1 {O(n)}
(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₁₄,f43), X₁: 4⋅X₂ {O(n)}
(g₁₄,f43), X₂: 8⋅X₂ {O(n)}
(g₁₄,f43), X₃: 8⋅X₂ {O(n)}
(g₁₄,f43), X₄: 2⋅X₂+1 {O(n)}
(g₁₄,f43), X₅: 192⋅X₂⋅X₂+236⋅X₂+4⋅X₅+78 {O(n^2)}
(g₁₄,f43), X₆: 48⋅X₂⋅X₂+4⋅X₆+56⋅X₂+16 {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: [f43]

Results of Probabilistic Analysis

All Bounds

Timebounds

Overall timebound:16⋅X₂⋅X₂+22⋅X₂+9 {O(n^2)}
g₀: 1 {O(1)}
g₂: X₂ {O(n)}
g₄: X₂+1 {O(n)}
g₆: 4⋅X₂⋅X₂+4⋅X₂ {O(n^2)}
g₉: 12⋅X₂⋅X₂+12⋅X₂+2 {O(n^2)}
g₁₂: 2⋅X₂+1 {O(n)}
g₁₄: 1 {O(1)}
g₁₆: 2⋅X₂+1 {O(n)}
g₁₈: 1 {O(1)}
g₂₀: 1 {O(1)}

Costbounds

Overall costbound: 32⋅X₂⋅X₂+38⋅X₂+11 {O(n^2)}
g₀: 1 {O(1)}
g₂: X₂ {O(n)}
g₄: X₂+1 {O(n)}
g₆: 8⋅X₂⋅X₂+8⋅X₂ {O(n^2)}
g₉: 24⋅X₂⋅X₂+24⋅X₂+4 {O(n^2)}
g₁₂: 2⋅X₂+1 {O(n)}
g₁₄: 1 {O(1)}
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₁₂,f34), X₁: 2⋅X₂ {O(n)}
(g₁₂,f34), X₂: 4⋅X₂ {O(n)}
(g₁₂,f34), X₃: 4⋅X₂ {O(n)}
(g₁₂,f34), X₄: 2⋅X₂+1 {O(n)}
(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₁₄,f43), X₁: 4⋅X₂ {O(n)}
(g₁₄,f43), X₂: 8⋅X₂ {O(n)}
(g₁₄,f43), X₃: 8⋅X₂ {O(n)}
(g₁₄,f43), X₄: 2⋅X₂+1 {O(n)}
(g₁₄,f43), X₅: 192⋅X₂⋅X₂+236⋅X₂+4⋅X₅+78 {O(n^2)}
(g₁₄,f43), X₆: 48⋅X₂⋅X₂+4⋅X₆+56⋅X₂+16 {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)}