Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: f0
      0: f0 -> f18 : A'=100, B'=0, [], cost: 1
      1: f0 -> f18 : A'=100, B'=10, [], cost: 1
      2: f18 -> f21 : C'=B, [ 0>=1+B ], cost: 1
      3: f18 -> f21 : C'=B, [ B>=1 ], cost: 1
      4: f18 -> f46 : B'=0, C'=0, [ B==0 ], cost: 1
      5: f21 -> f27 : D'=0, [], cost: 1
      6: f21 -> f27 : D'=10, [], cost: 1
     10: f46 -> f58 : G'=200, H'=0, [], cost: 1
     11: f46 -> f58 : G'=200, H'=10, [], cost: 1
      7: f27 -> f46 : D'=0, E'=0, [ D==0 ], cost: 1
      8: f27 -> f30 : E'=D, F'=0, [ 0>=1+D ], cost: 1
      9: f27 -> f30 : E'=D, F'=0, [ D>=1 ], cost: 1
     59: f30 -> f46 : [ F>=A ], cost: 1
     58: f30 -> f30 : F'=1+F, [ A>=1+F ], cost: 1
     12: f58 -> f61 : Q'=H, [ 0>=1+H ], cost: 1
     13: f58 -> f61 : Q'=H, [ H>=1 ], cost: 1
     14: f58 -> f86 : H'=0, Q'=0, [ H==0 ], cost: 1
     15: f61 -> f67 : J'=0, [], cost: 1
     16: f61 -> f67 : J'=10, [], cost: 1
     20: f86 -> f98 : M'=50, N'=0, [], cost: 1
     21: f86 -> f98 : M'=50, N'=10, [], cost: 1
     17: f67 -> f86 : J'=0, K'=0, [ J==0 ], cost: 1
     18: f67 -> f70 : K'=J, L'=0, [ 0>=1+J ], cost: 1
     19: f67 -> f70 : K'=J, L'=0, [ J>=1 ], cost: 1
     57: f70 -> f86 : [ L>=G ], cost: 1
     56: f70 -> f70 : L'=1+L, [ G>=1+L ], cost: 1
     22: f98 -> f101 : O'=N, [ 0>=1+N ], cost: 1
     23: f98 -> f101 : O'=N, [ N>=1 ], cost: 1
     24: f98 -> f126 : N'=0, O'=0, [ N==0 ], cost: 1
     25: f101 -> f107 : P'=0, [], cost: 1
     26: f101 -> f107 : P'=10, [], cost: 1
     30: f126 -> f138 : S'=20, T'=0, [], cost: 1
     31: f126 -> f138 : S'=20, T'=10, [], cost: 1
     27: f107 -> f126 : P'=0, Q_1'=0, [ P==0 ], cost: 1
     28: f107 -> f110 : Q_1'=P, R'=0, [ 0>=1+P ], cost: 1
     29: f107 -> f110 : Q_1'=P, R'=0, [ P>=1 ], cost: 1
     55: f110 -> f126 : [ R>=M ], cost: 1
     54: f110 -> f110 : R'=1+R, [ M>=1+R ], cost: 1
     32: f138 -> f141 : U'=T, [ 0>=1+T ], cost: 1
     33: f138 -> f141 : U'=T, [ T>=1 ], cost: 1
     34: f138 -> f166 : T'=0, U'=0, [ T==0 ], cost: 1
     35: f141 -> f147 : V'=0, [], cost: 1
     36: f141 -> f147 : V'=10, [], cost: 1
     40: f166 -> f178 : Y'=200, Z'=0, [], cost: 1
     41: f166 -> f178 : Y'=200, Z'=10, [], cost: 1
     37: f147 -> f166 : V'=0, W'=0, [ V==0 ], cost: 1
     38: f147 -> f150 : W'=V, X'=0, [ 0>=1+V ], cost: 1
     39: f147 -> f150 : W'=V, X'=0, [ V>=1 ], cost: 1
     53: f150 -> f166 : [ X>=S ], cost: 1
     52: f150 -> f150 : X'=1+X, [ S>=1+X ], cost: 1
     42: f178 -> f181 : A1'=Z, [ 0>=1+Z ], cost: 1
     43: f178 -> f181 : A1'=Z, [ Z>=1 ], cost: 1
     48: f178 -> f207 : Z'=0, A1'=0, [ Z==0 ], cost: 1
     44: f181 -> f187 : B1'=0, [], cost: 1
     45: f181 -> f187 : B1'=10, [], cost: 1
     46: f187 -> f190 : C1'=B1, D1'=0, [ 0>=1+B1 ], cost: 1
     47: f187 -> f190 : C1'=B1, D1'=0, [ B1>=1 ], cost: 1
     49: f187 -> f207 : B1'=0, C1'=0, [ B1==0 ], cost: 1
     50: f190 -> f190 : D1'=1+D1, [ Y>=1+D1 ], cost: 1
     51: f190 -> f207 : [ D1>=Y ], cost: 1


