Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: f0
      0: f0 -> f15 : A'=1, B'=4, C'=free, D'=0, E'=free_1, F'=0, G'=0, H'=0, Q'=0, J'=0, [ free>=0 && free_1>=0 ], cost: 1
      1: f15 -> f36 : D'=1+D, F'=0, G'=0, H'=0, Q'=0, J'=0, [ 0>=D && 0>=C && B>=1 && Q==0 ], cost: 1
      2: f15 -> f36 : B'=-1+B, D'=0, F'=free_2, G'=0, H'=0, Q'=0, J'=0, [ D>=1 && 0>=C && free_2>=0 && B>=1 && 1>=free_2 && Q==0 ], cost: 1
      3: f15 -> f36 : A'=1+A, B'=4+A, C'=free_3, D'=0, F'=free_4, G'=0, H'=0, Q'=0, J'=0, [ 0>=C && free_4>=0 && 1>=free_4 && 0>=B && free_3>=0 && Q==0 ], cost: 1
      4: f15 -> f36 : C'=-1+C, F'=free_5, G'=0, H'=0, Q'=0, J'=0, [ C>=1 && 1>=free_5 && free_5>=0 && Q==0 ], cost: 1
     19: f15 -> f81 : [ 0>=1+Q ], cost: 1
     20: f15 -> f81 : [ Q>=1 ], cost: 1
      5: f36 -> f77 : [ 0>=H && J>=1+E ], cost: 1
      6: f36 -> f77 : [ H>=1 ], cost: 1
      7: f36 -> f48 : D'=1+D, G'=0, [ E>=J && 0>=H && 0>=D && 0>=C && B>=1 ], cost: 1
      8: f36 -> f48 : B'=-1+B, D'=0, G'=free_6, [ E>=J && 0>=H && D>=1 && 0>=C && free_6>=0 && B>=1 && 1>=free_6 ], cost: 1
      9: f36 -> f48 : A'=1+A, B'=4+A, C'=free_7, D'=0, G'=free_8, [ E>=J && 0>=H && 0>=C && free_8>=0 && 1>=free_8 && 0>=B && free_7>=0 ], cost: 1
     10: f36 -> f48 : C'=-1+C, G'=free_9, [ E>=J && 0>=H && C>=1 && 1>=free_9 && free_9>=0 ], cost: 1
     17: f77 -> f15 : [ H>=1 ], cost: 1
     18: f77 -> f15 : Q'=1, [ 0>=H ], cost: 1
     11: f48 -> f36 : J'=1+J, [ 0>=G ], cost: 1
     12: f48 -> f36 : J'=1+J, [ F>=1 && G>=1 ], cost: 1
     13: f48 -> f36 : D'=1+D, H'=0, J'=1+J, [ G>=1 && 0>=F && 1+E>=A && 0>=D && 0>=C && B>=1 ], cost: 1
     14: f48 -> f36 : B'=-1+B, D'=0, H'=free_10, J'=1+J, [ G>=1 && 0>=F && 1+E>=A && D>=1 && 0>=C && free_10>=0 && B>=1 && 1>=free_10 ], cost: 1
     15: f48 -> f36 : A'=1+A, B'=4+A, C'=free_11, D'=0, H'=free_12, J'=1+J, [ G>=1 && 0>=F && E>=A && 0>=C && free_12>=0 && 1>=free_12 && 0>=B && free_11>=0 ], cost: 1
     16: f48 -> f36 : C'=-1+C, H'=free_13, J'=1+J, [ G>=1 && 0>=F && 1+E>=A && C>=1 && 1>=free_13 && free_13>=0 ], cost: 1


