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