Simplified the transitions:
  Start location: f0
      0: f0 -> f18 : A'=100, B'=0, [], cost: 1
      1: f0 -> f18 : A'=100, B'=10, [], cost: 1
      2: f18 -> f21 : C'=B, [ 0>=1+B ], cost: 1
      3: f18 -> f21 : C'=B, [ B>=1 ], cost: 1
      4: f18 -> f46 : B'=0, C'=0, [ B==0 ], cost: 1
      5: f21 -> f27 : D'=0, [], cost: 1
      6: f21 -> f27 : D'=10, [], cost: 1
     10: f46 -> f58 : G'=200, H'=0, [], cost: 1
     11: f46 -> f58 : G'=200, H'=10, [], cost: 1
      7: f27 -> f46 : D'=0, E'=0, [ D==0 ], cost: 1
      8: f27 -> f30 : E'=D, F'=0, [ 0>=1+D ], cost: 1
      9: f27 -> f30 : E'=D, F'=0, [ D>=1 ], cost: 1
     59: f30 -> f46 : [ F>=A ], cost: 1
     58: f30 -> f30 : F'=1+F, [ A>=1+F ], cost: 1
     12: f58 -> f61 : Q'=H, [ 0>=1+H ], cost: 1
     13: f58 -> f61 : Q'=H, [ H>=1 ], cost: 1
     14: f58 -> f86 : H'=0, Q'=0, [ H==0 ], cost: 1
     15: f61 -> f67 : J'=0, [], cost: 1
     16: f61 -> f67 : J'=10, [], cost: 1
     20: f86 -> f98 : M'=50, N'=0, [], cost: 1
     21: f86 -> f98 : M'=50, N'=10, [], cost: 1
     17: f67 -> f86 : J'=0, K'=0, [ J==0 ], cost: 1
     18: f67 -> f70 : K'=J, L'=0, [ 0>=1+J ], cost: 1
     19: f67 -> f70 : K'=J, L'=0, [ J>=1 ], cost: 1
     57: f70 -> f86 : [ L>=G ], cost: 1
     56: f70 -> f70 : L'=1+L, [ G>=1+L ], cost: 1
     22: f98 -> f101 : O'=N, [ 0>=1+N ], cost: 1
     23: f98 -> f101 : O'=N, [ N>=1 ], cost: 1
     24: f98 -> f126 : N'=0, O'=0, [ N==0 ], cost: 1
     25: f101 -> f107 : P'=0, [], cost: 1
     26: f101 -> f107 : P'=10, [], cost: 1
     30: f126 -> f138 : S'=20, T'=0, [], cost: 1
     31: f126 -> f138 : S'=20, T'=10, [], cost: 1
     27: f107 -> f126 : P'=0, Q_1'=0, [ P==0 ], cost: 1
     28: f107 -> f110 : Q_1'=P, R'=0, [ 0>=1+P ], cost: 1
     29: f107 -> f110 : Q_1'=P, R'=0, [ P>=1 ], cost: 1
     55: f110 -> f126 : [ R>=M ], cost: 1
     54: f110 -> f110 : R'=1+R, [ M>=1+R ], cost: 1
     32: f138 -> f141 : U'=T, [ 0>=1+T ], cost: 1
     33: f138 -> f141 : U'=T, [ T>=1 ], cost: 1
     34: f138 -> f166 : T'=0, U'=0, [ T==0 ], cost: 1
     35: f141 -> f147 : V'=0, [], cost: 1
     36: f141 -> f147 : V'=10, [], cost: 1
     40: f166 -> f178 : Y'=200, Z'=0, [], cost: 1
     41: f166 -> f178 : Y'=200, Z'=10, [], cost: 1
     37: f147 -> f166 : V'=0, W'=0, [ V==0 ], cost: 1
     38: f147 -> f150 : W'=V, X'=0, [ 0>=1+V ], cost: 1
     39: f147 -> f150 : W'=V, X'=0, [ V>=1 ], cost: 1
     53: f150 -> f166 : [ X>=S ], cost: 1
     52: f150 -> f150 : X'=1+X, [ S>=1+X ], cost: 1
     42: f178 -> f181 : A1'=Z, [ 0>=1+Z ], cost: 1
     43: f178 -> f181 : A1'=Z, [ Z>=1 ], cost: 1
     44: f181 -> f187 : B1'=0, [], cost: 1
     45: f181 -> f187 : B1'=10, [], cost: 1
     46: f187 -> f190 : C1'=B1, D1'=0, [ 0>=1+B1 ], cost: 1
     47: f187 -> f190 : C1'=B1, D1'=0, [ B1>=1 ], cost: 1
     50: f190 -> f190 : D1'=1+D1, [ Y>=1+D1 ], cost: 1

