Preprocessing

Found invariant 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₀ for location l2

Probabilistic Analysis

Probabilistic Program after Preprocessing

Start: l0
Program_Vars: X₀, X₁, X₂
Temp_Vars:
Locations: l0, l1, l2
Transitions:
g₀:l0(X₀,X₁,X₂) → t₁:l1(X₀,X₁,X₂) :|:
g₂:l1(X₀,X₁,X₂) → t₃:l2(X₀,X₁,X₂) :|: 1 ≤ X₀ ∧ X₀ ≤ X₂
g₄:l2(X₀,X₁,X₂) → t₅:l1(3⋅X₀,X₁,2⋅X₂) :|: X₁ ≤ 0 ∧ 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂
g₆:l2(X₀,X₁,X₂) → [1/2]:t₇:l1(X₀-1,X₁,X₂) :+: [1/2]:t₈:l1(X₀,X₁,X₂) :|: 1 ≤ X₁ ∧ 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂

Run classical analysis on SCC: [l0]

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₀,l1), X₀: X₀ {O(n)}
(g₀,l1), X₁: X₁ {O(n)}
(g₀,l1), X₂: X₂ {O(n)}

Run probabilistic analysis on SCC: [l0]

Run classical analysis on SCC: [l1; l2]

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₀,l1), X₀: X₀ {O(n)}
(g₀,l1), X₁: X₁ {O(n)}
(g₀,l1), X₂: X₂ {O(n)}
(g₂,l2), X₁: X₁ {O(n)}
(g₄,l1), X₁: X₁ {O(n)}
(g₆,l1), X₁: 2⋅X₁ {O(n)}

Run probabilistic analysis on SCC: [l1; l2]

Analysing control-flow refined program

Run classical analysis on SCC: [l1]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:inf {Infinity}
g₀: 1 {O(1)}
g₁₀: 1 {O(1)}
g₁₂: 1 {O(1)}
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}

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₀,l1), X₀: X₀ {O(n)}
(g₀,l1), X₁: X₁ {O(n)}
(g₀,l1), X₂: X₂ {O(n)}
(g₁₀,l2_v1), X₀: X₀ {O(n)}
(g₁₀,l2_v1), X₁: X₁ {O(n)}
(g₁₀,l2_v1), X₂: X₂ {O(n)}

Run probabilistic analysis on SCC: [l1]

Run classical analysis on SCC: [l2_v1]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:inf {Infinity}
g₀: 1 {O(1)}
g₁₀: 1 {O(1)}
g₁₂: 1 {O(1)}
g₁₅: 2 {O(1)}
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₀,l1), X₀: X₀ {O(n)}
(g₀,l1), X₁: X₁ {O(n)}
(g₀,l1), X₂: X₂ {O(n)}
(g₁₀,l2_v1), X₀: X₀ {O(n)}
(g₁₀,l2_v1), X₁: X₁ {O(n)}
(g₁₀,l2_v1), X₂: X₂ {O(n)}
(g₁₂,l1_v1), X₀: 3⋅X₀ {O(n)}
(g₁₂,l1_v1), X₁: X₁ {O(n)}
(g₁₂,l1_v1), X₂: 2⋅X₂ {O(n)}
(g₁₅,l1_v2), X₀: 2⋅X₀ {O(n)}
(g₁₅,l1_v2), X₁: 2⋅X₁ {O(n)}
(g₁₅,l1_v2), X₂: 2⋅X₂ {O(n)}
(g₁₅,l1_v3), X₀: 2⋅X₀ {O(n)}
(g₁₅,l1_v3), X₁: 2⋅X₁ {O(n)}
(g₁₅,l1_v3), X₂: 2⋅X₂ {O(n)}

Run probabilistic analysis on SCC: [l2_v1]

Run classical analysis on SCC: [l1_v1; l2_v4]

TWN: t₂₈: l1_v1→l2_v4

