never p5 {    /* !([] (((! (invariantPrecond)) || (X ((! (isPsystemStep)) U ((invariantPostcond) && (isPsystemStep))))) || (! (isPsystemStep)))) */
T0_init:
	if
	:: (! ((! (invariantPrecond))) && ! ((! (isPsystemStep)))) -> goto accept_S3
	:: (1) -> goto T0_init
	fi;
accept_S3:
	if
	:: (! (((invariantPostcond) && (isPsystemStep)))) -> goto accept_S3
	:: (! ((! (isPsystemStep))) && ! (((invariantPostcond) && (isPsystemStep)))) -> goto accept_all
	fi;
accept_all:
	skip
}