Eliminating 1 self-loops for location f30
  Self-Loop 58 has the metering function: -F+A, resulting in the new transition 60.
  Removing the self-loops: 58.
Eliminating 1 self-loops for location f70
  Self-Loop 56 has the metering function: -L+G, resulting in the new transition 61.
  Removing the self-loops: 56.
Eliminating 1 self-loops for location f110
  Self-Loop 54 has the metering function: -R+M, resulting in the new transition 62.
  Removing the self-loops: 54.
Eliminating 1 self-loops for location f150
  Self-Loop 52 has the metering function: -X+S, resulting in the new transition 63.
  Removing the self-loops: 52.
Eliminating 1 self-loops for location f190
  Self-Loop 50 has the metering function: Y-D1, resulting in the new transition 64.
  Removing the self-loops: 50.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
      0: f0 -> f18 : A'=100, B'=0, [], cost: 1
      1: f0 -> f18 : A'=100, B'=10, [], cost: 1
      2: f18 -> f21 : C'=B, [ 0>=1+B ], cost: 1
      3: f18 -> f21 : C'=B, [ B>=1 ], cost: 1
      4: f18 -> f46 : B'=0, C'=0, [ B==0 ], cost: 1
      5: f21 -> f27 : D'=0, [], cost: 1
      6: f21 -> f27 : D'=10, [], cost: 1
     10: f46 -> f58 : G'=200, H'=0, [], cost: 1
     11: f46 -> f58 : G'=200, H'=10, [], cost: 1
      7: f27 -> f46 : D'=0, E'=0, [ D==0 ], cost: 1
      8: f27 -> f30 : E'=D, F'=0, [ 0>=1+D ], cost: 1
      9: f27 -> f30 : E'=D, F'=0, [ D>=1 ], cost: 1
     60: f30 -> [26] : F'=A, [ A>=1+F ], cost: -F+A
     12: f58 -> f61 : Q'=H, [ 0>=1+H ], cost: 1
     13: f58 -> f61 : Q'=H, [ H>=1 ], cost: 1
     14: f58 -> f86 : H'=0, Q'=0, [ H==0 ], cost: 1
     15: f61 -> f67 : J'=0, [], cost: 1
     16: f61 -> f67 : J'=10, [], cost: 1
     20: f86 -> f98 : M'=50, N'=0, [], cost: 1
     21: f86 -> f98 : M'=50, N'=10, [], cost: 1
     17: f67 -> f86 : J'=0, K'=0, [ J==0 ], cost: 1
     18: f67 -> f70 : K'=J, L'=0, [ 0>=1+J ], cost: 1
     19: f67 -> f70 : K'=J, L'=0, [ J>=1 ], cost: 1
     61: f70 -> [27] : L'=G, [ G>=1+L ], cost: -L+G
     22: f98 -> f101 : O'=N, [ 0>=1+N ], cost: 1
     23: f98 -> f101 : O'=N, [ N>=1 ], cost: 1
     24: f98 -> f126 : N'=0, O'=0, [ N==0 ], cost: 1
     25: f101 -> f107 : P'=0, [], cost: 1
     26: f101 -> f107 : P'=10, [], cost: 1
     30: f126 -> f138 : S'=20, T'=0, [], cost: 1
     31: f126 -> f138 : S'=20, T'=10, [], cost: 1
     27: f107 -> f126 : P'=0, Q_1'=0, [ P==0 ], cost: 1
     28: f107 -> f110 : Q_1'=P, R'=0, [ 0>=1+P ], cost: 1
     29: f107 -> f110 : Q_1'=P, R'=0, [ P>=1 ], cost: 1
     62: f110 -> [28] : R'=M, [ M>=1+R ], cost: -R+M
     32: f138 -> f141 : U'=T, [ 0>=1+T ], cost: 1
     33: f138 -> f141 : U'=T, [ T>=1 ], cost: 1
     34: f138 -> f166 : T'=0, U'=0, [ T==0 ], cost: 1
     35: f141 -> f147 : V'=0, [], cost: 1
     36: f141 -> f147 : V'=10, [], cost: 1
     40: f166 -> f178 : Y'=200, Z'=0, [], cost: 1
     41: f166 -> f178 : Y'=200, Z'=10, [], cost: 1
     37: f147 -> f166 : V'=0, W'=0, [ V==0 ], cost: 1
     38: f147 -> f150 : W'=V, X'=0, [ 0>=1+V ], cost: 1
     39: f147 -> f150 : W'=V, X'=0, [ V>=1 ], cost: 1
     63: f150 -> [29] : X'=S, [ S>=1+X ], cost: -X+S
     42: f178 -> f181 : A1'=Z, [ 0>=1+Z ], cost: 1
     43: f178 -> f181 : A1'=Z, [ Z>=1 ], cost: 1
     44: f181 -> f187 : B1'=0, [], cost: 1
     45: f181 -> f187 : B1'=10, [], cost: 1
     46: f187 -> f190 : C1'=B1, D1'=0, [ 0>=1+B1 ], cost: 1
     47: f187 -> f190 : C1'=B1, D1'=0, [ B1>=1 ], cost: 1
     64: f190 -> [30] : D1'=Y, [ Y>=1+D1 ], cost: Y-D1
     59: [26] -> f46 : [ F>=A ], cost: 1
     57: [27] -> f86 : [ L>=G ], cost: 1
     55: [28] -> f126 : [ R>=M ], cost: 1
     53: [29] -> f166 : [ X>=S ], cost: 1