Simplified the transitions:
  Start location: f0
      0: f0 -> f15 : A'=1, B'=4, C'=free, D'=0, E'=free_1, F'=0, G'=0, H'=0, Q'=0, J'=0, [ free>=0 && free_1>=0 ], cost: 1
      1: f15 -> f36 : D'=1+D, F'=0, G'=0, H'=0, Q'=0, J'=0, [ 0>=D && 0>=C && B>=1 && Q==0 ], cost: 1
      2: f15 -> f36 : B'=-1+B, D'=0, F'=free_2, G'=0, H'=0, Q'=0, J'=0, [ D>=1 && 0>=C && free_2>=0 && B>=1 && 1>=free_2 && Q==0 ], cost: 1
      3: f15 -> f36 : A'=1+A, B'=4+A, C'=free_3, D'=0, F'=free_4, G'=0, H'=0, Q'=0, J'=0, [ 0>=C && free_4>=0 && 1>=free_4 && 0>=B && free_3>=0 && Q==0 ], cost: 1
      4: f15 -> f36 : C'=-1+C, F'=free_5, G'=0, H'=0, Q'=0, J'=0, [ C>=1 && 1>=free_5 && free_5>=0 && Q==0 ], cost: 1
      5: f36 -> f77 : [ 0>=H && J>=1+E ], cost: 1
      6: f36 -> f77 : [ H>=1 ], cost: 1
      7: f36 -> f48 : D'=1+D, G'=0, [ E>=J && 0>=H && 0>=D && 0>=C && B>=1 ], cost: 1
      8: f36 -> f48 : B'=-1+B, D'=0, G'=free_6, [ E>=J && 0>=H && D>=1 && 0>=C && free_6>=0 && B>=1 && 1>=free_6 ], cost: 1
      9: f36 -> f48 : A'=1+A, B'=4+A, C'=free_7, D'=0, G'=free_8, [ E>=J && 0>=H && 0>=C && free_8>=0 && 1>=free_8 && 0>=B && free_7>=0 ], cost: 1
     10: f36 -> f48 : C'=-1+C, G'=free_9, [ E>=J && 0>=H && C>=1 && 1>=free_9 && free_9>=0 ], cost: 1
     17: f77 -> f15 : [ H>=1 ], cost: 1
     18: f77 -> f15 : Q'=1, [ 0>=H ], cost: 1
     11: f48 -> f36 : J'=1+J, [ 0>=G ], cost: 1
     12: f48 -> f36 : J'=1+J, [ F>=1 && G>=1 ], cost: 1
     13: f48 -> f36 : D'=1+D, H'=0, J'=1+J, [ G>=1 && 0>=F && 1+E>=A && 0>=D && 0>=C && B>=1 ], cost: 1
     14: f48 -> f36 : B'=-1+B, D'=0, H'=free_10, J'=1+J, [ G>=1 && 0>=F && 1+E>=A && D>=1 && 0>=C && free_10>=0 && B>=1 && 1>=free_10 ], cost: 1
     15: f48 -> f36 : A'=1+A, B'=4+A, C'=free_11, D'=0, H'=free_12, J'=1+J, [ G>=1 && 0>=F && E>=A && 0>=C && free_12>=0 && 1>=free_12 && 0>=B && free_11>=0 ], cost: 1
     16: f48 -> f36 : C'=-1+C, H'=free_13, J'=1+J, [ G>=1 && 0>=F && 1+E>=A && C>=1 && 1>=free_13 && free_13>=0 ], cost: 1


Applied chaining over branches and pruning:
  Start location: f0
      0: f0 -> f15 : A'=1, B'=4, C'=free, D'=0, E'=free_1, F'=0, G'=0, H'=0, Q'=0, J'=0, [ free>=0 && free_1>=0 ], cost: 1
      1: f15 -> f36 : D'=1+D, F'=0, G'=0, H'=0, Q'=0, J'=0, [ 0>=D && 0>=C && B>=1 && Q==0 ], cost: 1
      2: f15 -> f36 : B'=-1+B, D'=0, F'=free_2, G'=0, H'=0, Q'=0, J'=0, [ D>=1 && 0>=C && free_2>=0 && B>=1 && 1>=free_2 && Q==0 ], cost: 1
      3: f15 -> f36 : A'=1+A, B'=4+A, C'=free_3, D'=0, F'=free_4, G'=0, H'=0, Q'=0, J'=0, [ 0>=C && free_4>=0 && 1>=free_4 && 0>=B && free_3>=0 && Q==0 ], cost: 1
      4: f15 -> f36 : C'=-1+C, F'=free_5, G'=0, H'=0, Q'=0, J'=0, [ C>=1 && 1>=free_5 && free_5>=0 && Q==0 ], cost: 1
     21: f36 -> f15 : Q'=1, [ 0>=H && J>=1+E && 0>=H ], cost: 2
     22: f36 -> f15 : [ H>=1 && H>=1 ], cost: 2
     23: f36 -> f36 : D'=1+D, G'=0, J'=1+J, [ E>=J && 0>=H && 0>=D && 0>=C && B>=1 && 0>=0 ], cost: 2
     24: f36 -> f36 : B'=-1+B, D'=0, G'=free_6, J'=1+J, [ E>=J && 0>=H && D>=1 && 0>=C && free_6>=0 && B>=1 && 1>=free_6 && 0>=free_6 ], cost: 2
     26: f36 -> f36 : B'=-1+B, D'=1, G'=free_6, H'=0, J'=1+J, [ E>=J && 0>=H && D>=1 && 0>=C && free_6>=0 && B>=1 && 1>=free_6 && free_6>=1 && 0>=F && 1+E>=A && 0>=0 && 0>=C && -1+B>=1 ], cost: 2
     30: f36 -> f36 : A'=1+A, B'=4+A, C'=free_7, D'=1, G'=free_8, H'=0, J'=1+J, [ E>=J && 0>=H && 0>=C && free_8>=0 && 1>=free_8 && 0>=B && free_7>=0 && free_8>=1 && 0>=F && 1+E>=1+A && 0>=0 && 0>=free_7 && 4+A>=1 ], cost: 2
     32: f36 -> f36 : A'=1+A, B'=4+A, C'=-1+free_7, D'=0, G'=free_8, H'=free_13, J'=1+J, [ E>=J && 0>=H && 0>=C && free_8>=0 && 1>=free_8 && 0>=B && free_7>=0 && free_8>=1 && 0>=F && 1+E>=1+A && free_7>=1 && 1>=free_13 && free_13>=0 ], cost: 2

