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₃

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

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

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

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

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₀

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

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

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

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

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₁

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₁

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

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

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

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

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

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

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₀

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₀

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₃

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