==> YES, main.fstb terminates. max_dim = 2 +-----------------------------------------------------------------------------+ | Ranking Function | +-----------------------------------------------------------------------------+ state start: 2 state stop: 0 state lbl32: 1 -1+D state start0: 3 state ____start0: 4 +-----------------------------------------------------------------------------+ | Worst Case Execution Time | +-----------------------------------------------------------------------------+ /--- / | -2+A__o' >= 0 | 1 >= 0 \ (((1+1)+(-1+A__o'))+1)+1 / | 1+(-1*A__o') >= 0 | 1 >= 0 \ ((1+1)+1)+1 \---