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