Inferring Expected Runtimes Using Sizes

KoAT2 Proof WORST_CASE( ?, 10+4*(1+2*Arg_0)*Arg_0+6*Arg_0+8*Arg_2 {O(n^2)})

Initial Complexity Problem (after preprocessing)

Start:start0
Program_Vars:Arg_0, Arg_1, Arg_2, Arg_3, Arg_4, Arg_5
Temp_Vars:
Locations:lbl52, lbl72, start, start0, stop
Transitions:
lbl52(Arg_0,Arg_1,Arg_2,Arg_3,Arg_4,Arg_5) -> lbl52(Arg_0,Uniform (-1, 0),Arg_2,Arg_3,Arg_4,Arg_5) :|: 1<=Arg_3 && 1<=Arg_1 && 0<=Arg_1 && Arg_3<=Arg_0 && Arg_5<=Arg_0 && Arg_0<=Arg_5 && Arg_5<=Arg_0 && 1<=Arg_5 && 2<=Arg_3+Arg_5 && Arg_3<=Arg_5 && 1<=Arg_1+Arg_5 && 2<=Arg_0+Arg_5 && Arg_0<=Arg_5 && Arg_3<=Arg_0 && 1<=Arg_3 && 1<=Arg_1+Arg_3 && 2<=Arg_0+Arg_3 && 0<=Arg_1 && 1<=Arg_0+Arg_1 && 1<=Arg_0 && Arg_5<=Arg_0 && 1<=Arg_5 && 2<=Arg_3+Arg_5 && Arg_3<=Arg_5 && 1<=Arg_1+Arg_5 && 2<=Arg_0+Arg_5 && Arg_0<=Arg_5 && Arg_3<=Arg_0 && 1<=Arg_3 && 1<=Arg_1+Arg_3 && 2<=Arg_0+Arg_3 && 0<=Arg_1 && 1<=Arg_0+Arg_1 && 1<=Arg_0
lbl52(Arg_0,Arg_1,Arg_2,Arg_3,Arg_4,Arg_5) -> lbl72(Arg_0,Arg_5,Arg_2,Arg_3-1,Arg_4,Arg_5) :|: 1<=Arg_3 && Arg_3<=Arg_0 && Arg_1<=0 && 0<=Arg_1 && Arg_5<=Arg_0 && Arg_0<=Arg_5 && Arg_5<=Arg_0 && 1<=Arg_5 && 2<=Arg_3+Arg_5 && Arg_3<=Arg_5 && 1<=Arg_1+Arg_5 && 2<=Arg_0+Arg_5 && Arg_0<=Arg_5 && Arg_3<=Arg_0 && 1<=Arg_3 && 1<=Arg_1+Arg_3 && 2<=Arg_0+Arg_3 && 0<=Arg_1 && 1<=Arg_0+Arg_1 && 1<=Arg_0 && Arg_5<=Arg_0 && 1<=Arg_5 && 2<=Arg_3+Arg_5 && Arg_3<=Arg_5 && 1<=Arg_1+Arg_5 && 2<=Arg_0+Arg_5 && Arg_0<=Arg_5 && Arg_3<=Arg_0 && 1<=Arg_3 && 1<=Arg_1+Arg_3 && 2<=Arg_0+Arg_3 && 0<=Arg_1 && 1<=Arg_0+Arg_1 && 1<=Arg_0
lbl72(Arg_0,Arg_1,Arg_2,Arg_3,Arg_4,Arg_5) -> stop(Arg_0,Arg_1,Arg_2,Arg_3,Arg_4,Arg_5) :|: 1<=Arg_0 && Arg_3<=0 && 0<=Arg_3 && Arg_5<=Arg_0 && Arg_0<=Arg_5 && Arg_1<=Arg_0 && Arg_0<=Arg_1 && Arg_5<=Arg_1 && Arg_5<=Arg_0 && 1<=Arg_5 && 1<=Arg_3+Arg_5 && 1+Arg_3<=Arg_5 && 2<=Arg_1+Arg_5 && Arg_1<=Arg_5 && 2<=Arg_0+Arg_5 && Arg_0<=Arg_5 && 1+Arg_3<=Arg_1 && 1+Arg_3<=Arg_0 && 0<=Arg_3 && 1<=Arg_1+Arg_3 && 1<=Arg_0+Arg_3 && Arg_1<=Arg_0 && 1<=Arg_1 && 2<=Arg_0+Arg_1 && Arg_0<=Arg_1 && 1<=Arg_0 && Arg_5<=Arg_1 && Arg_5<=Arg_0 && 1<=Arg_5 && 1<=Arg_3+Arg_5 && 1+Arg_3<=Arg_5 && 2<=Arg_1+Arg_5 && Arg_1<=Arg_5 && 2<=Arg_0+Arg_5 && Arg_0<=Arg_5 && 1+Arg_3<=Arg_1 && 1+Arg_3<=Arg_0 && 0<=Arg_3 && 1<=Arg_1+Arg_3 && 1<=Arg_0+Arg_3 && Arg_1<=Arg_0 && 1<=Arg_1 && 2<=Arg_0+Arg_1 && Arg_0<=Arg_1 && 1<=Arg_0
lbl72(Arg_0,Arg_1,Arg_2,Arg_3,Arg_4,Arg_5) -> lbl52(Arg_0,Arg_1-1,Arg_2,Arg_3,Arg_4,Arg_5) :|: 1<=Arg_3 && 1<=Arg_0 && 0<=Arg_3 && Arg_3+1<=Arg_0 && Arg_5<=Arg_0 && Arg_0<=Arg_5 && Arg_1<=Arg_0 && Arg_0<=Arg_1 && Arg_5<=Arg_1 && Arg_5<=Arg_0 && 1<=Arg_5 && 1<=Arg_3+Arg_5 && 1+Arg_3<=Arg_5 && 2<=Arg_1+Arg_5 && Arg_1<=Arg_5 && 2<=Arg_0+Arg_5 && Arg_0<=Arg_5 && 1+Arg_3<=Arg_1 && 1+Arg_3<=Arg_0 && 0<=Arg_3 && 1<=Arg_1+Arg_3 && 1<=Arg_0+Arg_3 && Arg_1<=Arg_0 && 1<=Arg_1 && 2<=Arg_0+Arg_1 && Arg_0<=Arg_1 && 1<=Arg_0 && Arg_5<=Arg_1 && Arg_5<=Arg_0 && 1<=Arg_5 && 1<=Arg_3+Arg_5 && 1+Arg_3<=Arg_5 && 2<=Arg_1+Arg_5 && Arg_1<=Arg_5 && 2<=Arg_0+Arg_5 && Arg_0<=Arg_5 && 1+Arg_3<=Arg_1 && 1+Arg_3<=Arg_0 && 0<=Arg_3 && 1<=Arg_1+Arg_3 && 1<=Arg_0+Arg_3 && Arg_1<=Arg_0 && 1<=Arg_1 && 2<=Arg_0+Arg_1 && Arg_0<=Arg_1 && 1<=Arg_0
start0(Arg_0,Arg_1,Arg_2,Arg_3,Arg_4,Arg_5) -> start(Arg_0,Arg_2,Arg_2,Arg_4,Arg_4,Arg_0)
start0(Arg_0,Arg_1,Arg_2,Arg_3,Arg_4,Arg_5) -{2}> stop(Arg_0,Arg_2,Arg_2,Arg_0,Arg_4,Arg_0) :|: Arg_0<=0 && 0<=0 && 0<=0 && 0<=0 && 0<=0 && 0<=0 && 0<=0 && 0<=0 && 0<=0 && 0<=0 && 0<=0 && 0<=0 && 0<=0
start0(Arg_0,Arg_1,Arg_2,Arg_3,Arg_4,Arg_5) -{2}> lbl52(Arg_0,Arg_2-1,Arg_2,Arg_0,Arg_4,Arg_0) :|: 1<=Arg_0 && 1<=Arg_2 && 0<=0 && 0<=0 && 0<=0 && 0<=0 && 0<=0 && 0<=0 && 0<=0 && 0<=0 && 0<=0 && 0<=0 && 0<=0 && 0<=0
start0(Arg_0,Arg_1,Arg_2,Arg_3,Arg_4,Arg_5) -{2}> lbl72(Arg_0,Arg_0,Arg_2,Arg_0-1,Arg_4,Arg_0) :|: 1<=Arg_0 && Arg_2<=0 && 0<=0 && 0<=0 && 0<=0 && 0<=0 && 0<=0 && 0<=0 && 0<=0 && 0<=0 && 0<=0 && 0<=0 && 0<=0 && 0<=0