cycle: [t₂₈: l1_v1→l2_v4; t₃₀: l2_v4→l1_v1]
loop: (1 ≤ X₀ ∧ X₀ ≤ X₂ ∧ X₁ ≤ 0,(X₀,X₁,X₂) -> (3⋅X₀,X₁,2⋅X₂)
order: [X₀; X₁; X₂]
closed-form:
X₀: X₀ * 3^n
X₁: X₁
X₂: X₂ * 2^n

Termination: true
Formula:

0 ≤ 1 ∧ 1 ≤ 0 ∧ 1+X₀ ≤ 0 ∧ 1+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 1 ∧ 1 ≤ 0 ∧ 1+X₀ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
∨ 0 ≤ 1 ∧ 1 ≤ 0 ∧ 1+X₁ ≤ 0 ∧ 1 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 0 ≤ 1 ∧ 1 ≤ 0 ∧ 1+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₂ ∧ X₂ ≤ 0
∨ 0 ≤ 1 ∧ 1 ≤ 0 ∧ 1 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
∨ 0 ≤ 1 ∧ 1 ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0 ∧ 0 ≤ X₂ ∧ X₂ ≤ 0
∨ 1 ≤ 0 ∧ 1+X₀ ≤ 0 ∧ 1+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 1 ≤ 0 ∧ 1+X₀ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
∨ 1 ≤ 0 ∧ 1+X₁ ≤ 0 ∧ 1 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 1 ≤ 0 ∧ 1+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₂ ∧ X₂ ≤ 0
∨ 1 ≤ 0 ∧ 1 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
∨ 1 ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0 ∧ 0 ≤ X₂ ∧ X₂ ≤ 0
∨ 1 ≤ X₀ ∧ 1+X₀ ≤ 0 ∧ 1+X₁ ≤ 0
∨ 1 ≤ X₀ ∧ 1+X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
∨ 1 ≤ X₀ ∧ 1+X₁ ≤ 0 ∧ 1 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
∨ 1 ≤ X₀ ∧ 1+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₂ ∧ X₂ ≤ 0
∨ 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0
∨ 1 ≤ X₀ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0 ∧ 0 ≤ X₂ ∧ X₂ ≤ 0

Stabilization-Threshold for: X₀ ≤ X₂
alphas_abs: 1+X₂
M: 0
N: 1
Bound: 2⋅X₂+4 {O(n)}

TWN - Lifting for [28: l1_v1->l2_v4; 30: l2_v4->l1_v1] of 2⋅X₂+8 {O(n)}

relevant size-bounds w.r.t. t₁₁: l2_v1→l1_v1:
X₂: 2⋅X₂ {O(n)}
Runtime-bound of t₁₁: 1 {O(1)}
Results in: 4⋅X₂+8 {O(n)}

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:inf {Infinity}
g₀: 1 {O(1)}
g₁₀: 1 {O(1)}
g₁₂: 1 {O(1)}
g₁₅: 2 {O(1)}
g₁₇: inf {Infinity}
g₂₀: inf {Infinity}
g₂₂: inf {Infinity}
g₂₄: inf {Infinity}
g₂₇: inf {Infinity}
g₂₉: 4⋅X₂+8 {O(n)}
g₃₁: 4⋅X₂+8 {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}

Sizebounds

(g₀,l1), X₀: X₀ {O(n)}
(g₀,l1), X₁: X₁ {O(n)}
(g₀,l1), X₂: X₂ {O(n)}
(g₁₀,l2_v1), X₀: X₀ {O(n)}
(g₁₀,l2_v1), X₁: X₁ {O(n)}
(g₁₀,l2_v1), X₂: X₂ {O(n)}
(g₁₂,l1_v1), X₀: 3⋅X₀ {O(n)}
(g₁₂,l1_v1), X₁: X₁ {O(n)}
(g₁₂,l1_v1), X₂: 2⋅X₂ {O(n)}
(g₁₅,l1_v2), X₀: X₀ {O(n)}
(g₁₅,l1_v2), X₁: X₁ {O(n)}
(g₁₅,l1_v2), X₂: X₂ {O(n)}
(g₁₅,l1_v3), X₀: X₀ {O(n)}
(g₁₅,l1_v3), X₁: X₁ {O(n)}
(g₁₅,l1_v3), X₂: X₂ {O(n)}
(g₂₉,l2_v4), X₀: 3⋅3^(4⋅X₂+8)⋅X₀ {O(EXP)}
(g₂₉,l2_v4), X₁: X₁ {O(n)}
(g₂₉,l2_v4), X₂: 2⋅2^(4⋅X₂+8)⋅X₂ {O(EXP)}
(g₃₁,l1_v1), X₀: 3⋅3^(4⋅X₂+8)⋅X₀ {O(EXP)}
(g₃₁,l1_v1), X₁: X₁ {O(n)}
(g₃₁,l1_v1), X₂: 2⋅2^(4⋅X₂+8)⋅X₂ {O(EXP)}

Run probabilistic analysis on SCC: [l1_v1; l2_v4]

Run classical analysis on SCC: [l1_v3; l2_v3]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:inf {Infinity}
g₀: 1 {O(1)}
g₁₀: 1 {O(1)}
g₁₂: 1 {O(1)}
g₁₅: 2 {O(1)}
g₁₇: inf {Infinity}
g₂₀: inf {Infinity}
g₂₂: inf {Infinity}
g₂₄: inf {Infinity}
g₂₇: inf {Infinity}
g₂₉: 4⋅X₂+8 {O(n)}
g₃₁: 4⋅X₂+8 {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}

Sizebounds

(g₀,l1), X₀: X₀ {O(n)}
(g₀,l1), X₁: X₁ {O(n)}
(g₀,l1), X₂: X₂ {O(n)}
(g₁₀,l2_v1), X₀: X₀ {O(n)}
(g₁₀,l2_v1), X₁: X₁ {O(n)}
(g₁₀,l2_v1), X₂: X₂ {O(n)}
(g₁₂,l1_v1), X₀: 3⋅X₀ {O(n)}
(g₁₂,l1_v1), X₁: X₁ {O(n)}
(g₁₂,l1_v1), X₂: 2⋅X₂ {O(n)}
(g₁₅,l1_v2), X₀: X₀ {O(n)}
(g₁₅,l1_v2), X₁: X₁ {O(n)}
(g₁₅,l1_v2), X₂: X₂ {O(n)}
(g₁₅,l1_v3), X₀: X₀ {O(n)}
(g₁₅,l1_v3), X₁: X₁ {O(n)}
(g₁₅,l1_v3), X₂: X₂ {O(n)}
(g₂₄,l2_v3), X₀: X₀ {O(n)}
(g₂₄,l2_v3), X₁: X₁ {O(n)}
(g₂₄,l2_v3), X₂: X₂ {O(n)}
(g₂₇,l1_v2), X₀: 2⋅X₀ {O(n)}
(g₂₇,l1_v2), X₁: 2⋅X₁ {O(n)}
(g₂₇,l1_v2), X₂: 2⋅X₂ {O(n)}
(g₂₇,l1_v3), X₀: 2⋅X₀ {O(n)}
(g₂₇,l1_v3), X₁: 2⋅X₁ {O(n)}
(g₂₇,l1_v3), X₂: 2⋅X₂ {O(n)}
(g₂₉,l2_v4), X₀: 3⋅3^(4⋅X₂+8)⋅X₀ {O(EXP)}
(g₂₉,l2_v4), X₁: X₁ {O(n)}
(g₂₉,l2_v4), X₂: 2⋅2^(4⋅X₂+8)⋅X₂ {O(EXP)}
(g₃₁,l1_v1), X₀: 3⋅3^(4⋅X₂+8)⋅X₀ {O(EXP)}
(g₃₁,l1_v1), X₁: X₁ {O(n)}
(g₃₁,l1_v1), X₂: 2⋅2^(4⋅X₂+8)⋅X₂ {O(EXP)}

Run probabilistic analysis on SCC: [l1_v3; l2_v3]

Plrf for transition g₂₄:l1_v3(X₀,X₁,X₂) → t₂₃:l2_v3(X₀,X₁,X₂) :|: 1 ≤ X₀ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁ ∧ 1 ≤ X₂ ∧ 0 ≤ X₀ ∧ 2⋅X₀ ≤ 3⋅X₂:

new bound:

X₂+1 {O(n)}

PLRF:

• l1_v2: X₂-1
• l1_v3: 1+X₂
• l2_v3: X₂

Use expected size bounds for entry point (g₁₅:l2_v1→[t₁₃:1/2:l1_v2; t₁₄:1/2:l1_v3],l1_v3)
Use classical time bound for entry point (g₁₅:l2_v1→[t₁₃:1/2:l1_v2; t₁₄:1/2:l1_v3],l1_v3)

Plrf for transition g₂₇:l2_v3(X₀,X₁,X₂) → [1/2]:t₂₅:l1_v2(X₀-1,X₁,X₂) :+: [1/2]:t₂₆:l1_v3(X₀,X₁,X₂) :|: 1 ≤ X₁ ∧ 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂:

new bound:

2⋅X₂ {O(n)}

PLRF:

• l1_v2: 0
• l1_v3: 2⋅X₂
• l2_v3: 1+X₂

Use expected size bounds for entry point (g₁₅:l2_v1→[t₁₃:1/2:l1_v2; t₁₄:1/2:l1_v3],l1_v3)
Use classical time bound for entry point (g₁₅:l2_v1→[t₁₃:1/2:l1_v2; t₁₄:1/2:l1_v3],l1_v3)

Run classical analysis on SCC: [l1_v2; l1_v4; l2_v2]

MPRF for transition t₁₆: l1_v2(X₀,X₁,X₂) → l2_v2(X₀,X₁,X₂) :|: 1+X₀ ≤ X₂ ∧ 1 ≤ X₁ ∧ 1 ≤ X₂ ∧ 0 ≤ X₀ ∧ 2⋅X₀ ≤ 3⋅X₂ ∧ 1 ≤ X₀ ∧ X₀ ≤ X₂ of depth 1:

new bound:

2⋅X₀+2 {O(n)}

MPRF:

• l1_v2: [1+X₀]
• l1_v4: [X₀]
• l2_v2: [X₀]

MPRF for transition t₁₈: l2_v2(X₀,X₁,X₂) → l1_v2(X₀-1,X₁,X₂) :|: 1 ≤ X₀ ∧ 1+X₀ ≤ X₂ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁ of depth 1:

new bound:

2⋅X₀ {O(n)}

MPRF:

• l1_v2: [X₀]
• l1_v4: [X₀]
• l2_v2: [X₀]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:inf {Infinity}
g₀: 1 {O(1)}
g₁₀: 1 {O(1)}
g₁₂: 1 {O(1)}
g₁₅: 2 {O(1)}
g₁₇: 2⋅X₀+2 {O(n)}
g₂₀: inf {Infinity}
g₂₂: inf {Infinity}
g₂₄: X₂+1 {O(n)}
g₂₇: 2⋅X₂ {O(n)}
g₂₉: 4⋅X₂+8 {O(n)}
g₃₁: 4⋅X₂+8 {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}

Sizebounds

(g₀,l1), X₀: X₀ {O(n)}
(g₀,l1), X₁: X₁ {O(n)}
(g₀,l1), X₂: X₂ {O(n)}
(g₁₀,l2_v1), X₀: X₀ {O(n)}
(g₁₀,l2_v1), X₁: X₁ {O(n)}
(g₁₀,l2_v1), X₂: X₂ {O(n)}
(g₁₂,l1_v1), X₀: 3⋅X₀ {O(n)}
(g₁₂,l1_v1), X₁: X₁ {O(n)}
(g₁₂,l1_v1), X₂: 2⋅X₂ {O(n)}
(g₁₅,l1_v2), X₀: X₀ {O(n)}
(g₁₅,l1_v2), X₁: X₁ {O(n)}
(g₁₅,l1_v2), X₂: X₂ {O(n)}
(g₁₅,l1_v3), X₀: X₀ {O(n)}
(g₁₅,l1_v3), X₁: X₁ {O(n)}
(g₁₅,l1_v3), X₂: X₂ {O(n)}
(g₁₇,l2_v2), X₀: 2⋅X₀ {O(n)}
(g₁₇,l2_v2), X₁: 2⋅X₁ {O(n)}
(g₁₇,l2_v2), X₂: 2⋅X₂ {O(n)}
(g₂₀,l1_v2), X₀: 4⋅X₀ {O(n)}
(g₂₀,l1_v2), X₁: 4⋅X₁ {O(n)}
(g₂₀,l1_v2), X₂: 4⋅X₂ {O(n)}
(g₂₀,l1_v4), X₀: 4⋅X₀ {O(n)}
(g₂₀,l1_v4), X₁: 4⋅X₁ {O(n)}
(g₂₀,l1_v4), X₂: 4⋅X₂ {O(n)}
(g₂₂,l2_v2), X₀: 2⋅X₀ {O(n)}
(g₂₂,l2_v2), X₁: 2⋅X₁ {O(n)}
(g₂₂,l2_v2), X₂: 2⋅X₂ {O(n)}
(g₂₄,l2_v3), X₀: X₀ {O(n)}
(g₂₄,l2_v3), X₁: X₁ {O(n)}
(g₂₄,l2_v3), X₂: X₂ {O(n)}
(g₂₇,l1_v2), X₀: X₀ {O(n)}
(g₂₇,l1_v2), X₁: X₁ {O(n)}
(g₂₇,l1_v2), X₂: X₂ {O(n)}
(g₂₇,l1_v3), X₀: X₀ {O(n)}
(g₂₇,l1_v3), X₁: X₁ {O(n)}
(g₂₇,l1_v3), X₂: X₂ {O(n)}
(g₂₉,l2_v4), X₀: 3⋅3^(4⋅X₂+8)⋅X₀ {O(EXP)}
(g₂₉,l2_v4), X₁: X₁ {O(n)}
(g₂₉,l2_v4), X₂: 2⋅2^(4⋅X₂+8)⋅X₂ {O(EXP)}
(g₃₁,l1_v1), X₀: 3⋅3^(4⋅X₂+8)⋅X₀ {O(EXP)}
(g₃₁,l1_v1), X₁: X₁ {O(n)}
(g₃₁,l1_v1), X₂: 2⋅2^(4⋅X₂+8)⋅X₂ {O(EXP)}

Run probabilistic analysis on SCC: [l1_v2; l1_v4; l2_v2]

Plrf for transition g₂₀:l2_v2(X₀,X₁,X₂) → [1/2]:t₁₈:l1_v2(X₀-1,X₁,X₂) :+: [1/2]:t₁₉:l1_v4(X₀,X₁,X₂) :|: 1 ≤ X₁ ∧ 1 ≤ X₀ ∧ 1+X₀ ≤ X₂ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂:

new bound:

4⋅X₀ {O(n)}

PLRF:

• l1_v2: 2⋅X₀
• l1_v4: 2⋅X₀
• l2_v2: 2⋅X₀

Use expected size bounds for entry point (g₁₅:l2_v1→[t₁₃:1/2:l1_v2; t₁₄:1/2:l1_v3],l1_v2)
Use classical time bound for entry point (g₁₅:l2_v1→[t₁₃:1/2:l1_v2; t₁₄:1/2:l1_v3],l1_v2)
Use expected size bounds for entry point (g₂₇:l2_v3→[t₂₅:1/2:l1_v2; t₂₆:1/2:l1_v3],l1_v2)
Use classical time bound for entry point (g₂₇:l2_v3→[t₂₅:1/2:l1_v2; t₂₆:1/2:l1_v3],l1_v2)

Plrf for transition g₂₂:l1_v4(X₀,X₁,X₂) → t₂₁:l2_v2(X₀,X₁,X₂) :|: 1 ≤ X₀ ∧ X₀ ≤ X₂ ∧ 1+X₀ ≤ X₂ ∧ 1 ≤ X₁ ∧ 1 ≤ X₂ ∧ 0 ≤ X₀ ∧ 2⋅X₀ ≤ 3⋅X₂:

new bound:

2⋅X₀ {O(n)}

PLRF:

• l1_v2: X₀
• l1_v4: 1+X₀
• l2_v2: X₀

Use expected size bounds for entry point (g₁₅:l2_v1→[t₁₃:1/2:l1_v2; t₁₄:1/2:l1_v3],l1_v2)
Use classical time bound for entry point (g₁₅:l2_v1→[t₁₃:1/2:l1_v2; t₁₄:1/2:l1_v3],l1_v2)
Use expected size bounds for entry point (g₂₇:l2_v3→[t₂₅:1/2:l1_v2; t₂₆:1/2:l1_v3],l1_v2)
Use classical time bound for entry point (g₂₇:l2_v3→[t₂₅:1/2:l1_v2; t₂₆:1/2:l1_v3],l1_v2)

CFR: Improvement to new bound with the following program:

method: PartialEvaluationProbabilistic new bound:

O(n)

cfr-program:

Start: l0
Program_Vars: X₀, X₁, X₂
Temp_Vars:
Locations: l0, l1, l1_v1, l1_v2, l1_v3, l1_v4, l2_v1, l2_v2, l2_v3, l2_v4
Transitions:
g₀:l0(X₀,X₁,X₂) → t₁:l1(X₀,X₁,X₂) :|:
g₁₀:l1(X₀,X₁,X₂) → t₉:l2_v1(X₀,X₁,X₂) :|: 1 ≤ X₀ ∧ X₀ ≤ X₂
g₁₂:l2_v1(X₀,X₁,X₂) → t₁₁:l1_v1(3⋅X₀,X₁,2⋅X₂) :|: X₁ ≤ 0 ∧ 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂
g₁₅:l2_v1(X₀,X₁,X₂) → [1/2]:t₁₃:l1_v2(X₀-1,X₁,X₂) :+: [1/2]:t₁₄:l1_v3(X₀,X₁,X₂) :|: 1 ≤ X₁ ∧ 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂
g₁₇:l1_v2(X₀,X₁,X₂) → t₁₆:l2_v2(X₀,X₁,X₂) :|: 1 ≤ X₀ ∧ X₀ ≤ X₂ ∧ 1+X₀ ≤ X₂ ∧ 1 ≤ X₁ ∧ 1 ≤ X₂ ∧ 0 ≤ X₀ ∧ 2⋅X₀ ≤ 3⋅X₂
g₂₀:l2_v2(X₀,X₁,X₂) → [1/2]:t₁₈:l1_v2(X₀-1,X₁,X₂) :+: [1/2]:t₁₉:l1_v4(X₀,X₁,X₂) :|: 1 ≤ X₁ ∧ 1 ≤ X₀ ∧ 1+X₀ ≤ X₂ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂
g₂₂:l1_v4(X₀,X₁,X₂) → t₂₁:l2_v2(X₀,X₁,X₂) :|: 1 ≤ X₀ ∧ X₀ ≤ X₂ ∧ 1+X₀ ≤ X₂ ∧ 1 ≤ X₁ ∧ 1 ≤ X₂ ∧ 0 ≤ X₀ ∧ 2⋅X₀ ≤ 3⋅X₂
g₂₄:l1_v3(X₀,X₁,X₂) → t₂₃:l2_v3(X₀,X₁,X₂) :|: 1 ≤ X₀ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₁ ∧ 1 ≤ X₂ ∧ 0 ≤ X₀ ∧ 2⋅X₀ ≤ 3⋅X₂
g₂₇:l2_v3(X₀,X₁,X₂) → [1/2]:t₂₅:l1_v2(X₀-1,X₁,X₂) :+: [1/2]:t₂₆:l1_v3(X₀,X₁,X₂) :|: 1 ≤ X₁ ∧ 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ X₀ ≤ X₂
g₂₉:l1_v1(X₀,X₁,X₂) → t₂₈:l2_v4(X₀,X₁,X₂) :|: 1 ≤ X₀ ∧ X₀ ≤ X₂ ∧ 1 ≤ X₂ ∧ 3 ≤ X₀ ∧ 0 ≤ X₀ ∧ 2⋅X₀ ≤ 3⋅X₂ ∧ X₁ ≤ 0
g₃₁:l2_v4(X₀,X₁,X₂) → t₃₀:l1_v1(3⋅X₀,X₁,2⋅X₂) :|: X₁ ≤ 0 ∧ 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₀+X₂ ∧ 3 ≤ X₀ ∧ X₀ ≤ X₂

Results of Probabilistic Analysis

All Bounds

Timebounds

Overall timebound:11⋅X₂+8⋅X₀+24 {O(n)}
g₀: 1 {O(1)}
g₁₀: 1 {O(1)}
g₁₂: 1 {O(1)}
g₁₅: 2 {O(1)}
g₁₇: 2⋅X₀+2 {O(n)}
g₂₀: 4⋅X₀ {O(n)}
g₂₂: 2⋅X₀ {O(n)}
g₂₄: X₂+1 {O(n)}
g₂₇: 2⋅X₂ {O(n)}
g₂₉: 4⋅X₂+8 {O(n)}
g₃₁: 4⋅X₂+8 {O(n)}

Costbounds

Overall costbound: 12⋅X₀+13⋅X₂+26 {O(n)}
g₀: 1 {O(1)}
g₁₀: 1 {O(1)}
g₁₂: 1 {O(1)}
g₁₅: 4 {O(1)}
g₁₇: 2⋅X₀+2 {O(n)}
g₂₀: 8⋅X₀ {O(n)}
g₂₂: 2⋅X₀ {O(n)}
g₂₄: X₂+1 {O(n)}
g₂₇: 4⋅X₂ {O(n)}
g₂₉: 4⋅X₂+8 {O(n)}
g₃₁: 4⋅X₂+8 {O(n)}

Sizebounds

(g₀,l1), X₀: X₀ {O(n)}
(g₀,l1), X₁: X₁ {O(n)}
(g₀,l1), X₂: X₂ {O(n)}
(g₁₀,l2_v1), X₀: X₀ {O(n)}
(g₁₀,l2_v1), X₁: X₁ {O(n)}
(g₁₀,l2_v1), X₂: X₂ {O(n)}
(g₁₂,l1_v1), X₀: 3⋅X₀ {O(n)}
(g₁₂,l1_v1), X₁: X₁ {O(n)}
(g₁₂,l1_v1), X₂: 2⋅X₂ {O(n)}
(g₁₅,l1_v2), X₀: X₀ {O(n)}
(g₁₅,l1_v2), X₁: X₁ {O(n)}
(g₁₅,l1_v2), X₂: X₂ {O(n)}
(g₁₅,l1_v3), X₀: X₀ {O(n)}
(g₁₅,l1_v3), X₁: X₁ {O(n)}
(g₁₅,l1_v3), X₂: X₂ {O(n)}
(g₁₇,l2_v2), X₀: 2⋅X₀ {O(n)}
(g₁₇,l2_v2), X₁: 2⋅X₁ {O(n)}
(g₁₇,l2_v2), X₂: 2⋅X₂ {O(n)}
(g₂₀,l1_v2), X₀: 4⋅X₀ {O(n)}
(g₂₀,l1_v2), X₁: 4⋅X₁ {O(n)}
(g₂₀,l1_v2), X₂: 4⋅X₂ {O(n)}
(g₂₀,l1_v4), X₀: 4⋅X₀ {O(n)}
(g₂₀,l1_v4), X₁: 4⋅X₁ {O(n)}
(g₂₀,l1_v4), X₂: 4⋅X₂ {O(n)}
(g₂₂,l2_v2), X₀: 2⋅X₀ {O(n)}
(g₂₂,l2_v2), X₁: 2⋅X₁ {O(n)}
(g₂₂,l2_v2), X₂: 2⋅X₂ {O(n)}
(g₂₄,l2_v3), X₀: X₀ {O(n)}
(g₂₄,l2_v3), X₁: X₁ {O(n)}
(g₂₄,l2_v3), X₂: X₂ {O(n)}
(g₂₇,l1_v2), X₀: X₀ {O(n)}
(g₂₇,l1_v2), X₁: X₁ {O(n)}
(g₂₇,l1_v2), X₂: X₂ {O(n)}
(g₂₇,l1_v3), X₀: X₀ {O(n)}
(g₂₇,l1_v3), X₁: X₁ {O(n)}
(g₂₇,l1_v3), X₂: X₂ {O(n)}
(g₂₉,l2_v4), X₀: 3⋅3^(4⋅X₂+8)⋅X₀ {O(EXP)}
(g₂₉,l2_v4), X₁: X₁ {O(n)}
(g₂₉,l2_v4), X₂: 2⋅2^(4⋅X₂+8)⋅X₂ {O(EXP)}
(g₃₁,l1_v1), X₀: 3⋅3^(4⋅X₂+8)⋅X₀ {O(EXP)}
(g₃₁,l1_v1), X₁: X₁ {O(n)}
(g₃₁,l1_v1), X₂: 2⋅2^(4⋅X₂+8)⋅X₂ {O(EXP)}