Applied simple chaining:
  Start location: f0
      0: f0 -> f18 : A'=100, B'=0, [], cost: 1
      1: f0 -> f18 : A'=100, B'=10, [], cost: 1
      2: f18 -> f21 : C'=B, [ 0>=1+B ], cost: 1
      3: f18 -> f21 : C'=B, [ B>=1 ], cost: 1
      4: f18 -> f46 : B'=0, C'=0, [ B==0 ], cost: 1
      5: f21 -> f27 : D'=0, [], cost: 1
      6: f21 -> f27 : D'=10, [], cost: 1
     10: f46 -> f58 : G'=200, H'=0, [], cost: 1
     11: f46 -> f58 : G'=200, H'=10, [], cost: 1
      7: f27 -> f46 : D'=0, E'=0, [ D==0 ], cost: 1
      8: f27 -> f30 : E'=D, F'=0, [ 0>=1+D ], cost: 1
      9: f27 -> f30 : E'=D, F'=0, [ D>=1 ], cost: 1
     60: f30 -> f46 : F'=A, [ A>=1+F && A>=A ], cost: 1-F+A
     12: f58 -> f61 : Q'=H, [ 0>=1+H ], cost: 1
     13: f58 -> f61 : Q'=H, [ H>=1 ], cost: 1
     14: f58 -> f86 : H'=0, Q'=0, [ H==0 ], cost: 1
     15: f61 -> f67 : J'=0, [], cost: 1
     16: f61 -> f67 : J'=10, [], cost: 1
     20: f86 -> f98 : M'=50, N'=0, [], cost: 1
     21: f86 -> f98 : M'=50, N'=10, [], cost: 1
     17: f67 -> f86 : J'=0, K'=0, [ J==0 ], cost: 1
     18: f67 -> f70 : K'=J, L'=0, [ 0>=1+J ], cost: 1
     19: f67 -> f70 : K'=J, L'=0, [ J>=1 ], cost: 1
     61: f70 -> f86 : L'=G, [ G>=1+L && G>=G ], cost: 1-L+G
     22: f98 -> f101 : O'=N, [ 0>=1+N ], cost: 1
     23: f98 -> f101 : O'=N, [ N>=1 ], cost: 1
     24: f98 -> f126 : N'=0, O'=0, [ N==0 ], cost: 1
     25: f101 -> f107 : P'=0, [], cost: 1
     26: f101 -> f107 : P'=10, [], cost: 1
     30: f126 -> f138 : S'=20, T'=0, [], cost: 1
     31: f126 -> f138 : S'=20, T'=10, [], cost: 1
     27: f107 -> f126 : P'=0, Q_1'=0, [ P==0 ], cost: 1
     28: f107 -> f110 : Q_1'=P, R'=0, [ 0>=1+P ], cost: 1
     29: f107 -> f110 : Q_1'=P, R'=0, [ P>=1 ], cost: 1
     62: f110 -> f126 : R'=M, [ M>=1+R && M>=M ], cost: 1-R+M
     32: f138 -> f141 : U'=T, [ 0>=1+T ], cost: 1
     33: f138 -> f141 : U'=T, [ T>=1 ], cost: 1
     34: f138 -> f166 : T'=0, U'=0, [ T==0 ], cost: 1
     35: f141 -> f147 : V'=0, [], cost: 1
     36: f141 -> f147 : V'=10, [], cost: 1
     40: f166 -> f178 : Y'=200, Z'=0, [], cost: 1
     41: f166 -> f178 : Y'=200, Z'=10, [], cost: 1
     37: f147 -> f166 : V'=0, W'=0, [ V==0 ], cost: 1
     38: f147 -> f150 : W'=V, X'=0, [ 0>=1+V ], cost: 1
     39: f147 -> f150 : W'=V, X'=0, [ V>=1 ], cost: 1
     63: f150 -> f166 : X'=S, [ S>=1+X && S>=S ], cost: 1-X+S
     42: f178 -> f181 : A1'=Z, [ 0>=1+Z ], cost: 1
     43: f178 -> f181 : A1'=Z, [ Z>=1 ], cost: 1
     44: f181 -> f187 : B1'=0, [], cost: 1
     45: f181 -> f187 : B1'=10, [], cost: 1
     46: f187 -> f190 : C1'=B1, D1'=0, [ 0>=1+B1 ], cost: 1
     47: f187 -> f190 : C1'=B1, D1'=0, [ B1>=1 ], cost: 1
     64: f190 -> [30] : D1'=Y, [ Y>=1+D1 ], cost: Y-D1


