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