Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: start0
      0: start -> lbl91 : C'=100, E'=1, [ A==0 && B==0 && C==D && E==F ], cost: 1
      1: start -> lbl111 : C'=100, E'=2, [ 0>=1+B && A==B && C==D && E==F ], cost: 1
      2: start -> lbl111 : C'=100, E'=2, [ B>=1 && A==B && C==D && E==F ], cost: 1
      4: lbl91 -> lbl91 : E'=1+E, [ 39>=E && E>=1 && 40>=E && A==0 && C==100 && B==0 ], cost: 1
      5: lbl91 -> lbl111 : E'=2+E, [ 0>=1 && 39>=E && E>=1 && 40>=E && C==100 && A==0 && B==0 ], cost: 1
      6: lbl91 -> lbl111 : E'=2+E, [ 0>=1 && 39>=E && E>=1 && 40>=E && C==100 && A==0 && B==0 ], cost: 1
      3: lbl91 -> stop : [ E==40 && C==100 && A==0 && B==0 ], cost: 1
      8: lbl111 -> lbl91 : E'=1+E, [ 39>=E && E>=2 && 41>=E && A==0 && C==100 && B==0 ], cost: 1
      9: lbl111 -> lbl111 : E'=2+E, [ 0>=1+B && 39>=E && E>=2 && 41>=E && C==100 && A==B ], cost: 1
     10: lbl111 -> lbl111 : E'=2+E, [ B>=1 && 39>=E && E>=2 && 41>=E && C==100 && A==B ], cost: 1
      7: lbl111 -> stop : [ E>=40 && E>=2 && 41>=E && C==100 && A==B ], cost: 1
     11: start0 -> start : A'=B, C'=D, E'=F, [], cost: 1

Removing duplicate transition: 5.

Simplified the transitions:
  Start location: start0
      0: start -> lbl91 : C'=100, E'=1, [ A==0 && B==0 && C==D && E==F ], cost: 1
      1: start -> lbl111 : C'=100, E'=2, [ 0>=1+B && A==B && C==D && E==F ], cost: 1
      2: start -> lbl111 : C'=100, E'=2, [ B>=1 && A==B && C==D && E==F ], cost: 1
      4: lbl91 -> lbl91 : E'=1+E, [ 39>=E && E>=1 && A==0 && C==100 && B==0 ], cost: 1
      6: lbl91 -> lbl111 : E'=2+E, [ 0>=1 ], cost: 1
      8: lbl111 -> lbl91 : E'=1+E, [ 39>=E && E>=2 && A==0 && C==100 && B==0 ], cost: 1
      9: lbl111 -> lbl111 : E'=2+E, [ 0>=1+B && 39>=E && E>=2 && C==100 && A==B ], cost: 1
     10: lbl111 -> lbl111 : E'=2+E, [ B>=1 && 39>=E && E>=2 && C==100 && A==B ], cost: 1
     11: start0 -> start : A'=B, C'=D, E'=F, [], cost: 1

Eliminating 1 self-loops for location lbl91
  Self-Loop 4 has the metering function: 40-E, resulting in the new transition 12.
  Removing the self-loops: 4.
Eliminating 2 self-loops for location lbl111
  Self-Loop 9 has the metering function: meter, resulting in the new transition 13.
  Self-Loop 10 has the metering function: meter_1, resulting in the new transition 14.
  Removing the self-loops: 9 10.

Removed all Self-loops using metering functions (where possible):
  Start location: start0
      0: start -> lbl91 : C'=100, E'=1, [ A==0 && B==0 && C==D && E==F ], cost: 1
      1: start -> lbl111 : C'=100, E'=2, [ 0>=1+B && A==B && C==D && E==F ], cost: 1
      2: start -> lbl111 : C'=100, E'=2, [ B>=1 && A==B && C==D && E==F ], cost: 1
     12: lbl91 -> [5] : E'=40, [ 39>=E && E>=1 && A==0 && C==100 && B==0 ], cost: 40-E
     13: lbl111 -> [6] : E'=E+2*meter, [ 0>=1+B && 39>=E && E>=2 && C==100 && A==B && 2*meter==39-E ], cost: meter
     14: lbl111 -> [6] : E'=2*meter_1+E, [ B>=1 && 39>=E && E>=2 && C==100 && A==B && 2*meter_1==39-E ], cost: meter_1
     11: start0 -> start : A'=B, C'=D, E'=F, [], cost: 1
      6: [5] -> lbl111 : E'=2+E, [ 0>=1 ], cost: 1
      8: [6] -> lbl91 : E'=1+E, [ 39>=E && E>=2 && A==0 && C==100 && B==0 ], cost: 1


Applied chaining over branches and pruning:
  Start location: start0
     18: lbl91 -> [7] : E'=40, [ 39>=E && E>=1 && A==0 && C==100 && B==0 ], cost: 40-E
     19: lbl111 -> [8] : E'=E+2*meter, [ 0>=1+B && 39>=E && E>=2 && C==100 && A==B && 2*meter==39-E ], cost: meter
     20: lbl111 -> [9] : E'=2*meter_1+E, [ B>=1 && 39>=E && E>=2 && C==100 && A==B && 2*meter_1==39-E ], cost: meter_1
     15: start0 -> lbl91 : A'=B, C'=100, E'=1, [ B==0 && B==0 && D==D && F==F ], cost: 2
     16: start0 -> lbl111 : A'=B, C'=100, E'=2, [ 0>=1+B && B==B && D==D && F==F ], cost: 2
     17: start0 -> lbl111 : A'=B, C'=100, E'=2, [ B>=1 && B==B && D==D && F==F ], cost: 2


Applied simple chaining:
  Start location: start0
     19: lbl111 -> [8] : E'=E+2*meter, [ 0>=1+B && 39>=E && E>=2 && C==100 && A==B && 2*meter==39-E ], cost: meter
     20: lbl111 -> [9] : E'=2*meter_1+E, [ B>=1 && 39>=E && E>=2 && C==100 && A==B && 2*meter_1==39-E ], cost: meter_1
     16: start0 -> lbl111 : A'=B, C'=100, E'=2, [ 0>=1+B && B==B && D==D && F==F ], cost: 2
     17: start0 -> lbl111 : A'=B, C'=100, E'=2, [ B>=1 && B==B && D==D && F==F ], cost: 2
     15: start0 -> [7] : A'=B, C'=100, E'=40, [ B==0 && B==0 && D==D && F==F && 39>=1 && 1>=1 && B==0 && 100==100 && B==0 ], cost: 41


Applied chaining over branches and pruning:
  Start location: start0
    <empty>


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: start0
    <empty>


Computing complexity for remaining 0 transitions.


The final runtime is determined by this resulting transition:
  Final Guard: 
  Final Cost:  1

Obtained the following complexity w.r.t. the length of the input n:
  Complexity class: const
  Complexity value: 0

WORST_CASE(Omega(1),?)