==> YES, main.fstb terminates. max_dim = 1 +-----------------------------------------------------------------------------+ | Ranking Function | +-----------------------------------------------------------------------------+ state f0: 38 state f5: 0 state f7: 37+(-1*B) state ____f0: 39 +-----------------------------------------------------------------------------+ | Worst Case Execution Time | +-----------------------------------------------------------------------------+ /--- / | 127+(-1*A__o') >= 0 | 1 >= 0 \ ((1+1)+37)+1 / | -128+A__o' >= 0 | 1 >= 0 \ (1+1)+1 \---