==> YES, main.fstb terminates. max_dim = 2 +-----------------------------------------------------------------------------+ | Ranking Function | +-----------------------------------------------------------------------------+ state f3: 1 state f1: 0 A state ____f3: 2 +-----------------------------------------------------------------------------+ | Worst Case Execution Time | +-----------------------------------------------------------------------------+ /--- / | A__o' >= 0 | 1 >= 0 \ (1+(1+A__o'))+1 \---