WARNING: state f13 is unreachable WARNING: state f12 is unreachable WARNING: state f10 is unreachable ==> main.fstb MAY NOT TERMINATE. Cycle with transition(s): t8 [A = 0, B = 1, C = 0, D = 0, E = 2, F = 0, G = 0, H = 0, I = 0, J = 0, K = 0, L = 0, M = 0, N = 0, O = 0, P = 0, A__o = 0, B__o = 0, C__o = 0, D__o = 0, E__o = 2, F__o = 0, G__o = 0, H__o = 0, I__o = 0, J__o = 0, K__o = 0, L__o = 0, M__o = 0, N__o = 0, O__o = 0, P__o = 0] is likely to be an infinite loop.