never { /* !(GFcs2) */ T0_init : /* init */ if :: (1) -> goto T0_init :: (!cs2) -> goto accept_S2 fi; accept_S2 : /* 1 */ if :: (!cs2) -> goto accept_S2 fi; }