Trying to load file: main.koat Initial Control flow graph problem: Start location: evalgcdstart 0: evalgcdstart -> evalgcdentryin : [], cost: 1 1: evalgcdentryin -> evalgcdreturnin : [ 0>=A ], cost: 1 2: evalgcdentryin -> evalgcdreturnin : [ 0>=B ], cost: 1 3: evalgcdentryin -> evalgcdbb7in : A'=B, B'=A, [ A>=1 && B>=1 ], cost: 1 11: evalgcdreturnin -> evalgcdstop : [], cost: 1 6: evalgcdbb7in -> evalgcdreturnin : [ B==A ], cost: 1 4: evalgcdbb7in -> evalgcdbb4in : [ A>=1+B ], cost: 1 5: evalgcdbb7in -> evalgcdbb4in : [ B>=1+A ], cost: 1 7: evalgcdbb4in -> evalgcdbb5in : [ A>=1+B ], cost: 1 8: evalgcdbb4in -> evalgcdbb6in : [ B>=A ], cost: 1 9: evalgcdbb5in -> evalgcdbb7in : A'=-B+A, [], cost: 1 10: evalgcdbb6in -> evalgcdbb7in : B'=B-A, [], cost: 1 Simplified the transitions: Start location: evalgcdstart 0: evalgcdstart -> evalgcdentryin : [], cost: 1 3: evalgcdentryin -> evalgcdbb7in : A'=B, B'=A, [ A>=1 && B>=1 ], cost: 1 4: evalgcdbb7in -> evalgcdbb4in : [ A>=1+B ], cost: 1 5: evalgcdbb7in -> evalgcdbb4in : [ B>=1+A ], cost: 1 7: evalgcdbb4in -> evalgcdbb5in : [ A>=1+B ], cost: 1 8: evalgcdbb4in -> evalgcdbb6in : [ B>=A ], cost: 1 9: evalgcdbb5in -> evalgcdbb7in : A'=-B+A, [], cost: 1 10: evalgcdbb6in -> evalgcdbb7in : B'=B-A, [], cost: 1 Applied simple chaining: Start location: evalgcdstart 0: evalgcdstart -> evalgcdbb7in : A'=B, B'=A, [ A>=1 && B>=1 ], cost: 2 4: evalgcdbb7in -> evalgcdbb4in : [ A>=1+B ], cost: 1 5: evalgcdbb7in -> evalgcdbb4in : [ B>=1+A ], cost: 1 7: evalgcdbb4in -> evalgcdbb7in : A'=-B+A, [ A>=1+B ], cost: 2 8: evalgcdbb4in -> evalgcdbb7in : B'=B-A, [ B>=A ], cost: 2 Applied chaining over branches and pruning: Start location: evalgcdstart 0: evalgcdstart -> evalgcdbb7in : A'=B, B'=A, [ A>=1 && B>=1 ], cost: 2 12: evalgcdbb7in -> evalgcdbb7in : A'=-B+A, [ A>=1+B && A>=1+B ], cost: 3 13: evalgcdbb7in -> evalgcdbb7in : B'=B-A, [ B>=1+A && B>=A ], cost: 3 Eliminating 2 self-loops for location evalgcdbb7in Removing the self-loops: 12 13. Adding an epsilon transition (to model nonexecution of the loops): 16. Removed all Self-loops using metering functions (where possible): Start location: evalgcdstart 0: evalgcdstart -> evalgcdbb7in : A'=B, B'=A, [ A>=1 && B>=1 ], cost: 2 14: evalgcdbb7in -> [8] : A'=-B+A, [ A>=1+B ], cost: 3 15: evalgcdbb7in -> [8] : B'=B-A, [ B>=1+A ], cost: 3 16: evalgcdbb7in -> [8] : [], cost: 0 Applied chaining over branches and pruning: Start location: evalgcdstart Final control flow graph problem, now checking costs for infinitely many models: Start location: evalgcdstart 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),?)