==> YES, main.fstb terminates. max_dim = 2 +-----------------------------------------------------------------------------+ | Ranking Function | +-----------------------------------------------------------------------------+ state start: 1 state a: 0 -1+(2*A) state ____start: 2 +-----------------------------------------------------------------------------+ | Worst Case Execution Time | +-----------------------------------------------------------------------------+ /--- / | -2*A__o' >= 0 | 1 >= 0 \ 1+1 / | -1+(2*A__o') >= 0 | 1 >= 0 \ (1+A__o')+1 \---