Inferring Expected Runtimes Using Sizes

KoAT2 Proof WORST_CASE( ?, 10*(1/95*Arg_1+2000/171*(1+Arg_0))+9+40*(1+Arg_0) {O(n)})

Initial Complexity Problem (after preprocessing)

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

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

Timebounds:

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

Expected Timebounds:

Overall expected timebound: 2*(1+10/9*(1+Arg_0))+2*(1/95*Arg_1+2000/171*(1+Arg_0))+4+40/9*(1+Arg_0) {O(n)}
0: f->[1:g]: 1 {O(1)}
2: h->[1:i]: 2*(1+10/9*(1+Arg_0)) {O(n)}
3: h->[1:g]: 1 {O(1)}
4: i->[1/2:i; 1/2:i]: 2*(1/95*Arg_1+2000/171*(1+Arg_0)) {O(n)}
5: i->[1:g]: 1 {O(1)}
6: f->[9/10:h; 1/10:h]: 1 {O(1)}
7: h->[9/10:h; 1/10:h]: 20/9*(1+Arg_0) {O(n)}
8: i->[9/10:h; 1/10:h]: 20/9*(1+Arg_0) {O(n)}

Costbounds:

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

Expected Costbounds:

Overall expected costbound: 10*(1/95*Arg_1+2000/171*(1+Arg_0))+9+40*(1+Arg_0) {O(n)}
0: f->[1:g]: 0 {O(1)}
2: h->[1:i]: 0 {O(1)}
3: h->[1:g]: 0 {O(1)}
4: i->[1/2:i; 1/2:i]: 10*(1/95*Arg_1+2000/171*(1+Arg_0)) {O(n)}
5: i->[1:g]: 0 {O(1)}
6: f->[9/10:h; 1/10:h]: 9 {O(1)}
7: h->[9/10:h; 1/10:h]: 20*(1+Arg_0) {O(n)}
8: i->[9/10:h; 1/10:h]: 20*(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)}
8,6: f->h, Arg_0: 0 {O(1)}
8,6: f->h, Arg_1: Arg_1 {O(n)}
9,6: f->h, Arg_0: (-1) {O(1)}
9,6: f->h, Arg_1: Arg_1 {O(n)}
3,2: h->i, Arg_0: 0 {O(1)}
3,2: h->i, Arg_1: max([1100, Arg_1]) {O(n)}
4,3: h->g, Arg_0: 0 {O(1)}
4,3: h->g, Arg_1: max([1100, Arg_1]) {O(n)}
10,7: h->h, Arg_0: 0 {O(1)}
10,7: h->h, Arg_1: max([1100, Arg_1]) {O(n)}
11,7: h->h, Arg_0: (-1) {O(1)}
11,7: h->h, Arg_1: max([1100, Arg_1]) {O(n)}
5,4: i->i, Arg_0: 0 {O(1)}
5,4: i->i, Arg_1: max([1100, Arg_1]) {O(n)}
6,4: i->i, Arg_0: 0 {O(1)}
6,4: i->i, Arg_1: max([1100, Arg_1]) {O(n)}
7,5: i->g, Arg_0: 0 {O(1)}
7,5: i->g, Arg_1: 1100 {O(1)}
12,8: i->h, Arg_0: 0 {O(1)}
12,8: i->h, Arg_1: 1100 {O(1)}
13,8: i->h, Arg_0: (-1) {O(1)}
13,8: i->h, Arg_1: 1100 {O(1)}

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: 1+Arg_0 {O(n)}
(2: h->[1:i], i), Arg_1: max([1100, Arg_1]) {O(n)}
(3: h->[1:g], g), Arg_0: Arg_0 {O(n)}
(3: h->[1:g], g), Arg_1: max([1100, Arg_1]) {O(n)}
(4: i->[1/2:i; 1/2:i], i), Arg_0: 1+Arg_0 {O(n)}
(4: i->[1/2:i; 1/2:i], i), Arg_1: max([1100, Arg_1]) {O(n)}
(5: i->[1:g], g), Arg_0: Arg_0 {O(n)}
(5: i->[1:g], g), Arg_1: 1100 {O(1)}
(6: f->[9/10:h; 1/10:h], h), Arg_0: 1+Arg_0 {O(n)}
(6: f->[9/10:h; 1/10:h], h), Arg_1: Arg_1 {O(n)}
(7: h->[9/10:h; 1/10:h], h), Arg_0: 1+Arg_0 {O(n)}
(7: h->[9/10:h; 1/10:h], h), Arg_1: max([1100, Arg_1]) {O(n)}
(8: i->[9/10:h; 1/10:h], h), Arg_0: 1+Arg_0 {O(n)}
(8: i->[9/10:h; 1/10:h], h), Arg_1: 1100 {O(1)}