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