Applied chaining over branches and pruning:
  Start location: f0
     66: f0 -> f21 : A'=100, B'=10, C'=10, [ 10>=1 ], cost: 2
     65: f0 -> f46 : A'=100, B'=0, C'=0, [ 0==0 ], cost: 2
     67: f21 -> f46 : D'=0, E'=0, [ 0==0 ], cost: 2
     68: f21 -> f30 : D'=10, E'=10, F'=0, [ 10>=1 ], cost: 2
     70: f46 -> f61 : G'=200, H'=10, Q'=10, [ 10>=1 ], cost: 2
     69: f46 -> f86 : G'=200, H'=0, Q'=0, [ 0==0 ], cost: 2
     60: f30 -> f46 : F'=A, [ A>=1+F && A>=A ], cost: 1-F+A
     71: f61 -> f86 : J'=0, K'=0, [ 0==0 ], cost: 2
     72: f61 -> f70 : J'=10, K'=10, L'=0, [ 10>=1 ], cost: 2
     74: f86 -> f101 : M'=50, N'=10, O'=10, [ 10>=1 ], cost: 2
     73: f86 -> f126 : M'=50, N'=0, O'=0, [ 0==0 ], cost: 2
     61: f70 -> f86 : L'=G, [ G>=1+L && G>=G ], cost: 1-L+G
     75: f101 -> f126 : P'=0, Q_1'=0, [ 0==0 ], cost: 2
     76: f101 -> f110 : P'=10, Q_1'=10, R'=0, [ 10>=1 ], cost: 2
     78: f126 -> f141 : S'=20, T'=10, U'=10, [ 10>=1 ], cost: 2
     77: f126 -> f166 : S'=20, T'=0, U'=0, [ 0==0 ], cost: 2
     62: f110 -> f126 : R'=M, [ M>=1+R && M>=M ], cost: 1-R+M
     79: f141 -> f166 : V'=0, W'=0, [ 0==0 ], cost: 2
     80: f141 -> f150 : V'=10, W'=10, X'=0, [ 10>=1 ], cost: 2
     81: f166 -> f181 : Y'=200, Z'=10, A1'=10, [ 10>=1 ], cost: 2
     63: f150 -> f166 : X'=S, [ S>=1+X && S>=S ], cost: 1-X+S
     82: f181 -> f190 : B1'=10, C1'=10, D1'=0, [ 10>=1 ], cost: 2
     64: f190 -> [30] : D1'=Y, [ Y>=1+D1 ], cost: Y-D1


