WARNING: state f24 is unreachable WARNING: state f27 is unreachable ==> main.fstb MAY NOT TERMINATE. Cycle with transition(s): t0 [A = 0, B = 0, C = 0, D = 0, E = 0, A__o = 0, B__o = 0, C__o = 0, D__o = 0, E__o = 0] -> t4 [A = 0, B = 0, C = 0, D = 0, E = 0, A__o = 0, B__o = 0, C__o = 0, D__o = 0, E__o = 0] is likely to be an infinite loop.