Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: f1
      1: f0 -> f0 : A'=1+3*A, C'=free_2, D'=free_1, E'=free_3, [ A>=1 && A>=1+2*free_3 && 3*A>=3*free_2 && 3*free_2>=3*A && free_2>=1+2*free_3 && free_2>=1 ], cost: 1
      2: f0 -> f0 : A'=1+3*A, C'=free_5, D'=free_4, E'=free_6, [ A>=1 && A>=1+2*free_6 && 3*A>=3*free_5 && 3*free_5>=3*A && 2*free_6>=1+free_5 && free_5>=1 ], cost: 1
      3: f0 -> f0 : A'=1+3*A, C'=free_8, D'=free_7, E'=free_9, [ A>=1 && 2*free_9>=1+A && 3*A>=3*free_8 && 3*free_8>=3*A && free_8>=1+2*free_9 && free_8>=1 ], cost: 1
      4: f0 -> f0 : A'=1+3*A, C'=free_11, D'=free_10, E'=free_12, [ A>=1 && 2*free_12>=1+A && 3*A>=3*free_11 && 3*free_11>=3*A && 2*free_12>=1+free_11 && free_11>=1 ], cost: 1
      5: f0 -> f0 : A'=free_14, D'=free_13, E'=free_14, [ 2*free_14>=1 && free_15>=1 && A==2*free_14 ], cost: 1
      0: f0 -> f2 : B'=free, [ 0>=A ], cost: 1
      6: f1 -> f0 : [], cost: 1


Simplified the transitions:
  Start location: f1
      1: f0 -> f0 : A'=1+3*A, C'=free_2, D'=free_1, E'=free_3, [ A>=1 && A>=1+2*free_3 && 3*free_2-3*A==0 && free_2>=1+2*free_3 && free_2>=1 ], cost: 1
      2: f0 -> f0 : A'=1+3*A, C'=free_5, D'=free_4, E'=free_6, [ A>=1 && A>=1+2*free_6 && 3*free_5-3*A==0 && 2*free_6>=1+free_5 && free_5>=1 ], cost: 1
      3: f0 -> f0 : A'=1+3*A, C'=free_8, D'=free_7, E'=free_9, [ A>=1 && 2*free_9>=1+A && 3*free_8-3*A==0 && free_8>=1+2*free_9 && free_8>=1 ], cost: 1
      4: f0 -> f0 : A'=1+3*A, C'=free_11, D'=free_10, E'=free_12, [ A>=1 && 2*free_12>=1+A && 3*free_11-3*A==0 && 2*free_12>=1+free_11 && free_11>=1 ], cost: 1
      5: f0 -> f0 : A'=free_14, D'=free_13, E'=free_14, [ 2*free_14>=1 && A==2*free_14 ], cost: 1
      6: f1 -> f0 : [], cost: 1

Eliminating 5 self-loops for location f0
  Self-Loop 1 has the metering function: meter, resulting in the new transition 7.
  Self-Loop 2 has the metering function: meter_1, resulting in the new transition 8.
  Self-Loop 3 has the metering function: meter_2, resulting in the new transition 9.
  Self-Loop 4 has the metering function: meter_3, resulting in the new transition 10.
  Removing the self-loops: 1 2 3 4 5.
Adding an epsilon transition (to model nonexecution of the loops): 12.

Removed all Self-loops using metering functions (where possible):
  Start location: f1
      7: f0 -> [3] : A'=-1/2+3^meter*A+1/2*3^meter, C'=1, D'=free_1, E'=free_3, [ A>=1 && A>=1+2*free_3 && 3-3*A==0 && 1>=1+2*free_3 && 1>=1 && 3*meter==1-A ], cost: meter
      8: f0 -> [3] : A'=-1/2+1/2*3^meter_1+3^meter_1*A, C'=1, D'=free_4, E'=free_6, [ A>=1 && A>=1+2*free_6 && 3-3*A==0 && 2*free_6>=2 && 1>=1 && 3*meter_1==-A ], cost: meter_1
      9: f0 -> [3] : A'=-1/2+1/2*3^meter_2+3^meter_2*A, C'=1, D'=free_7, E'=free_9, [ A>=1 && 2*free_9>=1+A && 3-3*A==0 && 1>=1+2*free_9 && 1>=1 && 3*meter_2==-A ], cost: meter_2
     10: f0 -> [3] : A'=-1/2+3^meter_3*A+1/2*3^meter_3, C'=1, D'=free_10, E'=free_12, [ A>=1 && 2*free_12>=1+A && 3-3*A==0 && 2*free_12>=2 && 1>=1 && 3*meter_3==1-A ], cost: meter_3
     11: f0 -> [3] : A'=free_14, D'=free_13, E'=free_14, [ 2*free_14>=1 && A==2*free_14 ], cost: 1
     12: f0 -> [3] : [], cost: 0
      6: f1 -> f0 : [], cost: 1


Applied chaining over branches and pruning:
  Start location: f1
     13: f1 -> [3] : A'=-1/2+3^meter*A+1/2*3^meter, C'=1, D'=free_1, E'=free_3, [ A>=1 && A>=1+2*free_3 && 3-3*A==0 && 1>=1+2*free_3 && 1>=1 && 3*meter==1-A ], cost: 1+meter
     14: f1 -> [3] : A'=-1/2+3^meter_3*A+1/2*3^meter_3, C'=1, D'=free_10, E'=free_12, [ A>=1 && 2*free_12>=1+A && 3-3*A==0 && 2*free_12>=2 && 1>=1 && 3*meter_3==1-A ], cost: 1+meter_3


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: f1
     13: f1 -> [3] : A'=-1/2+3^meter*A+1/2*3^meter, C'=1, D'=free_1, E'=free_3, [ A>=1 && A>=1+2*free_3 && 3-3*A==0 && 1>=1+2*free_3 && 1>=1 && 3*meter==1-A ], cost: 1+meter
     14: f1 -> [3] : A'=-1/2+3^meter_3*A+1/2*3^meter_3, C'=1, D'=free_10, E'=free_12, [ A>=1 && 2*free_12>=1+A && 3-3*A==0 && 2*free_12>=2 && 1>=1 && 3*meter_3==1-A ], cost: 1+meter_3


Computing complexity for remaining 2 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),?)