Trying to load file: main.koat Initial Control flow graph problem: Start location: evalrandom2dstart 0: evalrandom2dstart -> evalrandom2dentryin : [], cost: 1 1: evalrandom2dentryin -> evalrandom2dbb10in : A'=0, [], cost: 1 2: evalrandom2dbb10in -> evalrandom2dbbin : [ B>=1+A ], cost: 1 3: evalrandom2dbb10in -> evalrandom2dreturnin : [ A>=B ], cost: 1 5: evalrandom2dbbin -> evalrandom2dbb10in : A'=1+A, [ 0>=1+free_1 ], cost: 1 6: evalrandom2dbbin -> evalrandom2dbb10in : A'=1+A, [ free_2>=4 ], cost: 1 4: evalrandom2dbbin -> evalrandom2dbb2in : C'=1+A, D'=free, [ free>=0 && 3>=free ], cost: 1 31: evalrandom2dreturnin -> evalrandom2dstop : [], cost: 1 7: evalrandom2dbb2in -> evalrandom2dNodeBlock9in : [], cost: 1 8: evalrandom2dNodeBlock9in -> evalrandom2dNodeBlockin : [ 1>=D ], cost: 1 9: evalrandom2dNodeBlock9in -> evalrandom2dNodeBlock7in : [ D>=2 ], cost: 1 10: evalrandom2dNodeBlockin -> evalrandom2dLeafBlockin : [ 0>=D ], cost: 1 11: evalrandom2dNodeBlockin -> evalrandom2dLeafBlock1in : [ D>=1 ], cost: 1 20: evalrandom2dNodeBlock7in -> evalrandom2dLeafBlock3in : [ 2>=D ], cost: 1 21: evalrandom2dNodeBlock7in -> evalrandom2dLeafBlock5in : [ D>=3 ], cost: 1 12: evalrandom2dLeafBlockin -> evalrandom2dbb3in : [ D==0 ], cost: 1 13: evalrandom2dLeafBlockin -> evalrandom2dNewDefaultin : [ 0>=1+D ], cost: 1 14: evalrandom2dLeafBlockin -> evalrandom2dNewDefaultin : [ D>=1 ], cost: 1 17: evalrandom2dLeafBlock1in -> evalrandom2dNewDefaultin : [ 0>=D ], cost: 1 18: evalrandom2dLeafBlock1in -> evalrandom2dNewDefaultin : [ D>=2 ], cost: 1 16: evalrandom2dLeafBlock1in -> evalrandom2dbb5in : [ D==1 ], cost: 1 15: evalrandom2dbb3in -> evalrandom2dbb10in : A'=C, [], cost: 1 30: evalrandom2dNewDefaultin -> evalrandom2dbb10in : A'=C, [], cost: 1 19: evalrandom2dbb5in -> evalrandom2dbb10in : A'=C, [], cost: 1 23: evalrandom2dLeafBlock3in -> evalrandom2dNewDefaultin : [ 1>=D ], cost: 1 24: evalrandom2dLeafBlock3in -> evalrandom2dNewDefaultin : [ D>=3 ], cost: 1 22: evalrandom2dLeafBlock3in -> evalrandom2dbb7in : [ D==2 ], cost: 1 27: evalrandom2dLeafBlock5in -> evalrandom2dNewDefaultin : [ 2>=D ], cost: 1 28: evalrandom2dLeafBlock5in -> evalrandom2dNewDefaultin : [ D>=4 ], cost: 1 26: evalrandom2dLeafBlock5in -> evalrandom2dbb9in : [ D==3 ], cost: 1 25: evalrandom2dbb7in -> evalrandom2dbb10in : A'=C, [], cost: 1 29: evalrandom2dbb9in -> evalrandom2dbb10in : A'=C, [], cost: 1 Removing duplicate transition: 5. Simplified the transitions: Start location: evalrandom2dstart 0: evalrandom2dstart -> evalrandom2dentryin : [], cost: 1 1: evalrandom2dentryin -> evalrandom2dbb10in : A'=0, [], cost: 1 2: evalrandom2dbb10in -> evalrandom2dbbin : [ B>=1+A ], cost: 1 6: evalrandom2dbbin -> evalrandom2dbb10in : A'=1+A, [], cost: 1 4: evalrandom2dbbin -> evalrandom2dbb2in : C'=1+A, D'=free, [ free>=0 && 3>=free ], cost: 1 7: evalrandom2dbb2in -> evalrandom2dNodeBlock9in : [], cost: 1 8: evalrandom2dNodeBlock9in -> evalrandom2dNodeBlockin : [ 1>=D ], cost: 1 9: evalrandom2dNodeBlock9in -> evalrandom2dNodeBlock7in : [ D>=2 ], cost: 1 10: evalrandom2dNodeBlockin -> evalrandom2dLeafBlockin : [ 0>=D ], cost: 1 11: evalrandom2dNodeBlockin -> evalrandom2dLeafBlock1in : [ D>=1 ], cost: 1 20: evalrandom2dNodeBlock7in -> evalrandom2dLeafBlock3in : [ 2>=D ], cost: 1 21: evalrandom2dNodeBlock7in -> evalrandom2dLeafBlock5in : [ D>=3 ], cost: 1 12: evalrandom2dLeafBlockin -> evalrandom2dbb3in : [ D==0 ], cost: 1 13: evalrandom2dLeafBlockin -> evalrandom2dNewDefaultin : [ 0>=1+D ], cost: 1 14: evalrandom2dLeafBlockin -> evalrandom2dNewDefaultin : [ D>=1 ], cost: 1 17: evalrandom2dLeafBlock1in -> evalrandom2dNewDefaultin : [ 0>=D ], cost: 1 18: evalrandom2dLeafBlock1in -> evalrandom2dNewDefaultin : [ D>=2 ], cost: 1 16: evalrandom2dLeafBlock1in -> evalrandom2dbb5in : [ D==1 ], cost: 1 15: evalrandom2dbb3in -> evalrandom2dbb10in : A'=C, [], cost: 1 30: evalrandom2dNewDefaultin -> evalrandom2dbb10in : A'=C, [], cost: 1 19: evalrandom2dbb5in -> evalrandom2dbb10in : A'=C, [], cost: 1 23: evalrandom2dLeafBlock3in -> evalrandom2dNewDefaultin : [ 1>=D ], cost: 1 24: evalrandom2dLeafBlock3in -> evalrandom2dNewDefaultin : [ D>=3 ], cost: 1 22: evalrandom2dLeafBlock3in -> evalrandom2dbb7in : [ D==2 ], cost: 1 27: evalrandom2dLeafBlock5in -> evalrandom2dNewDefaultin : [ 2>=D ], cost: 1 28: evalrandom2dLeafBlock5in -> evalrandom2dNewDefaultin : [ D>=4 ], cost: 1 26: evalrandom2dLeafBlock5in -> evalrandom2dbb9in : [ D==3 ], cost: 1 25: evalrandom2dbb7in -> evalrandom2dbb10in : A'=C, [], cost: 1 29: evalrandom2dbb9in -> evalrandom2dbb10in : A'=C, [], cost: 1 Applied simple chaining: Start location: evalrandom2dstart 0: evalrandom2dstart -> evalrandom2dbb10in : A'=0, [], cost: 2 2: evalrandom2dbb10in -> evalrandom2dbbin : [ B>=1+A ], cost: 1 6: evalrandom2dbbin -> evalrandom2dbb10in : A'=1+A, [], cost: 1 4: evalrandom2dbbin -> evalrandom2dNodeBlock9in : C'=1+A, D'=free, [ free>=0 && 3>=free ], cost: 2 8: evalrandom2dNodeBlock9in -> evalrandom2dNodeBlockin : [ 1>=D ], cost: 1 9: evalrandom2dNodeBlock9in -> evalrandom2dNodeBlock7in : [ D>=2 ], cost: 1 10: evalrandom2dNodeBlockin -> evalrandom2dLeafBlockin : [ 0>=D ], cost: 1 11: evalrandom2dNodeBlockin -> evalrandom2dLeafBlock1in : [ D>=1 ], cost: 1 20: evalrandom2dNodeBlock7in -> evalrandom2dLeafBlock3in : [ 2>=D ], cost: 1 21: evalrandom2dNodeBlock7in -> evalrandom2dLeafBlock5in : [ D>=3 ], cost: 1 12: evalrandom2dLeafBlockin -> evalrandom2dbb10in : A'=C, [ D==0 ], cost: 2 13: evalrandom2dLeafBlockin -> evalrandom2dNewDefaultin : [ 0>=1+D ], cost: 1 14: evalrandom2dLeafBlockin -> evalrandom2dNewDefaultin : [ D>=1 ], cost: 1 16: evalrandom2dLeafBlock1in -> evalrandom2dbb10in : A'=C, [ D==1 ], cost: 2 17: evalrandom2dLeafBlock1in -> evalrandom2dNewDefaultin : [ 0>=D ], cost: 1 18: evalrandom2dLeafBlock1in -> evalrandom2dNewDefaultin : [ D>=2 ], cost: 1 30: evalrandom2dNewDefaultin -> evalrandom2dbb10in : A'=C, [], cost: 1 22: evalrandom2dLeafBlock3in -> evalrandom2dbb10in : A'=C, [ D==2 ], cost: 2 23: evalrandom2dLeafBlock3in -> evalrandom2dNewDefaultin : [ 1>=D ], cost: 1 24: evalrandom2dLeafBlock3in -> evalrandom2dNewDefaultin : [ D>=3 ], cost: 1 26: evalrandom2dLeafBlock5in -> evalrandom2dbb10in : A'=C, [ D==3 ], cost: 2 27: evalrandom2dLeafBlock5in -> evalrandom2dNewDefaultin : [ 2>=D ], cost: 1 28: evalrandom2dLeafBlock5in -> evalrandom2dNewDefaultin : [ D>=4 ], cost: 1 Applied chaining over branches and pruning: Start location: evalrandom2dstart 0: evalrandom2dstart -> evalrandom2dbb10in : A'=0, [], cost: 2 32: evalrandom2dbb10in -> evalrandom2dbb10in : A'=1+A, [ B>=1+A ], cost: 2 33: evalrandom2dbb10in -> evalrandom2dNodeBlock9in : C'=1+A, D'=free, [ B>=1+A && free>=0 && 3>=free ], cost: 3 34: evalrandom2dNodeBlock9in -> evalrandom2dLeafBlockin : [ 1>=D && 0>=D ], cost: 2 35: evalrandom2dNodeBlock9in -> evalrandom2dLeafBlock1in : [ 1>=D && D>=1 ], cost: 2 36: evalrandom2dNodeBlock9in -> evalrandom2dLeafBlock3in : [ D>=2 && 2>=D ], cost: 2 37: evalrandom2dNodeBlock9in -> evalrandom2dLeafBlock5in : [ D>=2 && D>=3 ], cost: 2 12: evalrandom2dLeafBlockin -> evalrandom2dbb10in : A'=C, [ D==0 ], cost: 2 13: evalrandom2dLeafBlockin -> evalrandom2dNewDefaultin : [ 0>=1+D ], cost: 1 14: evalrandom2dLeafBlockin -> evalrandom2dNewDefaultin : [ D>=1 ], cost: 1 16: evalrandom2dLeafBlock1in -> evalrandom2dbb10in : A'=C, [ D==1 ], cost: 2 17: evalrandom2dLeafBlock1in -> evalrandom2dNewDefaultin : [ 0>=D ], cost: 1 18: evalrandom2dLeafBlock1in -> evalrandom2dNewDefaultin : [ D>=2 ], cost: 1 30: evalrandom2dNewDefaultin -> evalrandom2dbb10in : A'=C, [], cost: 1 22: evalrandom2dLeafBlock3in -> evalrandom2dbb10in : A'=C, [ D==2 ], cost: 2 23: evalrandom2dLeafBlock3in -> evalrandom2dNewDefaultin : [ 1>=D ], cost: 1 24: evalrandom2dLeafBlock3in -> evalrandom2dNewDefaultin : [ D>=3 ], cost: 1 26: evalrandom2dLeafBlock5in -> evalrandom2dbb10in : A'=C, [ D==3 ], cost: 2 27: evalrandom2dLeafBlock5in -> evalrandom2dNewDefaultin : [ 2>=D ], cost: 1 28: evalrandom2dLeafBlock5in -> evalrandom2dNewDefaultin : [ D>=4 ], cost: 1 Eliminating 1 self-loops for location evalrandom2dbb10in Self-Loop 32 has the metering function: B-A, resulting in the new transition 38. Removing the self-loops: 32. Removed all Self-loops using metering functions (where possible): Start location: evalrandom2dstart 0: evalrandom2dstart -> evalrandom2dbb10in : A'=0, [], cost: 2 38: evalrandom2dbb10in -> [19] : A'=B, [ B>=1+A ], cost: 2*B-2*A 34: evalrandom2dNodeBlock9in -> evalrandom2dLeafBlockin : [ 1>=D && 0>=D ], cost: 2 35: evalrandom2dNodeBlock9in -> evalrandom2dLeafBlock1in : [ 1>=D && D>=1 ], cost: 2 36: evalrandom2dNodeBlock9in -> evalrandom2dLeafBlock3in : [ D>=2 && 2>=D ], cost: 2 37: evalrandom2dNodeBlock9in -> evalrandom2dLeafBlock5in : [ D>=2 && D>=3 ], cost: 2 12: evalrandom2dLeafBlockin -> evalrandom2dbb10in : A'=C, [ D==0 ], cost: 2 13: evalrandom2dLeafBlockin -> evalrandom2dNewDefaultin : [ 0>=1+D ], cost: 1 14: evalrandom2dLeafBlockin -> evalrandom2dNewDefaultin : [ D>=1 ], cost: 1 16: evalrandom2dLeafBlock1in -> evalrandom2dbb10in : A'=C, [ D==1 ], cost: 2 17: evalrandom2dLeafBlock1in -> evalrandom2dNewDefaultin : [ 0>=D ], cost: 1 18: evalrandom2dLeafBlock1in -> evalrandom2dNewDefaultin : [ D>=2 ], cost: 1 30: evalrandom2dNewDefaultin -> evalrandom2dbb10in : A'=C, [], cost: 1 22: evalrandom2dLeafBlock3in -> evalrandom2dbb10in : A'=C, [ D==2 ], cost: 2 23: evalrandom2dLeafBlock3in -> evalrandom2dNewDefaultin : [ 1>=D ], cost: 1 24: evalrandom2dLeafBlock3in -> evalrandom2dNewDefaultin : [ D>=3 ], cost: 1 26: evalrandom2dLeafBlock5in -> evalrandom2dbb10in : A'=C, [ D==3 ], cost: 2 27: evalrandom2dLeafBlock5in -> evalrandom2dNewDefaultin : [ 2>=D ], cost: 1 28: evalrandom2dLeafBlock5in -> evalrandom2dNewDefaultin : [ D>=4 ], cost: 1 33: [19] -> evalrandom2dNodeBlock9in : C'=1+A, D'=free, [ B>=1+A && free>=0 && 3>=free ], cost: 3 Applied chaining over branches and pruning: Start location: evalrandom2dstart 0: evalrandom2dstart -> evalrandom2dbb10in : A'=0, [], cost: 2 39: evalrandom2dbb10in -> [20] : A'=B, [ B>=1+A ], cost: 2*B-2*A Applied simple chaining: Start location: evalrandom2dstart 0: evalrandom2dstart -> [20] : A'=B, [ B>=1 ], cost: 2+2*B Final control flow graph problem, now checking costs for infinitely many models: Start location: evalrandom2dstart 0: evalrandom2dstart -> [20] : A'=B, [ B>=1 ], cost: 2+2*B Computing complexity for remaining 1 transitions. Found configuration with infinitely models for cost: 2+2*B and guard: B>=1: B: Pos Found new complexity n^1, because: Found infinity configuration. The final runtime is determined by this resulting transition: Final Guard: B>=1 Final Cost: 2+2*B Obtained the following complexity w.r.t. the length of the input n: Complexity class: n^1 Complexity value: 1 WORST_CASE(Omega(n^1),?)