Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: f0
      0: f0 -> f17 : A'=100, B'=0, [], cost: 1
      1: f0 -> f17 : A'=100, B'=10, [], cost: 1
      2: f17 -> f20 : C'=B, [ 0>=1+B ], cost: 1
      3: f17 -> f20 : C'=B, [ B>=1 ], cost: 1
      4: f17 -> f45 : B'=0, C'=0, [ B==0 ], cost: 1
      5: f20 -> f26 : D'=0, [], cost: 1
      6: f20 -> f26 : D'=10, [], cost: 1
     10: f45 -> f57 : G'=200, H'=0, [], cost: 1
     11: f45 -> f57 : G'=200, H'=10, [], cost: 1
      7: f26 -> f45 : D'=0, E'=0, [ D==0 ], cost: 1
      8: f26 -> f29 : E'=D, F'=0, [ 0>=1+D ], cost: 1
      9: f26 -> f29 : E'=D, F'=0, [ D>=1 ], cost: 1
     47: f29 -> f45 : [ F>=A ], cost: 1
     46: f29 -> f29 : F'=1+F, [ A>=1+F ], cost: 1
     12: f57 -> f60 : Q'=H, [ 0>=1+H ], cost: 1
     13: f57 -> f60 : Q'=H, [ H>=1 ], cost: 1
     14: f57 -> f85 : H'=0, Q'=0, [ H==0 ], cost: 1
     15: f60 -> f66 : J'=0, [], cost: 1
     16: f60 -> f66 : J'=10, [], cost: 1
     20: f85 -> f97 : M'=50, N'=0, [], cost: 1
     21: f85 -> f97 : M'=50, N'=10, [], cost: 1
     17: f66 -> f85 : J'=0, K'=0, [ J==0 ], cost: 1
     18: f66 -> f69 : K'=J, L'=0, [ 0>=1+J ], cost: 1
     19: f66 -> f69 : K'=J, L'=0, [ J>=1 ], cost: 1
     45: f69 -> f85 : [ L>=G ], cost: 1
     44: f69 -> f69 : L'=1+L, [ G>=1+L ], cost: 1
     22: f97 -> f100 : O'=N, [ 0>=1+N ], cost: 1
     23: f97 -> f100 : O'=N, [ N>=1 ], cost: 1
     24: f97 -> f125 : N'=0, O'=0, [ N==0 ], cost: 1
     25: f100 -> f106 : P'=0, [], cost: 1
     26: f100 -> f106 : P'=10, [], cost: 1
     30: f125 -> f137 : S'=20, T'=0, [], cost: 1
     31: f125 -> f137 : S'=20, T'=10, [], cost: 1
     27: f106 -> f125 : P'=0, Q_1'=0, [ P==0 ], cost: 1
     28: f106 -> f109 : Q_1'=P, R'=0, [ 0>=1+P ], cost: 1
     29: f106 -> f109 : Q_1'=P, R'=0, [ P>=1 ], cost: 1
     43: f109 -> f125 : [ R>=M ], cost: 1
     42: f109 -> f109 : R'=1+R, [ M>=1+R ], cost: 1
     32: f137 -> f140 : U'=T, [ 0>=1+T ], cost: 1
     33: f137 -> f140 : U'=T, [ T>=1 ], cost: 1
     38: f137 -> f166 : T'=0, U'=0, [ T==0 ], cost: 1
     34: f140 -> f146 : V'=0, [], cost: 1
     35: f140 -> f146 : V'=10, [], cost: 1
     36: f146 -> f149 : W'=V, X'=0, [ 0>=1+V ], cost: 1
     37: f146 -> f149 : W'=V, X'=0, [ V>=1 ], cost: 1
     39: f146 -> f166 : V'=0, W'=0, [ V==0 ], cost: 1
     40: f149 -> f149 : X'=1+X, [ S>=1+X ], cost: 1
     41: f149 -> f166 : [ X>=S ], cost: 1


