==> YES, main.fstb terminates. max_dim = 1 +-----------------------------------------------------------------------------+ | Ranking Function | +-----------------------------------------------------------------------------+ state f0: 21 state f5: (20+(-1*A))+B__o state f12: 0 state ____f0: 22 +-----------------------------------------------------------------------------+ | Worst Case Execution Time | +-----------------------------------------------------------------------------+ /--- / | -1+B__o' >= 0 | 1 >= 0 \ ((1+20)+1)+1 / | -1*B__o' >= 0 | 1 >= 0 \ (1+1)+1 \---