Inferring Expected Runtimes Using Sizes

KoAT2 Proof WORST_CASE( ?, (2*(2*max([max([1+Arg_1, 12]), 2+Arg_1])+24*(1+Arg_0)+3/2+Arg_1)+24)*(2+24*(1+Arg_0))+3+12*(1+Arg_0) {O(n^2)})

Initial Complexity Problem (after preprocessing)

Start:f
Program_Vars:Arg_0, Arg_1
Temp_Vars:
Locations:f, g, h, i, stop
Transitions:
f(Arg_0,Arg_1) -{0}> g(Arg_0,Arg_1)
h(Arg_0,Arg_1) -{0}> i(Arg_0-1,Arg_1) :|: 10<Arg_1
h(Arg_0,Arg_1) -> g(Arg_0,Arg_1) :|: Arg_1<=10
i(Arg_0,Arg_1) -> stop(Arg_0,Arg_1) :|: Arg_0<5 && 11<=Arg_1 && 11<=Arg_1
i(Arg_0,Arg_1) -> g(Arg_0,Arg_1) :|: 5<=Arg_0 && 11<=Arg_1 && 11<=Arg_1
f(Arg_0,Arg_1) -{0}> 1/2:h(Arg_0,Arg_1+2) :+: 1/2:h(Arg_0,Arg_1-1)
h(Arg_0,Arg_1) -> 1/2:h(Arg_0,Arg_1+2) :+: 1/2:h(Arg_0,Arg_1-1) :|: Arg_1<=10
i(Arg_0,Arg_1) -> 1/2:h(Arg_0,Arg_1+2) :+: 1/2:h(Arg_0,Arg_1-1) :|: 5<=Arg_0 && 11<=Arg_1 && 11<=Arg_1

G f f g g f->g t₀ ∈ g₀ {0} h h f->h t₇ ∈ g₆ p = 1/2 η (Arg_1) = Arg_1+2 {0} f->h t₈ ∈ g₆ p = 1/2 η (Arg_1) = Arg_1-1 {0} h->g t₄ ∈ g₃ τ = Arg_1<=10 h->h t₉ ∈ g₇ p = 1/2 η (Arg_1) = Arg_1+2 τ = Arg_1<=10 h->h t₁₀ ∈ g₇ p = 1/2 η (Arg_1) = Arg_1-1 τ = Arg_1<=10 i i h->i t₃ ∈ g₂ η (Arg_0) = Arg_0-1 τ = 10<Arg_1 {0} i->g t₆ ∈ g₅ τ = 5<=Arg_0 i->h t₁₁ ∈ g₈ p = 1/2 η (Arg_1) = Arg_1+2 τ = 5<=Arg_0 i->h t₁₂ ∈ g₈ p = 1/2 η (Arg_1) = Arg_1-1 τ = 5<=Arg_0 stop stop i->stop t₅ ∈ g₄ τ = Arg_0<5

Timebounds:

Overall timebound:inf {Infinity}
0,0: f->g: 1 {O(1)}
7,6: f->h: 1 {O(1)}
8,6: f->h: 1 {O(1)}
3,2: h->i: 24*max([(-1)+Arg_0, 0])+6 {O(n)}
4,3: h->g: 1 {O(1)}
9,7: h->h: inf {Infinity}
10,7: h->h: inf {Infinity}
5,4: i->stop: 1 {O(1)}
6,5: i->g: 1 {O(1)}
11,8: i->h: 6*max([(-1)+Arg_0, 0]) {O(n)}
12,8: i->h: 6*max([(-1)+Arg_0, 0]) {O(n)}

Expected Timebounds:

Overall expected timebound: (2*(2*max([max([1+Arg_1, 12]), 2+Arg_1])+24*(1+Arg_0)+3/2+Arg_1)+24)*(2+24*(1+Arg_0))+11+36*(1+Arg_0) {O(n^2)}
0: f->[1:g]: 1 {O(1)}
2: h->[1:i]: 24*(1+Arg_0)+6 {O(n)}
3: h->[1:g]: 1 {O(1)}
4: i->[1:stop]: 1 {O(1)}
5: i->[1:g]: 1 {O(1)}
6: f->[1/2:h; 1/2:h]: 1 {O(1)}
7: h->[1/2:h; 1/2:h]: (2*(2*max([max([1+Arg_1, 12]), 2+Arg_1])+24*(1+Arg_0)+3/2+Arg_1)+24)*(2+24*(1+Arg_0)) {O(n^2)}
8: i->[1/2:h; 1/2:h]: 12*(1+Arg_0) {O(n)}

Costbounds:

Overall costbound: inf {Infinity}
0,0: f->g: inf {Infinity}
7,6: f->h: inf {Infinity}
8,6: f->h: inf {Infinity}
3,2: h->i: inf {Infinity}
4,3: h->g: inf {Infinity}
9,7: h->h: inf {Infinity}
10,7: h->h: inf {Infinity}
5,4: i->stop: inf {Infinity}
6,5: i->g: inf {Infinity}
11,8: i->h: inf {Infinity}
12,8: i->h: inf {Infinity}

Expected Costbounds:

