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

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

state start:
2

state stop:
0

state lbl81:
1
(-2+B)+(-1*D)

state lbl91:
1
(-2+A)+(-1*B)

state start0:
3

state ____start0:
4


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

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

(((1+1)+((-2+(-1*C__o'))+A__o'))+1)+1

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

((1+1)+1)+1

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

(((1+1)+((-2+C__o')+(-1*A__o')))+1)+1

\---