Preprocessing

Found invariant X₀ ≤ 1 ∧ 0 ≤ 1+X₀ for location l1

Probabilistic Analysis

Probabilistic Program after Preprocessing

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

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}

Costbounds

Overall costbound: inf {Infinity}
g₀: inf {Infinity}
g₂: inf {Infinity}
g₅: inf {Infinity}

Sizebounds

(g₀,l1), X₀: 1 {O(1)}
(g₀,l1), X₁: X₁ {O(n)}

Run probabilistic analysis on SCC: [l0]

Run classical analysis on SCC: [l1]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:inf {Infinity}
g₀: 1 {O(1)}
g₂: inf {Infinity}
g₅: inf {Infinity}

Costbounds

Overall costbound: inf {Infinity}
g₀: inf {Infinity}
g₂: inf {Infinity}
g₅: inf {Infinity}

Sizebounds

(g₀,l1), X₀: 1 {O(1)}
(g₀,l1), X₁: X₁ {O(n)}
(g₂,l1), X₀: 2 {O(1)}
(g₅,l1), X₀: 2 {O(1)}

Run probabilistic analysis on SCC: [l1]

Analysing control-flow refined program

Run classical analysis on SCC: [l1_v1]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:inf {Infinity}
g₀: 1 {O(1)}
g₁₀: 2 {O(1)}
g₁₃: 1 {O(1)}
g₁₆: inf {Infinity}
g₁₉: inf {Infinity}
g₂₂: inf {Infinity}
g₂₅: inf {Infinity}
g₂₈: inf {Infinity}
g₃₁: 2 {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₀,l1), X₀: 1 {O(1)}
(g₀,l1), X₁: X₁ {O(n)}
(g₃₁,l1_v3), X₀: 2 {O(1)}
(g₃₁,l1_v3), X₁: 23 {O(1)}
(g₃₁,l1_v4), X₀: 2 {O(1)}
(g₃₁,l1_v4), X₁: 23 {O(1)}

Run probabilistic analysis on SCC: [l1_v1]

Run classical analysis on SCC: [l1_v2]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:inf {Infinity}
g₀: 1 {O(1)}
g₁₀: 2 {O(1)}
g₁₃: 1 {O(1)}
g₁₆: inf {Infinity}
g₁₉: inf {Infinity}
g₂₂: inf {Infinity}
g₂₅: inf {Infinity}
g₂₈: inf {Infinity}
g₃₁: 2 {O(1)}
g₃₄: 2 {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₀,l1), X₀: 1 {O(1)}
(g₀,l1), X₁: X₁ {O(n)}
(g₁₀,l1_v1), X₀: 1 {O(1)}
(g₁₀,l1_v1), X₁: 2⋅X₁+1 {O(n)}
(g₁₀,l1_v2), X₀: 1 {O(1)}
(g₁₀,l1_v2), X₁: X₁ {O(n)}
(g₃₁,l1_v3), X₀: 2 {O(1)}
(g₃₁,l1_v3), X₁: 23 {O(1)}
(g₃₁,l1_v4), X₀: 2 {O(1)}
(g₃₁,l1_v4), X₁: 23 {O(1)}
(g₃₄,l1_v3), X₀: 2 {O(1)}
(g₃₄,l1_v3), X₁: 21 {O(1)}
(g₃₄,l1_v7), X₀: 2 {O(1)}
(g₃₄,l1_v7), X₁: 21 {O(1)}

Run probabilistic analysis on SCC: [l1_v2]

Run classical analysis on SCC: [l1_v3; l1_v4; l1_v5; l1_v6; l1_v7]

MPRF for transition t₁₄: l1_v3(X₀,X₁) → l1_v5(-X₀,-X₀-X₁) :|: 0 ≤ 11+X₁ ∧ 0 ≤ 10+X₁ ∧ 0 ≤ 9+X₁ ∧ 0 ≤ 1+X₀ ∧ X₀ ≤ 1 ∧ 0 ≤ X₀ ∧ X₁ ≤ 10 ∧ 1 ≤ X₀ of depth 1:

new bound:

110 {O(1)}

MPRF:

• l1_v3: [11-X₁]
• l1_v4: [10+X₀-X₁]
• l1_v5: [10+X₁-X₀]
• l1_v6: [11+X₁]
• l1_v7: [11⋅X₀-X₁]

MPRF for transition t₁₅: l1_v3(X₀,X₁) → l1_v6(-X₀,-X₁) :|: 0 ≤ 11+X₁ ∧ 0 ≤ 10+X₁ ∧ 0 ≤ 9+X₁ ∧ 0 ≤ 1+X₀ ∧ X₀ ≤ 1 ∧ 0 ≤ X₀ ∧ X₁ ≤ 10 ∧ 1 ≤ X₀ of depth 1:

new bound:

2127 {O(1)}

MPRF:

• l1_v3: [211-21⋅X₁]
• l1_v4: [189+X₀-21⋅X₁]
• l1_v5: [189+21⋅X₁-X₀]
• l1_v6: [190+21⋅X₁]
• l1_v7: [21+169⋅X₀-21⋅X₁]

MPRF for transition t₁₇: l1_v5(X₀,X₁) → l1_v3(-X₀,-X₀-X₁) :|: 0 ≤ 11+X₁ ∧ 0 ≤ 1+X₀ ∧ X₀ ≤ 1 ∧ X₀ ≤ 0 ∧ X₁ ≤ 10 ∧ 1+X₀ ≤ 0 of depth 1:

new bound:

116 {O(1)}

MPRF:

• l1_v3: [11+X₀-X₁]
• l1_v4: [12-X₁]
• l1_v5: [12+X₁]
• l1_v6: [11+X₁-X₀]
• l1_v7: [1+11⋅X₀-X₁]

MPRF for transition t₁₈: l1_v5(X₀,X₁) → l1_v4(-X₀,-X₁) :|: 0 ≤ 11+X₁ ∧ 0 ≤ 1+X₀ ∧ X₀ ≤ 1 ∧ X₀ ≤ 0 ∧ X₁ ≤ 10 ∧ 1+X₀ ≤ 0 of depth 1:

new bound:

47132 {O(1)}

MPRF:

• l1_v3: [4810-420⋅X₀-399⋅X₁]
• l1_v4: [4621-X₀-420⋅X₁]
• l1_v5: [4621+420⋅X₁]
• l1_v6: [4201+420⋅X₁]
• l1_v7: [1+4200⋅X₀-420⋅X₁]

MPRF for transition t₂₀: l1_v6(X₀,X₁) → l1_v3(-X₀,-X₀-X₁) :|: 0 ≤ 11+X₁ ∧ 0 ≤ 10+X₁ ∧ 0 ≤ 1+X₀ ∧ X₀ ≤ 1 ∧ X₀ ≤ 0 ∧ X₁ ≤ 10 ∧ 1+X₀ ≤ 0 of depth 1:

new bound:

2313 {O(1)}

MPRF:

• l1_v3: [190+21⋅X₀-21⋅X₁]
• l1_v4: [230-9⋅X₀-20⋅X₁]
• l1_v5: [230+9⋅X₀+20⋅X₁]
• l1_v6: [211+21⋅X₁]
• l1_v7: [250-39⋅X₀-21⋅X₁]

MPRF for transition t₂₃: l1_v7(X₀,X₁) → l1_v5(-X₀,-X₀-X₁) :|: 0 ≤ 11+X₁ ∧ 0 ≤ 10+X₁ ∧ 0 ≤ 1+X₀ ∧ X₀ ≤ 1 ∧ 0 ≤ X₀ ∧ X₁ ≤ 10 ∧ 1 ≤ X₀ of depth 1:

new bound:

2086 {O(1)}

MPRF:

• l1_v3: [201-20⋅X₁]
• l1_v4: [181+20⋅X₀-20⋅X₁]
• l1_v5: [181+20⋅X₁-20⋅X₀]
• l1_v6: [190+20⋅X₁-11⋅X₀]
• l1_v7: [201-20⋅X₁]

MPRF for transition t₂₆: l1_v4(X₀,X₁) → l1_v5(-X₀,-X₀-X₁) :|: 0 ≤ 11+X₁ ∧ 0 ≤ 10+X₁ ∧ 0 ≤ 1+X₀ ∧ X₀ ≤ 1 ∧ 0 ≤ X₀ ∧ X₁ ≤ 10 ∧ 1 ≤ X₀ of depth 1:

new bound:

45366 {O(1)}

MPRF:

• l1_v3: [4369⋅X₀-399⋅X₁]
• l1_v4: [4621-420⋅X₀-420⋅X₁]
• l1_v5: [4600+420⋅X₁]
• l1_v6: [420⋅X₁-189-4369⋅X₀]
• l1_v7: [4180⋅X₀-420⋅X₁]

MPRF for transition t₂₇: l1_v4(X₀,X₁) → l1_v6(-X₀,-X₁) :|: 0 ≤ 11+X₁ ∧ 0 ≤ 10+X₁ ∧ 0 ≤ 1+X₀ ∧ X₀ ≤ 1 ∧ 0 ≤ X₀ ∧ X₁ ≤ 10 ∧ 1 ≤ X₀ of depth 1:

new bound:

106 {O(1)}

MPRF:

• l1_v3: [10-X₁]
• l1_v4: [11-X₁]
• l1_v5: [10+X₁-X₀]
• l1_v6: [10+X₁]
• l1_v7: [10-X₁]

TWN: t₂₁: l1_v6→l1_v7

