#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{
T0_init:
	if
	:: true -> goto T1
	:: (r0) && (!(p0)) -> goto accept_T2
	:: ((r0) && (p0)) && (!(co)) -> goto accept_T3
	fi;
T1:
	if
	:: true -> goto T1
	:: (r0) && (!(p0)) -> goto accept_T2
	:: ((r0) && (p0)) && (!(co)) -> goto accept_T3
	fi;
accept_T2:
	if
	:: !(p0) -> goto accept_T2
	:: (p0) && (!(co)) -> goto accept_T3
	fi;
accept_T3:
	if
	:: (p0) && (!(co)) -> goto accept_T3
	:: !(p0) -> goto accept_T4
	fi;
accept_T4:
	if
	:: !(p0) -> goto accept_T4
	:: (p0) && (!(co)) -> goto accept_T5
	fi;
accept_T5:
	if
	:: (p0) && (!(co)) -> goto accept_T5
	:: !(p0) -> goto accept_T6
	fi;
accept_T6:
	skip;
}