==> YES, main.fstb terminates. max_dim = 1 +-----------------------------------------------------------------------------+ | Ranking Function | +-----------------------------------------------------------------------------+ state f0: 34 state f9: 33+(-2*A) state f10: 32+(-2*A) state f16: 11+(-1*A) state f28: 0 state ____f0: 35 +-----------------------------------------------------------------------------+ | Worst Case Execution Time | +-----------------------------------------------------------------------------+ /--- / | 1 >= 0 \ ((((1+11)+11)+11)+1)+1 \---