Simplified the transitions:
  Start location: f0
      0: f0 -> f17 : A'=100, B'=0, [], cost: 1
      1: f0 -> f17 : A'=100, B'=10, [], cost: 1
      2: f17 -> f20 : C'=B, [ 0>=1+B ], cost: 1
      3: f17 -> f20 : C'=B, [ B>=1 ], cost: 1
      4: f17 -> f45 : B'=0, C'=0, [ B==0 ], cost: 1
      5: f20 -> f26 : D'=0, [], cost: 1
      6: f20 -> f26 : D'=10, [], cost: 1
     10: f45 -> f57 : G'=200, H'=0, [], cost: 1
     11: f45 -> f57 : G'=200, H'=10, [], cost: 1
      7: f26 -> f45 : D'=0, E'=0, [ D==0 ], cost: 1
      8: f26 -> f29 : E'=D, F'=0, [ 0>=1+D ], cost: 1
      9: f26 -> f29 : E'=D, F'=0, [ D>=1 ], cost: 1
     47: f29 -> f45 : [ F>=A ], cost: 1
     46: f29 -> f29 : F'=1+F, [ A>=1+F ], cost: 1
     12: f57 -> f60 : Q'=H, [ 0>=1+H ], cost: 1
     13: f57 -> f60 : Q'=H, [ H>=1 ], cost: 1
     14: f57 -> f85 : H'=0, Q'=0, [ H==0 ], cost: 1
     15: f60 -> f66 : J'=0, [], cost: 1
     16: f60 -> f66 : J'=10, [], cost: 1
     20: f85 -> f97 : M'=50, N'=0, [], cost: 1
     21: f85 -> f97 : M'=50, N'=10, [], cost: 1
     17: f66 -> f85 : J'=0, K'=0, [ J==0 ], cost: 1
     18: f66 -> f69 : K'=J, L'=0, [ 0>=1+J ], cost: 1
     19: f66 -> f69 : K'=J, L'=0, [ J>=1 ], cost: 1
     45: f69 -> f85 : [ L>=G ], cost: 1
     44: f69 -> f69 : L'=1+L, [ G>=1+L ], cost: 1
     22: f97 -> f100 : O'=N, [ 0>=1+N ], cost: 1
     23: f97 -> f100 : O'=N, [ N>=1 ], cost: 1
     24: f97 -> f125 : N'=0, O'=0, [ N==0 ], cost: 1
     25: f100 -> f106 : P'=0, [], cost: 1
     26: f100 -> f106 : P'=10, [], cost: 1
     30: f125 -> f137 : S'=20, T'=0, [], cost: 1
     31: f125 -> f137 : S'=20, T'=10, [], cost: 1
     27: f106 -> f125 : P'=0, Q_1'=0, [ P==0 ], cost: 1
     28: f106 -> f109 : Q_1'=P, R'=0, [ 0>=1+P ], cost: 1
     29: f106 -> f109 : Q_1'=P, R'=0, [ P>=1 ], cost: 1
     43: f109 -> f125 : [ R>=M ], cost: 1
     42: f109 -> f109 : R'=1+R, [ M>=1+R ], cost: 1
     32: f137 -> f140 : U'=T, [ 0>=1+T ], cost: 1
     33: f137 -> f140 : U'=T, [ T>=1 ], cost: 1
     34: f140 -> f146 : V'=0, [], cost: 1
     35: f140 -> f146 : V'=10, [], cost: 1
     36: f146 -> f149 : W'=V, X'=0, [ 0>=1+V ], cost: 1
     37: f146 -> f149 : W'=V, X'=0, [ V>=1 ], cost: 1
     40: f149 -> f149 : X'=1+X, [ S>=1+X ], cost: 1

Eliminating 1 self-loops for location f29
  Self-Loop 46 has the metering function: -F+A, resulting in the new transition 48.
  Removing the self-loops: 46.
Eliminating 1 self-loops for location f69
  Self-Loop 44 has the metering function: -L+G, resulting in the new transition 49.
  Removing the self-loops: 44.
Eliminating 1 self-loops for location f109
  Self-Loop 42 has the metering function: -R+M, resulting in the new transition 50.
  Removing the self-loops: 42.
