never {    /* !([]!(e1szEQ0 && (notifyclienteventa1e1 || notifyclienteventa2e1)))
 */
T0_init:
	if
	:: ((((e1szEQ0) && (notifyclienteventa1e1)) || ((e1szEQ0) && (notifyclienteventa2e1)))) -> goto accept_all
	:: (1) -> goto T0_init
	fi;
accept_all:
	skip
}