==> YES, main.fstb terminates. max_dim = 2

+-----------------------------------------------------------------------------+
|                             Ranking Function                                |
+-----------------------------------------------------------------------------+

state start:
1

state m1:
0
(1+B)+(-1*F)

state ____start:
2


+-----------------------------------------------------------------------------+
|                         Worst Case Execution Time                           |
+-----------------------------------------------------------------------------+

/---
/
| (-1+A__o')+(-1*F__o') >= 0
| 1 >= 0
\

1+1

/
| A__o'+(-1*F__o') = 0
| (-1+C__o')+(-1*E__o') = 0
| ((2+(-1*B__o'))+(2*E__o'))+(-1*F__o') >= 0
| (B__o'+(-2*E__o'))+F__o' >= 0
| (-1+B__o')+(-1*F__o') >= 0
| F__o' >= 0
| D__o' >= 0
\

(1+((2+(-1*F__o'))+B__o'))+1

/
| ((-1+(-1*B__o'))+(2*E__o'))+(-1*F__o') >= 0
| 1 >= 0
\

1+1

/
| (-1+(-1*A__o'))+F__o' >= 0
| 1 >= 0
\

1+1

/
| (-1*C__o')+E__o' >= 0
| 1 >= 0
\

1+1

/
| (-2+C__o')+(-1*E__o') >= 0
| 1 >= 0
\

1+1

/
| ((-3+B__o')+(-2*E__o'))+F__o' >= 0
| 1 >= 0
\

1+1

/
| (-1*B__o')+F__o' >= 0
| 1 >= 0
\

1+1

\---