Eliminating 1 self-loops for location f149
  Self-Loop 40 has the metering function: -X+S, resulting in the new transition 51.
  Removing the self-loops: 40.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
      0: f0 -> f17 : A'=100, B'=0, [], cost: 1
      1: f0 -> f17 : A'=100, B'=10, [], cost: 1
      2: f17 -> f20 : C'=B, [ 0>=1+B ], cost: 1
      3: f17 -> f20 : C'=B, [ B>=1 ], cost: 1
      4: f17 -> f45 : B'=0, C'=0, [ B==0 ], cost: 1
      5: f20 -> f26 : D'=0, [], cost: 1
      6: f20 -> f26 : D'=10, [], cost: 1
     10: f45 -> f57 : G'=200, H'=0, [], cost: 1
     11: f45 -> f57 : G'=200, H'=10, [], cost: 1
      7: f26 -> f45 : D'=0, E'=0, [ D==0 ], cost: 1
      8: f26 -> f29 : E'=D, F'=0, [ 0>=1+D ], cost: 1
      9: f26 -> f29 : E'=D, F'=0, [ D>=1 ], cost: 1
     48: f29 -> [21] : F'=A, [ A>=1+F ], cost: -F+A
     12: f57 -> f60 : Q'=H, [ 0>=1+H ], cost: 1
     13: f57 -> f60 : Q'=H, [ H>=1 ], cost: 1
     14: f57 -> f85 : H'=0, Q'=0, [ H==0 ], cost: 1
     15: f60 -> f66 : J'=0, [], cost: 1
     16: f60 -> f66 : J'=10, [], cost: 1
     20: f85 -> f97 : M'=50, N'=0, [], cost: 1
     21: f85 -> f97 : M'=50, N'=10, [], cost: 1
     17: f66 -> f85 : J'=0, K'=0, [ J==0 ], cost: 1
     18: f66 -> f69 : K'=J, L'=0, [ 0>=1+J ], cost: 1
     19: f66 -> f69 : K'=J, L'=0, [ J>=1 ], cost: 1
     49: f69 -> [22] : L'=G, [ G>=1+L ], cost: -L+G
     22: f97 -> f100 : O'=N, [ 0>=1+N ], cost: 1
     23: f97 -> f100 : O'=N, [ N>=1 ], cost: 1
     24: f97 -> f125 : N'=0, O'=0, [ N==0 ], cost: 1
     25: f100 -> f106 : P'=0, [], cost: 1
     26: f100 -> f106 : P'=10, [], cost: 1
     30: f125 -> f137 : S'=20, T'=0, [], cost: 1
     31: f125 -> f137 : S'=20, T'=10, [], cost: 1
     27: f106 -> f125 : P'=0, Q_1'=0, [ P==0 ], cost: 1
     28: f106 -> f109 : Q_1'=P, R'=0, [ 0>=1+P ], cost: 1
     29: f106 -> f109 : Q_1'=P, R'=0, [ P>=1 ], cost: 1
     50: f109 -> [23] : R'=M, [ M>=1+R ], cost: -R+M
     32: f137 -> f140 : U'=T, [ 0>=1+T ], cost: 1
     33: f137 -> f140 : U'=T, [ T>=1 ], cost: 1
     34: f140 -> f146 : V'=0, [], cost: 1
     35: f140 -> f146 : V'=10, [], cost: 1
     36: f146 -> f149 : W'=V, X'=0, [ 0>=1+V ], cost: 1
     37: f146 -> f149 : W'=V, X'=0, [ V>=1 ], cost: 1
     51: f149 -> [24] : X'=S, [ S>=1+X ], cost: -X+S
     47: [21] -> f45 : [ F>=A ], cost: 1
     45: [22] -> f85 : [ L>=G ], cost: 1
     43: [23] -> f125 : [ R>=M ], cost: 1


Applied simple chaining:
  Start location: f0
      0: f0 -> f17 : A'=100, B'=0, [], cost: 1
      1: f0 -> f17 : A'=100, B'=10, [], cost: 1
      2: f17 -> f20 : C'=B, [ 0>=1+B ], cost: 1
      3: f17 -> f20 : C'=B, [ B>=1 ], cost: 1
      4: f17 -> f45 : B'=0, C'=0, [ B==0 ], cost: 1
      5: f20 -> f26 : D'=0, [], cost: 1
      6: f20 -> f26 : D'=10, [], cost: 1
     10: f45 -> f57 : G'=200, H'=0, [], cost: 1
     11: f45 -> f57 : G'=200, H'=10, [], cost: 1
      7: f26 -> f45 : D'=0, E'=0, [ D==0 ], cost: 1
      8: f26 -> f29 : E'=D, F'=0, [ 0>=1+D ], cost: 1
      9: f26 -> f29 : E'=D, F'=0, [ D>=1 ], cost: 1
     48: f29 -> f45 : F'=A, [ A>=1+F && A>=A ], cost: 1-F+A
     12: f57 -> f60 : Q'=H, [ 0>=1+H ], cost: 1
     13: f57 -> f60 : Q'=H, [ H>=1 ], cost: 1
     14: f57 -> f85 : H'=0, Q'=0, [ H==0 ], cost: 1
     15: f60 -> f66 : J'=0, [], cost: 1
     16: f60 -> f66 : J'=10, [], cost: 1
     20: f85 -> f97 : M'=50, N'=0, [], cost: 1
     21: f85 -> f97 : M'=50, N'=10, [], cost: 1
     17: f66 -> f85 : J'=0, K'=0, [ J==0 ], cost: 1
     18: f66 -> f69 : K'=J, L'=0, [ 0>=1+J ], cost: 1
     19: f66 -> f69 : K'=J, L'=0, [ J>=1 ], cost: 1
     49: f69 -> f85 : L'=G, [ G>=1+L && G>=G ], cost: 1-L+G
     22: f97 -> f100 : O'=N, [ 0>=1+N ], cost: 1
     23: f97 -> f100 : O'=N, [ N>=1 ], cost: 1
     24: f97 -> f125 : N'=0, O'=0, [ N==0 ], cost: 1
     25: f100 -> f106 : P'=0, [], cost: 1
     26: f100 -> f106 : P'=10, [], cost: 1
     30: f125 -> f137 : S'=20, T'=0, [], cost: 1
     31: f125 -> f137 : S'=20, T'=10, [], cost: 1
     27: f106 -> f125 : P'=0, Q_1'=0, [ P==0 ], cost: 1
     28: f106 -> f109 : Q_1'=P, R'=0, [ 0>=1+P ], cost: 1
     29: f106 -> f109 : Q_1'=P, R'=0, [ P>=1 ], cost: 1
     50: f109 -> f125 : R'=M, [ M>=1+R && M>=M ], cost: 1-R+M
     32: f137 -> f140 : U'=T, [ 0>=1+T ], cost: 1
     33: f137 -> f140 : U'=T, [ T>=1 ], cost: 1
     34: f140 -> f146 : V'=0, [], cost: 1
     35: f140 -> f146 : V'=10, [], cost: 1
     36: f146 -> f149 : W'=V, X'=0, [ 0>=1+V ], cost: 1
     37: f146 -> f149 : W'=V, X'=0, [ V>=1 ], cost: 1
     51: f149 -> [24] : X'=S, [ S>=1+X ], cost: -X+S