G lbl52 lbl52 lbl52->lbl52 t₄ ∈ g₄ η (Arg_1) = Uniform (-1, 0) τ = 1<=Arg_3 && 1<=Arg_1 && 0<=Arg_1 && Arg_3<=Arg_0 && Arg_5<=Arg_0 && Arg_0<=Arg_5 lbl72 lbl72 lbl52->lbl72 t₅ ∈ g₅ η (Arg_1) = Arg_5 η (Arg_3) = Arg_3-1 τ = 1<=Arg_3 && Arg_3<=Arg_0 && Arg_1<=0 && 0<=Arg_1 && Arg_5<=Arg_0 && Arg_0<=Arg_5 lbl72->lbl52 t₇ ∈ g₇ η (Arg_1) = Arg_1-1 τ = 1<=Arg_3 && 1<=Arg_0 && 0<=Arg_3 && Arg_3+1<=Arg_0 && Arg_5<=Arg_0 && Arg_0<=Arg_5 && Arg_1<=Arg_0 && Arg_0<=Arg_1 stop stop lbl72->stop t₆ ∈ g₆ τ = 1<=Arg_0 && Arg_3<=0 && 0<=Arg_3 && Arg_5<=Arg_0 && Arg_0<=Arg_5 && Arg_1<=Arg_0 && Arg_0<=Arg_1 start start start0 start0 start0->lbl52 t₁₁ ∈ g₁₁ η (Arg_1) = Arg_2-1 η (Arg_3) = Arg_0 η (Arg_5) = Arg_0 τ = 1<=Arg_0 && 1<=Arg_2 && 0<=0 && 0<=0 && 0<=0 && 0<=0 && 0<=0 && 0<=0 {2} start0->lbl72 t₁₂ ∈ g₁₂ η (Arg_1) = Arg_0 η (Arg_3) = Arg_0-1 η (Arg_5) = Arg_0 τ = 1<=Arg_0 && Arg_2<=0 && 0<=0 && 0<=0 && 0<=0 && 0<=0 && 0<=0 && 0<=0 {2} start0->start t₉ ∈ g₉ η (Arg_1) = Arg_2 η (Arg_3) = Arg_4 η (Arg_5) = Arg_0 start0->stop t₁₀ ∈ g₁₀ η (Arg_1) = Arg_2 η (Arg_3) = Arg_0 η (Arg_5) = Arg_0 τ = Arg_0<=0 && 0<=0 && 0<=0 && 0<=0 && 0<=0 && 0<=0 && 0<=0 {2}

