==> YES, main.fstb terminates. max_dim = 1 +-----------------------------------------------------------------------------+ | Ranking Function | +-----------------------------------------------------------------------------+ state start: 41 state lbl91: 41+(-1*E) state lbl111: 42+(-1*E) state stop: 0 state start0: 42 state ____start0: 43 +-----------------------------------------------------------------------------+ | Worst Case Execution Time | +-----------------------------------------------------------------------------+ /--- / | -1+B__o' >= 0 | 1 >= 0 \ (((1+40)+1)+1)+1 / | B__o' = 0 | 1 >= 0 \ ((((1+40)+40)+1)+1)+1 \---