Applied chaining over branches and pruning:
  Start location: f0
     53: f0 -> f20 : A'=100, B'=10, C'=10, [ 10>=1 ], cost: 2
     52: f0 -> f45 : A'=100, B'=0, C'=0, [ 0==0 ], cost: 2
     54: f20 -> f45 : D'=0, E'=0, [ 0==0 ], cost: 2
     55: f20 -> f29 : D'=10, E'=10, F'=0, [ 10>=1 ], cost: 2
     57: f45 -> f60 : G'=200, H'=10, Q'=10, [ 10>=1 ], cost: 2
     56: f45 -> f85 : G'=200, H'=0, Q'=0, [ 0==0 ], cost: 2
     48: f29 -> f45 : F'=A, [ A>=1+F && A>=A ], cost: 1-F+A
     58: f60 -> f85 : J'=0, K'=0, [ 0==0 ], cost: 2
     59: f60 -> f69 : J'=10, K'=10, L'=0, [ 10>=1 ], cost: 2
     61: f85 -> f100 : M'=50, N'=10, O'=10, [ 10>=1 ], cost: 2
     60: f85 -> f125 : M'=50, N'=0, O'=0, [ 0==0 ], cost: 2
     49: f69 -> f85 : L'=G, [ G>=1+L && G>=G ], cost: 1-L+G
     62: f100 -> f125 : P'=0, Q_1'=0, [ 0==0 ], cost: 2
     63: f100 -> f109 : P'=10, Q_1'=10, R'=0, [ 10>=1 ], cost: 2
     64: f125 -> f140 : S'=20, T'=10, U'=10, [ 10>=1 ], cost: 2
     50: f109 -> f125 : R'=M, [ M>=1+R && M>=M ], cost: 1-R+M
     65: f140 -> f149 : V'=10, W'=10, X'=0, [ 10>=1 ], cost: 2
     51: f149 -> [24] : X'=S, [ S>=1+X ], cost: -X+S


Applied simple chaining:
  Start location: f0
     53: f0 -> f20 : A'=100, B'=10, C'=10, [ 10>=1 ], cost: 2
     52: f0 -> f45 : A'=100, B'=0, C'=0, [ 0==0 ], cost: 2
     54: f20 -> f45 : D'=0, E'=0, [ 0==0 ], cost: 2
     55: f20 -> f45 : D'=10, E'=10, F'=A, [ 10>=1 && A>=1 && A>=A ], cost: 3+A
     57: f45 -> f60 : G'=200, H'=10, Q'=10, [ 10>=1 ], cost: 2
     56: f45 -> f85 : G'=200, H'=0, Q'=0, [ 0==0 ], cost: 2
     58: f60 -> f85 : J'=0, K'=0, [ 0==0 ], cost: 2
     59: f60 -> f85 : J'=10, K'=10, L'=G, [ 10>=1 && G>=1 && G>=G ], cost: 3+G
     61: f85 -> f100 : M'=50, N'=10, O'=10, [ 10>=1 ], cost: 2
     60: f85 -> f125 : M'=50, N'=0, O'=0, [ 0==0 ], cost: 2
     62: f100 -> f125 : P'=0, Q_1'=0, [ 0==0 ], cost: 2
     63: f100 -> f125 : P'=10, Q_1'=10, R'=M, [ 10>=1 && M>=1 && M>=M ], cost: 3+M
     64: f125 -> [24] : S'=20, T'=10, U'=10, V'=10, W'=10, X'=20, [ 10>=1 && 10>=1 && 20>=1 ], cost: 24


Applied chaining over branches and pruning:
  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),?)