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