Timebounds:

Overall timebound:inf {Infinity}
4,4: lbl52->lbl52: inf {Infinity}
5,5: lbl52->lbl72: 2*max([0, Arg_0]) {O(n)}
6,6: lbl72->stop: 1 {O(1)}
7,7: lbl72->lbl52: max([(-2)+2*Arg_0, 0])+max([0, 2*Arg_0]) {O(n)}
9,9: start0->start: 1 {O(1)}
10,10: start0->stop: 1 {O(1)}
11,11: start0->lbl52: 1 {O(1)}
12,12: start0->lbl72: 1 {O(1)}

Expected Timebounds:

Overall expected timebound: 4*(1+2*Arg_0)*Arg_0+6*Arg_0+7+8*Arg_2 {O(n^2)}
4: lbl52->[1:lbl52]: 4*(1+2*Arg_0)*Arg_0+8*Arg_2 {O(n^2)}
5: lbl52->[1:lbl72]: 2*Arg_0 {O(n)}
6: lbl72->[1:stop]: 1 {O(1)}
7: lbl72->[1:lbl52]: 2+4*Arg_0 {O(n)}
9: start0->[1:start]: 1 {O(1)}
10: start0->[1:stop]: 1 {O(1)}
11: start0->[1:lbl52]: 1 {O(1)}
12: start0->[1:lbl72]: 1 {O(1)}

Costbounds:

Overall costbound: inf {Infinity}
4,4: lbl52->lbl52: inf {Infinity}
5,5: lbl52->lbl72: inf {Infinity}
6,6: lbl72->stop: inf {Infinity}
7,7: lbl72->lbl52: inf {Infinity}
9,9: start0->start: inf {Infinity}
10,10: start0->stop: inf {Infinity}
11,11: start0->lbl52: inf {Infinity}
12,12: start0->lbl72: inf {Infinity}

Expected Costbounds:

