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