Overall expected costbound: (2*(2*max([max([1+Arg_1, 12]), 2+Arg_1])+24*(1+Arg_0)+3/2+Arg_1)+24)*(2+24*(1+Arg_0))+3+12*(1+Arg_0) {O(n^2)}
0: f->[1:g]: 0 {O(1)}
2: h->[1:i]: 0 {O(1)}
3: h->[1:g]: 1 {O(1)}
4: i->[1:stop]: 1 {O(1)}
5: i->[1:g]: 1 {O(1)}
6: f->[1/2:h; 1/2:h]: 0 {O(1)}
7: h->[1/2:h; 1/2:h]: (2*(2*max([max([1+Arg_1, 12]), 2+Arg_1])+24*(1+Arg_0)+3/2+Arg_1)+24)*(2+24*(1+Arg_0)) {O(n^2)}
8: i->[1/2:h; 1/2:h]: 12*(1+Arg_0) {O(n)}

Sizebounds:

0,0: f->g, Arg_0: Arg_0 {O(n)}
0,0: f->g, Arg_1: Arg_1 {O(n)}
7,6: f->h, Arg_0: Arg_0 {O(n)}
7,6: f->h, Arg_1: 2+Arg_1 {O(n)}
8,6: f->h, Arg_0: Arg_0 {O(n)}
8,6: f->h, Arg_1: (-1)+Arg_1 {O(n)}
3,2: h->i, Arg_0: Arg_0 {O(n)}
3,2: h->i, Arg_1: 12*max([(-1)+Arg_0, 0])+max([max([(-1)+Arg_1, 12]), 2+Arg_1]) {O(n)}
4,3: h->g, Arg_0: Arg_0 {O(n)}
4,3: h->g, Arg_1: 10 {O(1)}
9,7: h->h, Arg_0: Arg_0 {O(n)}
9,7: h->h, Arg_1: 12 {O(1)}
10,7: h->h, Arg_0: Arg_0 {O(n)}
10,7: h->h, Arg_1: 9 {O(1)}
5,4: i->stop, Arg_0: 4 {O(1)}
5,4: i->stop, Arg_1: 12*max([(-1)+Arg_0, 0])+max([max([(-1)+Arg_1, 12]), 2+Arg_1]) {O(n)}
6,5: i->g, Arg_0: Arg_0 {O(n)}
6,5: i->g, Arg_1: 12*max([(-1)+Arg_0, 0])+max([max([(-1)+Arg_1, 12]), 2+Arg_1]) {O(n)}
11,8: i->h, Arg_0: Arg_0 {O(n)}
11,8: i->h, Arg_1: 12*max([(-1)+Arg_0, 0])+max([max([(-1)+Arg_1, 12]), 2+Arg_1]) {O(n)}
12,8: i->h, Arg_0: Arg_0 {O(n)}
12,8: i->h, Arg_1: 12*max([(-1)+Arg_0, 0])+max([max([(-1)+Arg_1, 12]), 2+Arg_1]) {O(n)}

ExpSizeBounds:

(0: f->[1:g], g), Arg_0: Arg_0 {O(n)}
(0: f->[1:g], g), Arg_1: Arg_1 {O(n)}
(2: h->[1:i], i), Arg_0: 24*(1+Arg_0)+6+Arg_0 {O(n)}
(2: h->[1:i], i), Arg_1: 12*(1+Arg_0)+max([max([1+Arg_1, 12]), 2+Arg_1]) {O(n)}
(3: h->[1:g], g), Arg_0: Arg_0 {O(n)}
(3: h->[1:g], g), Arg_1: 2*Arg_1+3+3/2*(2*(2*max([max([1+Arg_1, 12]), 2+Arg_1])+24*(1+Arg_0)+3/2+Arg_1)+24)*(2+24*(1+Arg_0))+30*(1+Arg_0)+max([max([1+Arg_1, 12]), 2+Arg_1]) {O(n^2)}
(4: i->[1:stop], stop), Arg_0: 4 {O(1)}
(4: i->[1:stop], stop), Arg_1: 12*(1+Arg_0)+max([max([1+Arg_1, 12]), 2+Arg_1]) {O(n)}
(5: i->[1:g], g), Arg_0: Arg_0 {O(n)}
(5: i->[1:g], g), Arg_1: 12*(1+Arg_0)+max([max([1+Arg_1, 12]), 2+Arg_1]) {O(n)}
(6: f->[1/2:h; 1/2:h], h), Arg_0: Arg_0 {O(n)}
(6: f->[1/2:h; 1/2:h], h), Arg_1: 3/2+Arg_1 {O(n)}
(7: h->[1/2:h; 1/2:h], h), Arg_0: max([5, Arg_0]) {O(n)}
(7: h->[1/2:h; 1/2:h], h), Arg_1: 18*(1+Arg_0)+3/2+Arg_1+3/2*(2*(2*max([max([1+Arg_1, 12]), 2+Arg_1])+24*(1+Arg_0)+3/2+Arg_1)+24)*(2+24*(1+Arg_0)) {O(n^2)}
(8: i->[1/2:h; 1/2:h], h), Arg_0: Arg_0 {O(n)}
(8: i->[1/2:h; 1/2:h], h), Arg_1: 12*(1+Arg_0)+max([max([1+Arg_1, 12]), 2+Arg_1]) {O(n)}