Overall expected costbound: 10+4*(1+2*Arg_0)*Arg_0+6*Arg_0+8*Arg_2 {O(n^2)}
4: lbl52->[1:lbl52]: 4*(1+2*Arg_0)*Arg_0+8*Arg_2 {O(n^2)}
5: lbl52->[1:lbl72]: 2*Arg_0 {O(n)}
6: lbl72->[1:stop]: 1 {O(1)}
7: lbl72->[1:lbl52]: 2+4*Arg_0 {O(n)}
9: start0->[1:start]: 1 {O(1)}
10: start0->[1:stop]: 2 {O(1)}
11: start0->[1:lbl52]: 2 {O(1)}
12: start0->[1:lbl72]: 2 {O(1)}

Sizebounds:

4,4: lbl52->lbl52, Arg_0: Arg_0 {O(n)}
4,4: lbl52->lbl52, Arg_1: max([(-1)+Arg_0, Arg_2]) {O(n)}
4,4: lbl52->lbl52, Arg_2: max([0, Arg_2]) {O(n)}
4,4: lbl52->lbl52, Arg_3: Arg_0 {O(n)}
4,4: lbl52->lbl52, Arg_4: Arg_4 {O(n)}
4,4: lbl52->lbl52, Arg_5: Arg_0 {O(n)}
5,5: lbl52->lbl72, Arg_0: Arg_0 {O(n)}
5,5: lbl52->lbl72, Arg_1: Arg_0 {O(n)}
5,5: lbl52->lbl72, Arg_2: max([0, Arg_2]) {O(n)}
5,5: lbl52->lbl72, Arg_3: Arg_0 {O(n)}
5,5: lbl52->lbl72, Arg_4: Arg_4 {O(n)}
5,5: lbl52->lbl72, Arg_5: Arg_0 {O(n)}
6,6: lbl72->stop, Arg_0: Arg_0 {O(n)}
6,6: lbl72->stop, Arg_1: Arg_0 {O(n)}
6,6: lbl72->stop, Arg_2: max([0, Arg_2]) {O(n)}
6,6: lbl72->stop, Arg_3: 0 {O(1)}
6,6: lbl72->stop, Arg_4: Arg_4 {O(n)}
6,6: lbl72->stop, Arg_5: Arg_0 {O(n)}
7,7: lbl72->lbl52, Arg_0: Arg_0 {O(n)}
7,7: lbl72->lbl52, Arg_1: (-1)+Arg_0 {O(n)}
7,7: lbl72->lbl52, Arg_2: max([0, Arg_2]) {O(n)}
7,7: lbl72->lbl52, Arg_3: Arg_0 {O(n)}
7,7: lbl72->lbl52, Arg_4: Arg_4 {O(n)}
7,7: lbl72->lbl52, Arg_5: Arg_0 {O(n)}
9,9: start0->start, Arg_0: Arg_0 {O(n)}
9,9: start0->start, Arg_1: Arg_2 {O(n)}
9,9: start0->start, Arg_2: Arg_2 {O(n)}
9,9: start0->start, Arg_3: Arg_4 {O(n)}
9,9: start0->start, Arg_4: Arg_4 {O(n)}
9,9: start0->start, Arg_5: Arg_0 {O(n)}
10,10: start0->stop, Arg_0: 0 {O(1)}
10,10: start0->stop, Arg_1: Arg_2 {O(n)}
10,10: start0->stop, Arg_2: Arg_2 {O(n)}
10,10: start0->stop, Arg_3: 0 {O(1)}
10,10: start0->stop, Arg_4: Arg_4 {O(n)}
10,10: start0->stop, Arg_5: 0 {O(1)}
11,11: start0->lbl52, Arg_0: Arg_0 {O(n)}
11,11: start0->lbl52, Arg_1: Arg_2 {O(n)}
11,11: start0->lbl52, Arg_2: Arg_2 {O(n)}
11,11: start0->lbl52, Arg_3: Arg_0 {O(n)}
11,11: start0->lbl52, Arg_4: Arg_4 {O(n)}
11,11: start0->lbl52, Arg_5: Arg_0 {O(n)}
12,12: start0->lbl72, Arg_0: Arg_0 {O(n)}
12,12: start0->lbl72, Arg_1: Arg_0 {O(n)}
12,12: start0->lbl72, Arg_2: 0 {O(1)}
12,12: start0->lbl72, Arg_3: Arg_0 {O(n)}
12,12: start0->lbl72, Arg_4: Arg_4 {O(n)}
12,12: start0->lbl72, Arg_5: Arg_0 {O(n)}

ExpSizeBounds:

