==> YES, main.fstb terminates. max_dim = 2 +-----------------------------------------------------------------------------+ | Ranking Function | +-----------------------------------------------------------------------------+ state f5: 1 A state f1: 0 state f300: 2 state ____f300: 3 +-----------------------------------------------------------------------------+ | Worst Case Execution Time | +-----------------------------------------------------------------------------+ /--- / | -1*A__o' >= 0 | 1 >= 0 \ (1+1)+1 / | -1+A__o' >= 0 | 1 >= 0 \ ((A__o'+1)+1)+1 \---