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