#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

never{ 
T5_init:
	if
	:: ((! p0) && r0) || ((! co) && r0) -> goto accept_T2
	:: (p0 && (! co) && r0) -> goto accept_T1
	:: (1) -> goto T5_init
	fi;
accept_T2:
	if
	:: ((! p0)) || ((! co)) -> goto accept_T2
	:: ((! co) && p0) -> goto accept_T1
	fi;
accept_T1:
	if
	:: ((! co)) -> goto accept_T1
	:: ((! p0)) -> goto accept_T0
	fi;
accept_T0:
	if
	:: ((! co) && p0) -> goto accept_T3
	:: ((! p0)) || ((! co)) -> goto accept_T0
	fi;
accept_T3:
	if
	:: ((! p0)) -> goto accept_all
	:: ((! co)) -> goto accept_T3
	fi;
accept_all:
	skip
}