Eliminating 5 self-loops for location f36
  Removing the self-loops: 23 24 26 30 32 39 40 42 43 45 46 49 50.
Adding an epsilon transition (to model nonexecution of the loops): 52.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
      0: f0 -> f15 : A'=1, B'=4, C'=free, D'=0, E'=free_1, F'=0, G'=0, H'=0, Q'=0, J'=0, [ free>=0 && free_1>=0 ], cost: 1
      1: f15 -> f36 : D'=1+D, F'=0, G'=0, H'=0, Q'=0, J'=0, [ 0>=D && 0>=C && B>=1 && Q==0 ], cost: 1
      2: f15 -> f36 : B'=-1+B, D'=0, F'=free_2, G'=0, H'=0, Q'=0, J'=0, [ D>=1 && 0>=C && free_2>=0 && B>=1 && 1>=free_2 && Q==0 ], cost: 1
      3: f15 -> f36 : A'=1+A, B'=4+A, C'=free_3, D'=0, F'=free_4, G'=0, H'=0, Q'=0, J'=0, [ 0>=C && free_4>=0 && 1>=free_4 && 0>=B && free_3>=0 && Q==0 ], cost: 1
      4: f15 -> f36 : C'=-1+C, F'=free_5, G'=0, H'=0, Q'=0, J'=0, [ C>=1 && 1>=free_5 && free_5>=0 && Q==0 ], cost: 1
     41: f36 -> [6] : D'=1+D, G'=0, J'=1+J, [ E>=J && 0>=H && 0>=D && 0>=C && B>=1 ], cost: 2
     44: f36 -> [6] : B'=-1+B, D'=0, G'=0, J'=1+J, [ E>=J && 0>=H && D>=1 && 0>=C && B>=1 ], cost: 2
     47: f36 -> [6] : B'=-1+B, D'=1, G'=1, H'=0, J'=1+J, [ E>=J && 0>=H && D>=1 && 0>=C && 0>=F && 1+E>=A && -1+B>=1 ], cost: 2
     48: f36 -> [6] : A'=1+A, B'=4+A, C'=0, D'=1, G'=1, H'=0, J'=1+J, [ E>=J && 0>=H && 0>=C && 0>=B && 0>=F && 1+E>=1+A && 4+A>=1 ], cost: 2
     51: f36 -> [6] : A'=1+A, B'=4+A, C'=-1+free_7, D'=0, G'=1, H'=free_13, J'=1+J, [ E>=J && 0>=H && 0>=C && 0>=B && 0>=F && 1+E>=1+A && free_7>=1 && 1>=free_13 && free_13>=0 ], cost: 2
     52: f36 -> [6] : [], cost: 0
     21: [6] -> f15 : Q'=1, [ 0>=H && J>=1+E && 0>=H ], cost: 2
     22: [6] -> f15 : [ H>=1 && H>=1 ], cost: 2


Applied chaining over branches and pruning:
  Start location: f0
      0: f0 -> f15 : A'=1, B'=4, C'=free, D'=0, E'=free_1, F'=0, G'=0, H'=0, Q'=0, J'=0, [ free>=0 && free_1>=0 ], cost: 1
     53: f15 -> [6] : D'=2+D, F'=0, G'=0, H'=0, Q'=0, J'=1, [ 0>=D && 0>=C && B>=1 && Q==0 && E>=0 && 0>=0 && 0>=1+D && 0>=C && B>=1 ], cost: 3
     54: f15 -> [6] : B'=-1+B, D'=0, F'=0, G'=0, H'=0, Q'=0, J'=1, [ 0>=D && 0>=C && B>=1 && Q==0 && E>=0 && 0>=0 && 1+D>=1 && 0>=C && B>=1 ], cost: 3
     56: f15 -> [6] : D'=1+D, F'=0, G'=0, H'=0, Q'=0, J'=0, [ 0>=D && 0>=C && B>=1 && Q==0 ], cost: 1
     60: f15 -> [6] : B'=-1+B, D'=0, F'=free_2, G'=0, H'=0, Q'=0, J'=0, [ D>=1 && 0>=C && free_2>=0 && B>=1 && 1>=free_2 && Q==0 ], cost: 1
     62: f15 -> [6] : A'=2+A, B'=5+A, C'=0, D'=1, F'=free_4, G'=1, H'=0, Q'=0, J'=1, [ 0>=C && free_4>=0 && 1>=free_4 && 0>=B && free_3>=0 && Q==0 && E>=0 && 0>=0 && 0>=free_3 && 0>=4+A && 0>=free_4 && 1+E>=2+A && 5+A>=1 ], cost: 3
     21: [6] -> f15 : Q'=1, [ 0>=H && J>=1+E && 0>=H ], cost: 2
     22: [6] -> f15 : [ H>=1 && H>=1 ], cost: 2


