never solYes { /* !(((((ms[2].x[25]==0)) && ((ms[2].x[1]==0))) || (! (isPsystemStep))) U ((((ms[2].x[1]==1)) && ((ms[2].x[25]==0))) && (isPsystemStep))) */ accept_init: T0_init: if :: (! (((((ms[2].x[1]==1)) && ((ms[2].x[25]==0))) && (isPsystemStep)))) -> goto T0_init :: (! (((((ms[2].x[1]==1)) && ((ms[2].x[25]==0))) && (isPsystemStep))) && ! (((((ms[2].x[25]==0)) && ((ms[2].x[1]==0))) || (! (isPsystemStep))))) -> goto accept_all fi; accept_all: skip }