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

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

state f1:
0
(2*A)+(2*B)
B

state f2:
0
(1+(2*A))+(2*B)
A

state f999:
1

state ____f999:
2


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

/---
/
| A__o' = 0
| -1+B__o' >= 0
| 1 >= 0
\

(((((3/2)*B__o')+((1/2)*(B__o'*B__o')))+(((1/2)*B__o')+((1/2)*(B__o'*B__o'))))+1)+1

/
| -1+A__o' >= 0
| 1 >= 0
\

1+1

/
| -1*B__o' >= 0
| 1 >= 0
\

1+1

\---