never p3 {    /* !([] (((! (((ms[1].x[12]==1)) && ((ms[1].x[4]==1)))) || (X ((! (isPsystemStep)) U (((ms[2].x[25]==1)) && (isPsystemStep))))) || (! (isPsystemStep)))) */
T0_init:
	if
	:: (! ((! (((ms[1].x[12]==1)) && ((ms[1].x[4]==1))))) && ! ((! (isPsystemStep)))) -> goto accept_S3
	:: (1) -> goto T0_init
	fi;
accept_S3:
	if
	:: (! ((((ms[2].x[25]==1)) && (isPsystemStep)))) -> goto accept_S3
	:: (! ((! (isPsystemStep))) && ! ((((ms[2].x[25]==1)) && (isPsystemStep)))) -> goto accept_all
	fi;
accept_all:
	skip
}