Trying to load file: main.koat

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


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

Eliminating 1 self-loops for location lbl111
  Removing the self-loops: 3.
Adding an epsilon transition (to model nonexecution of the loops): 14.
Eliminating 3 self-loops for location lbl82
  Self-Loop 9 has unbounded runtime, resulting in the new transition 15.
  Self-Loop 10 has unbounded runtime, resulting in the new transition 16.
  Self-Loop 11 has unbounded runtime, resulting in the new transition 17.
  Removing the self-loops: 9 10 11.

Removed all Self-loops using metering functions (where possible):
  Start location: start0
      1: start -> lbl111 : B'=H, D'=1, F'=-1+H, [ A>=2 && B==C && D==E && F==G && H==A ], cost: 1
     13: lbl111 -> [6] : D'=-F+D, [ D>=F && A>=1+F && A>=F+D && A>=B && F>=1 && D>=0 && H==A ], cost: 1
     14: lbl111 -> [6] : [], cost: 0
     15: lbl82 -> [7] : [ F>=1+A && A>=1 && F>=0 && A>=2+F && A>=B && F+A>=1+B && H==A && D==A ], cost: INF
     16: lbl82 -> [7] : [ F>=1 && 0>=1+A && A>=2+F && A>=B && F+A>=1+B && H==A && D==A ], cost: INF
     17: lbl82 -> [7] : [ F>=1 && 0>=2+F && 0>=B && F>=1+B && D==0 && H==0 && A==0 ], cost: INF
     12: start0 -> start : B'=C, D'=E, F'=G, H'=A, [], cost: 1
      4: [6] -> lbl82 : D'=H, F'=-1+F, [ F>=1+D && 0>=1+D && A>=1+F && A>=F+D && A>=B && F>=1 && D>=0 && H==A ], cost: 1
      5: [6] -> lbl82 : D'=H, F'=-1+F, [ F>=1+D && D>=1 && A>=1+F && A>=F+D && A>=B && F>=1 && H==A ], cost: 1
      6: [6] -> lbl82 : B'=B-F, D'=H, F'=-1+F, [ F>=1 && A>=1+F && A>=B && D==0 && H==A ], cost: 1
      8: [7] -> lbl111 : D'=-F+D, [ F>=1 && A>=2+F && A>=B && F+A>=1+B && H==A && D==A ], cost: 1


Applied simple chaining:
  Start location: start0
     13: lbl111 -> [6] : D'=-F+D, [ D>=F && A>=1+F && A>=F+D && A>=B && F>=1 && D>=0 && H==A ], cost: 1
     14: lbl111 -> [6] : [], cost: 0
     15: lbl82 -> [7] : [ F>=1+A && A>=1 && F>=0 && A>=2+F && A>=B && F+A>=1+B && H==A && D==A ], cost: INF
     16: lbl82 -> [7] : [ F>=1 && 0>=1+A && A>=2+F && A>=B && F+A>=1+B && H==A && D==A ], cost: INF
     17: lbl82 -> [7] : [ F>=1 && 0>=2+F && 0>=B && F>=1+B && D==0 && H==0 && A==0 ], cost: INF
     12: start0 -> lbl111 : B'=A, D'=1, F'=-1+A, H'=A, [ A>=2 && C==C && E==E && G==G && A==A ], cost: 2
      4: [6] -> lbl82 : D'=H, F'=-1+F, [ F>=1+D && 0>=1+D && A>=1+F && A>=F+D && A>=B && F>=1 && D>=0 && H==A ], cost: 1
      5: [6] -> lbl82 : D'=H, F'=-1+F, [ F>=1+D && D>=1 && A>=1+F && A>=F+D && A>=B && F>=1 && H==A ], cost: 1
      6: [6] -> lbl82 : B'=B-F, D'=H, F'=-1+F, [ F>=1 && A>=1+F && A>=B && D==0 && H==A ], cost: 1
      8: [7] -> lbl111 : D'=-F+D, [ F>=1 && A>=2+F && A>=B && F+A>=1+B && H==A && D==A ], cost: 1


Applied chaining over branches and pruning:
  Start location: start0
     18: lbl111 -> lbl82 : D'=H, F'=-1+F, [ D>=F && A>=1+F && A>=F+D && A>=B && F>=1 && D>=0 && H==A && F>=1-F+D && -F+D>=1 && A>=1+F && A>=D && A>=B && F>=1 && H==A ], cost: 2
     19: lbl111 -> lbl82 : B'=B-F, D'=H, F'=-1+F, [ D>=F && A>=1+F && A>=F+D && A>=B && F>=1 && D>=0 && H==A && F>=1 && A>=1+F && A>=B && -F+D==0 && H==A ], cost: 2
     20: lbl111 -> lbl82 : D'=H, F'=-1+F, [ F>=1+D && D>=1 && A>=1+F && A>=F+D && A>=B && F>=1 && H==A ], cost: 1
     21: lbl111 -> lbl82 : B'=B-F, D'=H, F'=-1+F, [ F>=1 && A>=1+F && A>=B && D==0 && H==A ], cost: 1
     22: lbl82 -> [8] : [ F>=1+A && A>=1 && F>=0 && A>=2+F && A>=B && F+A>=1+B && H==A && D==A ], cost: INF
     23: lbl82 -> [9] : [ F>=1 && 0>=1+A && A>=2+F && A>=B && F+A>=1+B && H==A && D==A ], cost: INF
     24: lbl82 -> [10] : [ F>=1 && 0>=2+F && 0>=B && F>=1+B && D==0 && H==0 && A==0 ], cost: INF
     12: start0 -> lbl111 : B'=A, D'=1, F'=-1+A, H'=A, [ A>=2 && C==C && E==E && G==G && A==A ], cost: 2


Applied chaining over branches and pruning:
  Start location: start0
     22: lbl82 -> [8] : [ F>=1+A && A>=1 && F>=0 && A>=2+F && A>=B && F+A>=1+B && H==A && D==A ], cost: INF
     23: lbl82 -> [9] : [ F>=1 && 0>=1+A && A>=2+F && A>=B && F+A>=1+B && H==A && D==A ], cost: INF
     24: lbl82 -> [10] : [ F>=1 && 0>=2+F && 0>=B && F>=1+B && D==0 && H==0 && A==0 ], cost: INF
     25: start0 -> lbl82 : B'=1, D'=A, F'=-2+A, H'=A, [ A>=2 && C==C && E==E && G==G && A==A && 1>=-1+A && A>=A && A>=A && A>=A && -1+A>=1 && 1>=0 && A==A && -1+A>=1 && A>=A && A>=A && 2-A==0 && A==A ], cost: 4
     26: start0 -> lbl82 : B'=A, D'=A, F'=-2+A, H'=A, [ A>=2 && C==C && E==E && G==G && A==A && -1+A>=2 && 1>=1 && A>=A && A>=A && A>=A && -1+A>=1 && A==A ], 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),?)