Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: f0
      0: f0 -> f2 : [ A>=1+B ], cost: 1
      1: f0 -> f2 : [ B>=1+A ], cost: 1
     70: f0 -> f17 : A'=B, H'=0, L'=0, [ B==A ], cost: 1
      2: f2 -> f3 : [ C>=1+B ], cost: 1
      3: f2 -> f3 : [ B>=1+C ], cost: 1
     69: f2 -> f17 : C'=B, H'=0, L'=0, [ B==C ], cost: 1
      4: f3 -> f4 : [ D>=1+B ], cost: 1
      5: f3 -> f4 : [ B>=1+D ], cost: 1
     68: f3 -> f17 : D'=B, H'=0, L'=0, [ B==D ], cost: 1
      6: f4 -> f5 : [ E>=1+B ], cost: 1
      7: f4 -> f5 : [ B>=1+E ], cost: 1
     67: f4 -> f17 : E'=B, H'=0, L'=0, [ B==E ], cost: 1
      8: f5 -> f6 : [ F>=1+B ], cost: 1
      9: f5 -> f6 : [ B>=1+F ], cost: 1
     66: f5 -> f17 : F'=B, H'=0, L'=0, [ B==F ], cost: 1
     10: f6 -> f7 : [ G>=1+B ], cost: 1
     11: f6 -> f7 : [ B>=1+G ], cost: 1
     65: f6 -> f17 : G'=B, H'=0, L'=0, [ B==G ], cost: 1
     62: f7 -> f17 : H'=1, L'=1, [ K>=1+B ], cost: 1
     63: f7 -> f17 : H'=1, L'=1, [ B>=1+K ], cost: 1
     64: f7 -> f17 : H'=0, K'=B, L'=0, [ B==K ], cost: 1
     12: f17 -> f18 : [ 0>=1+H ], cost: 1
     13: f17 -> f18 : [ H>=1 ], cost: 1
     79: f17 -> f33 : H'=0, M'=0, [ H==0 ], cost: 1
     14: f18 -> f19 : [ C>=1+A ], cost: 1
     15: f18 -> f19 : [ A>=1+C ], cost: 1
     78: f18 -> f33 : C'=A, H'=0, M'=0, [ A==C ], cost: 1
     16: f19 -> f20 : [ D>=1+A ], cost: 1
     17: f19 -> f20 : [ A>=1+D ], cost: 1
     77: f19 -> f33 : D'=A, H'=0, M'=0, [ A==D ], cost: 1
     18: f20 -> f21 : [ E>=1+A ], cost: 1
     19: f20 -> f21 : [ A>=1+E ], cost: 1
     76: f20 -> f33 : E'=A, H'=0, M'=0, [ A==E ], cost: 1
     20: f21 -> f22 : [ F>=1+A ], cost: 1
     21: f21 -> f22 : [ A>=1+F ], cost: 1
     75: f21 -> f33 : F'=A, H'=0, M'=0, [ A==F ], cost: 1
     22: f22 -> f23 : [ G>=1+A ], cost: 1
     23: f22 -> f23 : [ A>=1+G ], cost: 1
     74: f22 -> f33 : G'=A, H'=0, M'=0, [ A==G ], cost: 1
     71: f23 -> f33 : H'=1, M'=1, [ K>=1+A ], cost: 1
     72: f23 -> f33 : H'=1, M'=1, [ A>=1+K ], cost: 1
     73: f23 -> f33 : H'=0, K'=A, M'=0, [ A==K ], cost: 1
     24: f33 -> f34 : [ 0>=1+H ], cost: 1
     25: f33 -> f34 : [ H>=1 ], cost: 1
     87: f33 -> f47 : H'=0, N'=0, [ H==0 ], cost: 1
     26: f34 -> f35 : [ D>=1+C ], cost: 1
     27: f34 -> f35 : [ C>=1+D ], cost: 1
     86: f34 -> f47 : D'=C, H'=0, N'=0, [ C==D ], cost: 1
     28: f35 -> f36 : [ E>=1+C ], cost: 1
     29: f35 -> f36 : [ C>=1+E ], cost: 1
     85: f35 -> f47 : E'=C, H'=0, N'=0, [ C==E ], cost: 1
     30: f36 -> f37 : [ F>=1+C ], cost: 1
     31: f36 -> f37 : [ C>=1+F ], cost: 1
     84: f36 -> f47 : F'=C, H'=0, N'=0, [ C==F ], cost: 1
     32: f37 -> f38 : [ G>=1+C ], cost: 1
     33: f37 -> f38 : [ C>=1+G ], cost: 1
     83: f37 -> f47 : G'=C, H'=0, N'=0, [ C==G ], cost: 1
     80: f38 -> f47 : H'=1, N'=1, [ K>=1+C ], cost: 1
     81: f38 -> f47 : H'=1, N'=1, [ C>=1+K ], cost: 1
     82: f38 -> f47 : H'=0, K'=C, N'=0, [ C==K ], cost: 1
     34: f47 -> f48 : [ 0>=1+H ], cost: 1
     35: f47 -> f48 : [ H>=1 ], cost: 1
     94: f47 -> f59 : H'=0, O'=0, [ H==0 ], cost: 1
     36: f48 -> f49 : [ E>=1+D ], cost: 1
     37: f48 -> f49 : [ D>=1+E ], cost: 1
     93: f48 -> f59 : E'=D, H'=0, O'=0, [ D==E ], cost: 1
     38: f49 -> f50 : [ F>=1+D ], cost: 1
     39: f49 -> f50 : [ D>=1+F ], cost: 1
     92: f49 -> f59 : F'=D, H'=0, O'=0, [ D==F ], cost: 1
     40: f50 -> f51 : [ G>=1+D ], cost: 1
     41: f50 -> f51 : [ D>=1+G ], cost: 1
     91: f50 -> f59 : G'=D, H'=0, O'=0, [ D==G ], cost: 1
     88: f51 -> f59 : H'=1, O'=1, [ K>=1+D ], cost: 1
     89: f51 -> f59 : H'=1, O'=1, [ D>=1+K ], cost: 1
     90: f51 -> f59 : H'=0, K'=D, O'=0, [ D==K ], cost: 1
     42: f59 -> f60 : [ 0>=1+H ], cost: 1
     43: f59 -> f60 : [ H>=1 ], cost: 1
    100: f59 -> f69 : H'=0, P'=0, [ H==0 ], cost: 1
     44: f60 -> f61 : [ F>=1+E ], cost: 1
     45: f60 -> f61 : [ E>=1+F ], cost: 1
     99: f60 -> f69 : F'=E, H'=0, P'=0, [ E==F ], cost: 1
     46: f61 -> f62 : [ G>=1+E ], cost: 1
     47: f61 -> f62 : [ E>=1+G ], cost: 1
     98: f61 -> f69 : G'=E, H'=0, P'=0, [ E==G ], cost: 1
     95: f62 -> f69 : H'=1, P'=1, [ K>=1+E ], cost: 1
     96: f62 -> f69 : H'=1, P'=1, [ E>=1+K ], cost: 1
     97: f62 -> f69 : H'=0, K'=E, P'=0, [ E==K ], cost: 1
     48: f69 -> f70 : [ 0>=1+H ], cost: 1
     49: f69 -> f70 : [ H>=1 ], cost: 1
    105: f69 -> f77 : H'=0, Q_1'=0, [ H==0 ], cost: 1
     50: f70 -> f71 : [ G>=1+F ], cost: 1
     51: f70 -> f71 : [ F>=1+G ], cost: 1
    104: f70 -> f77 : G'=F, H'=0, Q_1'=0, [ F==G ], cost: 1
    101: f71 -> f77 : H'=1, Q_1'=1, [ K>=1+F ], cost: 1
    102: f71 -> f77 : H'=1, Q_1'=1, [ F>=1+K ], cost: 1
    103: f71 -> f77 : H'=0, K'=F, Q_1'=0, [ F==K ], cost: 1
     52: f77 -> f78 : [ 0>=1+H ], cost: 1
     53: f77 -> f78 : [ H>=1 ], cost: 1
    109: f77 -> f83 : H'=0, R'=0, [ H==0 ], cost: 1
    106: f78 -> f83 : H'=1, R'=1, [ K>=1+G ], cost: 1
    107: f78 -> f83 : H'=1, R'=1, [ G>=1+K ], cost: 1
    108: f78 -> f83 : H'=0, K'=G, R'=0, [ G==K ], cost: 1
     54: f101 -> f102 : [ 0>=1+E ], cost: 1
     55: f101 -> f102 : [ E>=1 ], cost: 1
    122: f101 -> f108 : E'=0, J'=0, T'=0, U'=free_3, [ E==0 ], cost: 1
    119: f102 -> f108 : J'=1, T'=1, U'=free, [ 0>=1+B ], cost: 1
    120: f102 -> f108 : J'=1, T'=1, U'=free_1, [ B>=1 ], cost: 1
    121: f102 -> f108 : B'=0, J'=0, T'=0, U'=free_2, [ B==0 ], cost: 1
     56: f108 -> f109 : [ 0>=1+H ], cost: 1
     57: f108 -> f109 : [ H>=1 ], cost: 1
    128: f108 -> f119 : H'=0, V'=1, [ H==0 ], cost: 1
     58: f109 -> f110 : [ 0>=1+Q ], cost: 1
     59: f109 -> f110 : [ Q>=1 ], cost: 1
    127: f109 -> f119 : Q'=0, V'=1, [ Q==0 ], cost: 1
     60: f110 -> f111 : [ 0>=1+J ], cost: 1
     61: f110 -> f111 : [ J>=1 ], cost: 1
    126: f110 -> f119 : J'=0, V'=1, [ J==0 ], cost: 1
    123: f111 -> f119 : V'=0, [ 0>=1+U ], cost: 1
    124: f111 -> f119 : V'=0, [ U>=1 ], cost: 1
    125: f111 -> f119 : U'=0, V'=1, [ U==0 ], cost: 1
    110: f83 -> f101 : Q'=1, S'=1, [ 9>=K && 9>=G && 9>=F && 9>=E && 9>=D && 9>=C && 9>=B && 9>=A ], cost: 1
    111: f83 -> f101 : Q'=0, S'=0, [ K>=10 && 9>=G && 9>=F && 9>=E && 9>=D && 9>=C && 9>=B && 9>=A ], cost: 1
    112: f83 -> f101 : Q'=0, S'=0, [ G>=10 && 9>=F && 9>=E && 9>=D && 9>=C && 9>=B && 9>=A ], cost: 1
    113: f83 -> f101 : Q'=0, S'=0, [ F>=10 && 9>=E && 9>=D && 9>=C && 9>=B && 9>=A ], cost: 1
    114: f83 -> f101 : Q'=0, S'=0, [ E>=10 && 9>=D && 9>=C && 9>=B && 9>=A ], cost: 1
    115: f83 -> f101 : Q'=0, S'=0, [ D>=10 && 9>=C && 9>=B && 9>=A ], cost: 1
    116: f83 -> f101 : Q'=0, S'=0, [ C>=10 && 9>=B && 9>=A ], cost: 1
    117: f83 -> f101 : Q'=0, S'=0, [ 9>=B && A>=10 ], cost: 1
    118: f83 -> f101 : Q'=0, S'=0, [ B>=10 ], cost: 1


Simplified the transitions:
  Start location: f0
    <empty>


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: f0
    <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),?)