WARNING: state f15 is unreachable
WARNING: state f17 is unreachable

==> main.fstb MAY NOT TERMINATE. 

Cycle with transition(s):

t1 [A = 1, B = 1, C = 1, A__o = 0, B__o = 0, C__o = 0]

is likely to be an infinite loop.