cycle: [t₂₁: l1_v6→l1_v7; t₂₄: l1_v7→l1_v6]
loop: (X₁ ≤ 10 ∧ 1+X₀ ≤ 0 ∧ 0 ≤ 10+X₁ ∧ 1+X₀ ≤ 0,(X₀,X₁) -> (X₀,X₁)
order: [X₀; X₁]
closed-form:
X₀: X₀
X₁: X₁

Termination: true
Formula:

0 ≤ 10+X₁ ∧ X₁ ≤ 10 ∧ 0 ≤ 1+X₀ ∧ 1+X₀ ≤ 0 ∧ 10 ≤ X₁ ∧ 10+X₁ ≤ 0
∨ 0 ≤ 10+X₁ ∧ X₁ ≤ 10 ∧ 2+X₀ ≤ 0 ∧ 10 ≤ X₁ ∧ 10+X₁ ≤ 0
∨ 0 ≤ 10+X₁ ∧ X₁ ≤ 9 ∧ 0 ≤ 1+X₀ ∧ 1+X₀ ≤ 0 ∧ 10+X₁ ≤ 0
∨ 0 ≤ 10+X₁ ∧ X₁ ≤ 9 ∧ 2+X₀ ≤ 0 ∧ 10+X₁ ≤ 0
∨ X₁ ≤ 10 ∧ 0 ≤ 9+X₁ ∧ 0 ≤ 1+X₀ ∧ 1+X₀ ≤ 0 ∧ 10 ≤ X₁
∨ X₁ ≤ 10 ∧ 0 ≤ 9+X₁ ∧ 2+X₀ ≤ 0 ∧ 10 ≤ X₁
∨ 0 ≤ 9+X₁ ∧ X₁ ≤ 9 ∧ 0 ≤ 1+X₀ ∧ 1+X₀ ≤ 0
∨ 0 ≤ 9+X₁ ∧ X₁ ≤ 9 ∧ 2+X₀ ≤ 0

loop: (X₁ ≤ 10 ∧ 1+X₀ ≤ 0 ∧ 0 ≤ 10+X₁ ∧ 1+X₀ ≤ 0,(X₀,X₁) -> (X₀,X₁)
order: [X₀; X₁]
closed-form:
X₀: X₀
X₁: X₁

Termination: true
Formula:

0 ≤ 10+X₁ ∧ X₁ ≤ 10 ∧ 0 ≤ 1+X₀ ∧ 1+X₀ ≤ 0 ∧ 10 ≤ X₁ ∧ 10+X₁ ≤ 0
∨ 0 ≤ 10+X₁ ∧ X₁ ≤ 10 ∧ 2+X₀ ≤ 0 ∧ 10 ≤ X₁ ∧ 10+X₁ ≤ 0
∨ 0 ≤ 10+X₁ ∧ X₁ ≤ 9 ∧ 0 ≤ 1+X₀ ∧ 1+X₀ ≤ 0 ∧ 10+X₁ ≤ 0
∨ 0 ≤ 10+X₁ ∧ X₁ ≤ 9 ∧ 2+X₀ ≤ 0 ∧ 10+X₁ ≤ 0
∨ X₁ ≤ 10 ∧ 0 ≤ 9+X₁ ∧ 0 ≤ 1+X₀ ∧ 1+X₀ ≤ 0 ∧ 10 ≤ X₁
∨ X₁ ≤ 10 ∧ 0 ≤ 9+X₁ ∧ 2+X₀ ≤ 0 ∧ 10 ≤ X₁
∨ 0 ≤ 9+X₁ ∧ X₁ ≤ 9 ∧ 0 ≤ 1+X₀ ∧ 1+X₀ ≤ 0
∨ 0 ≤ 9+X₁ ∧ X₁ ≤ 9 ∧ 2+X₀ ≤ 0

loop: (X₁ ≤ 10 ∧ 1 ≤ X₀ ∧ 0 ≤ 10+X₁ ∧ 1 ≤ X₀,(X₀,X₁) -> (X₀,X₁)
order: [X₀; X₁]
closed-form:
X₀: X₀
X₁: X₁

Termination: true
Formula:

0 ≤ 10+X₁ ∧ X₁ ≤ 10 ∧ X₀ ≤ 1 ∧ 1 ≤ X₀ ∧ 10 ≤ X₁ ∧ 10+X₁ ≤ 0
∨ 0 ≤ 10+X₁ ∧ X₁ ≤ 10 ∧ 2 ≤ X₀ ∧ 10 ≤ X₁ ∧ 10+X₁ ≤ 0
∨ 0 ≤ 10+X₁ ∧ X₁ ≤ 9 ∧ X₀ ≤ 1 ∧ 1 ≤ X₀ ∧ 10+X₁ ≤ 0
∨ 0 ≤ 10+X₁ ∧ X₁ ≤ 9 ∧ 2 ≤ X₀ ∧ 10+X₁ ≤ 0
∨ X₁ ≤ 10 ∧ 0 ≤ 9+X₁ ∧ X₀ ≤ 1 ∧ 1 ≤ X₀ ∧ 10 ≤ X₁
∨ X₁ ≤ 10 ∧ 0 ≤ 9+X₁ ∧ 2 ≤ X₀ ∧ 10 ≤ X₁
∨ 0 ≤ 9+X₁ ∧ X₁ ≤ 9 ∧ X₀ ≤ 1 ∧ 1 ≤ X₀
∨ 0 ≤ 9+X₁ ∧ X₁ ≤ 9 ∧ 2 ≤ X₀

TWN - Lifting for [21: l1_v6->l1_v7; 24: l1_v7->l1_v6] of 5 {O(1)}

relevant size-bounds w.r.t. t₁₅: l1_v3→l1_v6:
Runtime-bound of t₁₅: 2127 {O(1)}
Results in: 10635 {O(1)}

TWN - Lifting for [21: l1_v6->l1_v7; 24: l1_v7->l1_v6] of 5 {O(1)}

relevant size-bounds w.r.t. t₂₇: l1_v4→l1_v6:
Runtime-bound of t₂₇: 106 {O(1)}
Results in: 530 {O(1)}

TWN - Lifting for [21: l1_v6->l1_v7; 24: l1_v7->l1_v6] of 5 {O(1)}

relevant size-bounds w.r.t. t₃₃: l1_v2→l1_v7:
Runtime-bound of t₃₃: 1 {O(1)}
Results in: 5 {O(1)}

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:121705 {O(1)}
g₀: 1 {O(1)}
g₁₀: 2 {O(1)}
g₁₃: 2 {O(1)}
g₁₆: 2237 {O(1)}
g₁₉: 47248 {O(1)}
g₂₂: 13483 {O(1)}
g₂₅: 13256 {O(1)}
g₂₈: 45472 {O(1)}
g₃₁: 2 {O(1)}
g₃₄: 2 {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₀,l1), X₀: 1 {O(1)}
(g₀,l1), X₁: X₁ {O(n)}
(g₁₀,l1_v1), X₀: 1 {O(1)}
(g₁₀,l1_v1), X₁: 2⋅X₁+1 {O(n)}
(g₁₀,l1_v2), X₀: 1 {O(1)}
(g₁₀,l1_v2), X₁: X₁ {O(n)}
(g₁₃,l1_v3), X₀: 2 {O(1)}
(g₁₃,l1_v3), X₁: 0 {O(1)}
(g₁₃,l1_v4), X₀: 2 {O(1)}
(g₁₃,l1_v4), X₁: 0 {O(1)}
(g₁₆,l1_v5), X₀: 2 {O(1)}
(g₁₆,l1_v5), X₁: 21 {O(1)}
(g₁₆,l1_v6), X₀: 2 {O(1)}
(g₁₆,l1_v6), X₁: 21 {O(1)}
(g₁₉,l1_v3), X₀: 2 {O(1)}
(g₁₉,l1_v3), X₁: 23 {O(1)}
(g₁₉,l1_v4), X₀: 2 {O(1)}
(g₁₉,l1_v4), X₁: 23 {O(1)}
(g₂₂,l1_v3), X₀: 2 {O(1)}
(g₂₂,l1_v3), X₁: 21 {O(1)}
(g₂₂,l1_v7), X₀: 2 {O(1)}
(g₂₂,l1_v7), X₁: 21 {O(1)}
(g₂₅,l1_v5), X₀: 2 {O(1)}
(g₂₅,l1_v5), X₁: 21 {O(1)}
(g₂₅,l1_v6), X₀: 2 {O(1)}
(g₂₅,l1_v6), X₁: 21 {O(1)}
(g₂₈,l1_v5), X₀: 2 {O(1)}
(g₂₈,l1_v5), X₁: 21 {O(1)}
(g₂₈,l1_v6), X₀: 2 {O(1)}
(g₂₈,l1_v6), X₁: 21 {O(1)}
(g₃₁,l1_v3), X₀: 2 {O(1)}
(g₃₁,l1_v3), X₁: 23 {O(1)}
(g₃₁,l1_v4), X₀: 2 {O(1)}
(g₃₁,l1_v4), X₁: 23 {O(1)}
(g₃₄,l1_v3), X₀: 2 {O(1)}
(g₃₄,l1_v3), X₁: 21 {O(1)}
(g₃₄,l1_v7), X₀: 2 {O(1)}
(g₃₄,l1_v7), X₁: 21 {O(1)}

Run probabilistic analysis on SCC: [l1_v3; l1_v4; l1_v5; l1_v6; l1_v7]

CFR: Improvement to new bound with the following program:

method: PartialEvaluationProbabilistic new bound:

O(1)

cfr-program:

Start: l0
Program_Vars: X₀, X₁
Temp_Vars:
Locations: l0, l1, l1_v1, l1_v2, l1_v3, l1_v4, l1_v5, l1_v6, l1_v7
Transitions:
g₀:l0(X₀,X₁) → t₁:l1(1,X₁) :|:
g₁₀:l1(X₀,X₁) → [1/2]:t₈:l1_v1(-X₀,-X₀-X₁) :+: [1/2]:t₉:l1_v2(-X₀,-X₁) :|: X₁ ≤ 10 ∧ 1 ≤ X₀ ∧ 0 ≤ 1+X₀ ∧ X₀ ≤ 1
g₁₃:l1(X₀,X₁) → [1/2]:t₁₁:l1_v3(-X₀,-X₀-X₁) :+: [1/2]:t₁₂:l1_v4(-X₀,-X₁) :|: X₁ ≤ 10 ∧ 1+X₀ ≤ 0 ∧ 0 ≤ 1+X₀ ∧ X₀ ≤ 1
g₁₆:l1_v3(X₀,X₁) → [1/2]:t₁₄:l1_v5(-X₀,-X₀-X₁) :+: [1/2]:t₁₅:l1_v6(-X₀,-X₁) :|: X₁ ≤ 10 ∧ 1 ≤ X₀ ∧ 0 ≤ 11+X₁ ∧ 0 ≤ 10+X₁ ∧ 0 ≤ 9+X₁ ∧ 0 ≤ 1+X₀ ∧ X₀ ≤ 1 ∧ 0 ≤ X₀
g₁₉:l1_v5(X₀,X₁) → [1/2]:t₁₇:l1_v3(-X₀,-X₀-X₁) :+: [1/2]:t₁₈:l1_v4(-X₀,-X₁) :|: X₁ ≤ 10 ∧ 1+X₀ ≤ 0 ∧ 0 ≤ 11+X₁ ∧ 0 ≤ 1+X₀ ∧ X₀ ≤ 1 ∧ X₀ ≤ 0
g₂₂:l1_v6(X₀,X₁) → [1/2]:t₂₀:l1_v3(-X₀,-X₀-X₁) :+: [1/2]:t₂₁:l1_v7(-X₀,-X₁) :|: X₁ ≤ 10 ∧ 1+X₀ ≤ 0 ∧ 0 ≤ 11+X₁ ∧ 0 ≤ 10+X₁ ∧ 0 ≤ 1+X₀ ∧ X₀ ≤ 1 ∧ X₀ ≤ 0
g₂₅:l1_v7(X₀,X₁) → [1/2]:t₂₃:l1_v5(-X₀,-X₀-X₁) :+: [1/2]:t₂₄:l1_v6(-X₀,-X₁) :|: X₁ ≤ 10 ∧ 1 ≤ X₀ ∧ 0 ≤ 11+X₁ ∧ 0 ≤ 10+X₁ ∧ 0 ≤ 1+X₀ ∧ X₀ ≤ 1 ∧ 0 ≤ X₀
g₂₈:l1_v4(X₀,X₁) → [1/2]:t₂₆:l1_v5(-X₀,-X₀-X₁) :+: [1/2]:t₂₇:l1_v6(-X₀,-X₁) :|: X₁ ≤ 10 ∧ 1 ≤ X₀ ∧ 0 ≤ 11+X₁ ∧ 0 ≤ 10+X₁ ∧ 0 ≤ 1+X₀ ∧ X₀ ≤ 1 ∧ 0 ≤ X₀
g₃₁:l1_v1(X₀,X₁) → [1/2]:t₂₉:l1_v3(-X₀,-X₀-X₁) :+: [1/2]:t₃₀:l1_v4(-X₀,-X₁) :|: X₁ ≤ 10 ∧ 1+X₀ ≤ 0 ∧ 0 ≤ 11+X₁ ∧ 0 ≤ 1+X₀ ∧ X₀ ≤ 1 ∧ X₀ ≤ 0
g₃₄:l1_v2(X₀,X₁) → [1/2]:t₃₂:l1_v3(-X₀,-X₀-X₁) :+: [1/2]:t₃₃:l1_v7(-X₀,-X₁) :|: X₁ ≤ 10 ∧ 1+X₀ ≤ 0 ∧ 0 ≤ 11+X₁ ∧ 0 ≤ 10+X₁ ∧ 0 ≤ 1+X₀ ∧ X₀ ≤ 1 ∧ X₀ ≤ 0

Results of Probabilistic Analysis

All Bounds

Timebounds

Overall timebound:121705 {O(1)}
g₀: 1 {O(1)}
g₁₀: 2 {O(1)}
g₁₃: 2 {O(1)}
g₁₆: 2237 {O(1)}
g₁₉: 47248 {O(1)}
g₂₂: 13483 {O(1)}
g₂₅: 13256 {O(1)}
g₂₈: 45472 {O(1)}
g₃₁: 2 {O(1)}
g₃₄: 2 {O(1)}

Costbounds

Overall costbound: 243409 {O(1)}
g₀: 1 {O(1)}
g₁₀: 4 {O(1)}
g₁₃: 4 {O(1)}
g₁₆: 4474 {O(1)}
g₁₉: 94496 {O(1)}
g₂₂: 26966 {O(1)}
g₂₅: 26512 {O(1)}
g₂₈: 90944 {O(1)}
g₃₁: 4 {O(1)}
g₃₄: 4 {O(1)}

Sizebounds

(g₀,l1), X₀: 1 {O(1)}
(g₀,l1), X₁: X₁ {O(n)}
(g₁₀,l1_v1), X₀: 1 {O(1)}
(g₁₀,l1_v1), X₁: 2⋅X₁+1 {O(n)}
(g₁₀,l1_v2), X₀: 1 {O(1)}
(g₁₀,l1_v2), X₁: X₁ {O(n)}
(g₁₃,l1_v3), X₀: 2 {O(1)}
(g₁₃,l1_v3), X₁: 0 {O(1)}
(g₁₃,l1_v4), X₀: 2 {O(1)}
(g₁₃,l1_v4), X₁: 0 {O(1)}
(g₁₆,l1_v5), X₀: 2 {O(1)}
(g₁₆,l1_v5), X₁: 21 {O(1)}
(g₁₆,l1_v6), X₀: 2 {O(1)}
(g₁₆,l1_v6), X₁: 21 {O(1)}
(g₁₉,l1_v3), X₀: 2 {O(1)}
(g₁₉,l1_v3), X₁: 23 {O(1)}
(g₁₉,l1_v4), X₀: 2 {O(1)}
(g₁₉,l1_v4), X₁: 23 {O(1)}
(g₂₂,l1_v3), X₀: 2 {O(1)}
(g₂₂,l1_v3), X₁: 21 {O(1)}
(g₂₂,l1_v7), X₀: 2 {O(1)}
(g₂₂,l1_v7), X₁: 21 {O(1)}
(g₂₅,l1_v5), X₀: 2 {O(1)}
(g₂₅,l1_v5), X₁: 21 {O(1)}
(g₂₅,l1_v6), X₀: 2 {O(1)}
(g₂₅,l1_v6), X₁: 21 {O(1)}
(g₂₈,l1_v5), X₀: 2 {O(1)}
(g₂₈,l1_v5), X₁: 21 {O(1)}
(g₂₈,l1_v6), X₀: 2 {O(1)}
(g₂₈,l1_v6), X₁: 21 {O(1)}
(g₃₁,l1_v3), X₀: 2 {O(1)}
(g₃₁,l1_v3), X₁: 23 {O(1)}
(g₃₁,l1_v4), X₀: 2 {O(1)}
(g₃₁,l1_v4), X₁: 23 {O(1)}
(g₃₄,l1_v3), X₀: 2 {O(1)}
(g₃₄,l1_v3), X₁: 21 {O(1)}
(g₃₄,l1_v7), X₀: 2 {O(1)}
(g₃₄,l1_v7), X₁: 21 {O(1)}