Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: start0
      0: start -> stop : [ 0>=A && B==C && D==E && F==G && H==A ], cost: 1
      1: start -> stop : [ 0>=1+G && B==C && D==E && F==G && H==A ], cost: 1
      2: start -> stop : B'=0, D'=F, [ A>=1 && F==0 && B==C && D==E && G==0 && H==A ], cost: 1
      3: start -> lM1 : B'=1, D'=-1+F, [ A>=1 && G>=1 && B==C && D==E && F==G && H==A ], cost: 1
      4: lM1 -> stop : [ A>=B && G>=B && B>=1 && D==0 && H==A && F==G ], cost: 1
      6: lM1 -> lM1 : B'=1+B, D'=-1+D, [ A>=1+B && D>=1 && A>=B && G>=B+D && B>=1 && D>=0 && H==A && F==G ], cost: 1
      5: lM1 -> lZZ1 : B'=0, [ D>=1 && G>=D+A && A>=1 && D>=0 && B==A && H==A && F==G ], cost: 1
      7: lZZ1 -> stop : [ 0>=D && G>=D+A && A>=2 && D>=1 && B==0 && H==A && F==G ], cost: 1
      9: lZZ1 -> lM1 : B'=1+B, D'=-1+D, [ A>=1 && D>=1 && G>=D+A && A>=2 && B==0 && H==A && F==G ], cost: 1
      8: lZZ1 -> lZZ1 : B'=0, [ D>=1 && 0>=A && G>=D+A && A>=2 && B==0 && H==A && F==G ], cost: 1
     10: start0 -> start : B'=C, D'=E, F'=G, H'=A, [], cost: 1


Simplified the transitions:
  Start location: start0
      3: start -> lM1 : B'=1, D'=-1+F, [ A>=1 && G>=1 && B==C && D==E && F==G && H==A ], cost: 1
      6: lM1 -> lM1 : B'=1+B, D'=-1+D, [ A>=1+B && D>=1 && G>=B+D && B>=1 && H==A && F==G ], cost: 1
      5: lM1 -> lZZ1 : B'=0, [ D>=1 && G>=D+A && A>=1 && B==A && H==A && F==G ], cost: 1
      9: lZZ1 -> lM1 : B'=1+B, D'=-1+D, [ D>=1 && G>=D+A && A>=2 && B==0 && H==A && F==G ], cost: 1
      8: lZZ1 -> lZZ1 : B'=0, [ D>=1 && 0>=A && G>=D+A && A>=2 && B==0 && H==A && F==G ], cost: 1
     10: start0 -> start : B'=C, D'=E, F'=G, H'=A, [], cost: 1

Eliminating 1 self-loops for location lM1
  Removing the self-loops: 6.
Adding an epsilon transition (to model nonexecution of the loops): 12.
Eliminating 1 self-loops for location lZZ1
  Self-Loop 8 has unbounded runtime, resulting in the new transition 13.
  Removing the self-loops: 8.

Removed all Self-loops using metering functions (where possible):
  Start location: start0
      3: start -> lM1 : B'=1, D'=-1+F, [ A>=1 && G>=1 && B==C && D==E && F==G && H==A ], cost: 1
     11: lM1 -> [5] : B'=1+B, D'=-1+D, [ A>=1+B && D>=1 && G>=B+D && B>=1 && H==A && F==G ], cost: 1
     12: lM1 -> [5] : [], cost: 0
     13: lZZ1 -> [6] : [ D>=1 && 0>=A && G>=D+A && A>=2 && B==0 && H==A && F==G ], cost: INF
     10: start0 -> start : B'=C, D'=E, F'=G, H'=A, [], cost: 1
      5: [5] -> lZZ1 : B'=0, [ D>=1 && G>=D+A && A>=1 && B==A && H==A && F==G ], cost: 1
      9: [6] -> lM1 : B'=1+B, D'=-1+D, [ D>=1 && G>=D+A && A>=2 && B==0 && H==A && F==G ], cost: 1


Applied simple chaining:
  Start location: start0
     11: lM1 -> [5] : B'=1+B, D'=-1+D, [ A>=1+B && D>=1 && G>=B+D && B>=1 && H==A && F==G ], cost: 1
     12: lM1 -> [5] : [], cost: 0
     13: lZZ1 -> [6] : [ D>=1 && 0>=A && G>=D+A && A>=2 && B==0 && H==A && F==G ], cost: INF
     10: start0 -> lM1 : B'=1, D'=-1+G, F'=G, H'=A, [ A>=1 && G>=1 && C==C && E==E && G==G && A==A ], cost: 2
      5: [5] -> lZZ1 : B'=0, [ D>=1 && G>=D+A && A>=1 && B==A && H==A && F==G ], cost: 1
      9: [6] -> lM1 : B'=1+B, D'=-1+D, [ D>=1 && G>=D+A && A>=2 && B==0 && H==A && F==G ], cost: 1


Applied chaining over branches and pruning:
  Start location: start0
     14: lM1 -> lZZ1 : B'=0, D'=-1+D, [ A>=1+B && D>=1 && G>=B+D && B>=1 && H==A && F==G && -1+D>=1 && G>=-1+D+A && A>=1 && 1+B==A && H==A && F==G ], cost: 2
     15: lM1 -> lZZ1 : B'=0, [ D>=1 && G>=D+A && A>=1 && B==A && H==A && F==G ], cost: 1
     16: lZZ1 -> [7] : [ D>=1 && 0>=A && G>=D+A && A>=2 && B==0 && H==A && F==G ], cost: INF
     10: start0 -> lM1 : B'=1, D'=-1+G, F'=G, H'=A, [ A>=1 && G>=1 && C==C && E==E && G==G && A==A ], cost: 2


Applied chaining over branches and pruning:
  Start location: start0
     16: lZZ1 -> [7] : [ D>=1 && 0>=A && G>=D+A && A>=2 && B==0 && H==A && F==G ], cost: INF
     17: start0 -> lZZ1 : B'=0, D'=-2+G, F'=G, H'=A, [ A>=1 && G>=1 && C==C && E==E && G==G && A==A && A>=2 && -1+G>=1 && G>=G && 1>=1 && A==A && G==G && -2+G>=1 && G>=-2+G+A && A>=1 && 2==A && A==A && G==G ], cost: 4
     18: start0 -> lZZ1 : B'=0, D'=-1+G, F'=G, H'=A, [ A>=1 && G>=1 && C==C && E==E && G==G && A==A && -1+G>=1 && G>=-1+G+A && A>=1 && 1==A && A==A && G==G ], cost: 3


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),?)