Applied chaining over branches and pruning:
  Start location: f0
      0: f0 -> f15 : A'=1, B'=4, C'=free, D'=0, E'=free_1, F'=0, G'=0, H'=0, Q'=0, J'=0, [ free>=0 && free_1>=0 ], cost: 1
     71: f15 -> f15 : D'=2+D, F'=0, G'=0, H'=0, Q'=1, J'=1, [ 0>=D && 0>=C && B>=1 && Q==0 && E>=0 && 0>=0 && 0>=1+D && 0>=C && B>=1 && 0>=0 && 1>=1+E && 0>=0 ], cost: 5
     72: f15 -> f15 : B'=-1+B, D'=0, F'=0, G'=0, H'=0, Q'=1, J'=1, [ 0>=D && 0>=C && B>=1 && Q==0 && E>=0 && 0>=0 && 1+D>=1 && 0>=C && B>=1 && 0>=0 && 1>=1+E && 0>=0 ], cost: 5
     73: f15 -> f15 : D'=1+D, F'=0, G'=0, H'=0, Q'=1, J'=0, [ 0>=D && 0>=C && B>=1 && Q==0 && 0>=0 && 0>=1+E && 0>=0 ], cost: 3
     74: f15 -> f15 : B'=-1+B, D'=0, F'=free_2, G'=0, H'=0, Q'=1, J'=0, [ D>=1 && 0>=C && free_2>=0 && B>=1 && 1>=free_2 && Q==0 && 0>=0 && 0>=1+E && 0>=0 ], cost: 3
     75: f15 -> f15 : A'=2+A, B'=5+A, C'=0, D'=1, F'=free_4, G'=1, H'=0, Q'=1, J'=1, [ 0>=C && free_4>=0 && 1>=free_4 && 0>=B && free_3>=0 && Q==0 && E>=0 && 0>=0 && 0>=free_3 && 0>=4+A && 0>=free_4 && 1+E>=2+A && 5+A>=1 && 0>=0 && 1>=1+E && 0>=0 ], cost: 5

Eliminating 5 self-loops for location f15
  Self-Loop 71 has the metering function: -Q, resulting in the new transition 76.
  Self-Loop 72 has the metering function: -Q, resulting in the new transition 77.
  Self-Loop 73 has the metering function: -Q, resulting in the new transition 78.
  Self-Loop 74 has the metering function: -Q, resulting in the new transition 79.
  Self-Loop 75 has the metering function: meter, resulting in the new transition 80.
  Removing the self-loops: 71 72 73 74 75.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
      0: f0 -> f15 : A'=1, B'=4, C'=free, D'=0, E'=free_1, F'=0, G'=0, H'=0, Q'=0, J'=0, [ free>=0 && free_1>=0 ], cost: 1
     76: f15 -> [7] : D'=-2*Q+D, F'=0, G'=0, H'=0, Q'=1, J'=1, [ 0>=C && B>=1 && Q==0 && -E==0 && 0>=1+D ], cost: -5*Q
     77: f15 -> [7] : B'=B+Q, D'=0, F'=0, G'=0, H'=0, Q'=1, J'=1, [ D==0 && 0>=C && B>=1 && Q==0 && -E==0 ], cost: -5*Q
     78: f15 -> [7] : D'=-Q+D, F'=0, G'=0, H'=0, Q'=1, J'=0, [ 0>=D && 0>=C && B>=1 && Q==0 && 0>=1+E ], cost: -3*Q
     79: f15 -> [7] : B'=B+Q, D'=0, F'=free_2, G'=0, H'=0, Q'=1, J'=0, [ D>=1 && 0>=C && free_2>=0 && B>=1 && 1>=free_2 && Q==0 && 0>=1+E ], cost: -3*Q
     80: f15 -> [7] : A'=2*meter+A, B'=3+2*meter+A, C'=0, D'=1, F'=0, G'=1, H'=0, Q'=1, J'=1, [ 0>=C && 0>=B && Q==0 && -E==0 && 4+A==0 && 1+E>=2+A && 3*meter==-4-Q-A ], cost: 5*meter


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