(4: lbl52->[1:lbl52], lbl52), Arg_0: Arg_0 {O(n)}
(4: lbl52->[1:lbl52], lbl52), Arg_1: max([1+Arg_0, Arg_2]) {O(n)}
(4: lbl52->[1:lbl52], lbl52), Arg_2: Arg_2 {O(n)}
(4: lbl52->[1:lbl52], lbl52), Arg_3: Arg_0 {O(n)}
(4: lbl52->[1:lbl52], lbl52), Arg_4: Arg_4 {O(n)}
(4: lbl52->[1:lbl52], lbl52), Arg_5: Arg_0 {O(n)}
(5: lbl52->[1:lbl72], lbl72), Arg_0: Arg_0 {O(n)}
(5: lbl52->[1:lbl72], lbl72), Arg_1: Arg_0 {O(n)}
(5: lbl52->[1:lbl72], lbl72), Arg_2: Arg_2 {O(n)}
(5: lbl52->[1:lbl72], lbl72), Arg_3: Arg_0 {O(n)}
(5: lbl52->[1:lbl72], lbl72), Arg_4: Arg_4 {O(n)}
(5: lbl52->[1:lbl72], lbl72), Arg_5: Arg_0 {O(n)}
(6: lbl72->[1:stop], stop), Arg_0: Arg_0 {O(n)}
(6: lbl72->[1:stop], stop), Arg_1: Arg_0 {O(n)}
(6: lbl72->[1:stop], stop), Arg_2: Arg_2 {O(n)}
(6: lbl72->[1:stop], stop), Arg_3: 0 {O(1)}
(6: lbl72->[1:stop], stop), Arg_4: Arg_4 {O(n)}
(6: lbl72->[1:stop], stop), Arg_5: Arg_0 {O(n)}
(7: lbl72->[1:lbl52], lbl52), Arg_0: Arg_0 {O(n)}
(7: lbl72->[1:lbl52], lbl52), Arg_1: 1+Arg_0 {O(n)}
(7: lbl72->[1:lbl52], lbl52), Arg_2: Arg_2 {O(n)}
(7: lbl72->[1:lbl52], lbl52), Arg_3: Arg_0 {O(n)}
(7: lbl72->[1:lbl52], lbl52), Arg_4: Arg_4 {O(n)}
(7: lbl72->[1:lbl52], lbl52), Arg_5: Arg_0 {O(n)}
(9: start0->[1:start], start), Arg_0: Arg_0 {O(n)}
(9: start0->[1:start], start), Arg_1: Arg_2 {O(n)}
(9: start0->[1:start], start), Arg_2: Arg_2 {O(n)}
(9: start0->[1:start], start), Arg_3: Arg_4 {O(n)}
(9: start0->[1:start], start), Arg_4: Arg_4 {O(n)}
(9: start0->[1:start], start), Arg_5: Arg_0 {O(n)}
(10: start0->[1:stop], stop), Arg_0: Arg_0 {O(n)}
(10: start0->[1:stop], stop), Arg_1: Arg_2 {O(n)}
(10: start0->[1:stop], stop), Arg_2: Arg_2 {O(n)}
(10: start0->[1:stop], stop), Arg_3: Arg_0 {O(n)}
(10: start0->[1:stop], stop), Arg_4: Arg_4 {O(n)}
(10: start0->[1:stop], stop), Arg_5: Arg_0 {O(n)}
(11: start0->[1:lbl52], lbl52), Arg_0: Arg_0 {O(n)}
(11: start0->[1:lbl52], lbl52), Arg_1: Arg_2 {O(n)}
(11: start0->[1:lbl52], lbl52), Arg_2: Arg_2 {O(n)}
(11: start0->[1:lbl52], lbl52), Arg_3: Arg_0 {O(n)}
(11: start0->[1:lbl52], lbl52), Arg_4: Arg_4 {O(n)}
(11: start0->[1:lbl52], lbl52), Arg_5: Arg_0 {O(n)}
(12: start0->[1:lbl72], lbl72), Arg_0: Arg_0 {O(n)}
(12: start0->[1:lbl72], lbl72), Arg_1: Arg_0 {O(n)}
(12: start0->[1:lbl72], lbl72), Arg_2: Arg_2 {O(n)}
(12: start0->[1:lbl72], lbl72), Arg_3: Arg_0 {O(n)}
(12: start0->[1:lbl72], lbl72), Arg_4: Arg_4 {O(n)}
(12: start0->[1:lbl72], lbl72), Arg_5: Arg_0 {O(n)}