Applied simple chaining:
  Start location: f0
     66: f0 -> f21 : A'=100, B'=10, C'=10, [ 10>=1 ], cost: 2
     65: f0 -> f46 : A'=100, B'=0, C'=0, [ 0==0 ], cost: 2
     67: f21 -> f46 : D'=0, E'=0, [ 0==0 ], cost: 2
     68: f21 -> f46 : D'=10, E'=10, F'=A, [ 10>=1 && A>=1 && A>=A ], cost: 3+A
     70: f46 -> f61 : G'=200, H'=10, Q'=10, [ 10>=1 ], cost: 2
     69: f46 -> f86 : G'=200, H'=0, Q'=0, [ 0==0 ], cost: 2
     71: f61 -> f86 : J'=0, K'=0, [ 0==0 ], cost: 2
     72: f61 -> f86 : J'=10, K'=10, L'=G, [ 10>=1 && G>=1 && G>=G ], cost: 3+G
     74: f86 -> f101 : M'=50, N'=10, O'=10, [ 10>=1 ], cost: 2
     73: f86 -> f126 : M'=50, N'=0, O'=0, [ 0==0 ], cost: 2
     75: f101 -> f126 : P'=0, Q_1'=0, [ 0==0 ], cost: 2
     76: f101 -> f126 : P'=10, Q_1'=10, R'=M, [ 10>=1 && M>=1 && M>=M ], cost: 3+M
     78: f126 -> f141 : S'=20, T'=10, U'=10, [ 10>=1 ], cost: 2
     77: f126 -> f166 : S'=20, T'=0, U'=0, [ 0==0 ], cost: 2
     79: f141 -> f166 : V'=0, W'=0, [ 0==0 ], cost: 2
     80: f141 -> f166 : V'=10, W'=10, X'=S, [ 10>=1 && S>=1 && S>=S ], cost: 3+S
     81: f166 -> [30] : Y'=200, Z'=10, A1'=10, B1'=10, C1'=10, D1'=200, [ 10>=1 && 10>=1 && 200>=1 ], cost: 204


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