#define r0  	req[0]==1
#define r1  	req[0]==1
#define r2  	req[0]==1
#define p0  	p==0
#define p1  	p==1
#define p2  	p==2
#define co	cabin@open


/* ! ( [] (r0 -> (!p0 U (p0 U (!p0 U (p0 U (p0&&co)))))) ) */


never {    /* ! ( [] (r0 -> (!p0 U (p0 U (!p0 U (p0 U (p0&&co)))))) ) */
T0_init:
	if
	:: (((! ((co)) && (r0)) || (! ((p0)) && (r0)))) -> goto accept_S2
	:: (! ((co)) && (p0) && (r0)) -> goto accept_S812
	:: (1) -> goto T0_init
	fi;
accept_S2:
	if
	:: (((! ((co))) || (! ((p0))))) -> goto T0_S2
	:: (! ((co)) && (p0)) -> goto T0_S812
	fi;
accept_S812:
	if
	:: (((! ((co))) || (! ((p0))))) -> goto T0_S812
	:: (! ((p0))) -> goto T0_S890
	fi;
accept_S890:
	if
	:: (((! ((co))) || (! ((p0))))) -> goto T0_S890
	:: (! ((co)) && (p0)) -> goto accept_S912
	fi;
accept_S912:
	if
	:: (((! ((co))) || (! ((p0))))) -> goto accept_S912
	:: (! ((p0))) -> goto accept_all
	fi;
T0_S2:
	if
	:: (((! ((co))) || (! ((p0))))) -> goto accept_S2
	:: (! ((co)) && (p0)) -> goto accept_S812
	fi;
T0_S812:
	if
	:: (((! ((co))) || (! ((p0))))) -> goto accept_S812
	:: (! ((p0))) -> goto accept_S890
	fi;
T0_S890:
	if
	:: (((! ((co))) || (! ((p0))))) -> goto accept_S890
	:: (! ((co)) && (p0)) -> goto accept_S912
	fi;
accept_all:
	skip
}