==> YES, main.fstb terminates. max_dim = 1 +-----------------------------------------------------------------------------+ | Ranking Function | +-----------------------------------------------------------------------------+ state f4: 9+(-2*A) state f5: 8+(-2*A) state f0: 10 state f11: 1 state f14: 0 state ____f0: 11 +-----------------------------------------------------------------------------+ | Worst Case Execution Time | +-----------------------------------------------------------------------------+ /--- / | 1 >= 0 \ ((((4+4)+1)+1)+1)+1 \---