#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 { /* ! ( [] (r0 -> (!p0 U (p0 U (!p0 U (p0 U (p0&&co)))))) ) */
T0_init:
	if
	:: (1) -> goto T0_init
	:: (!p0 && r0) || (!co && r0) -> goto accept_S3
	:: (!co && p0 && r0) -> goto accept_S4
	fi;
accept_S3:
	if
	:: (!co) || (!p0) -> goto accept_S3
	:: (!co && p0) -> goto accept_S4
	fi;
accept_S4:
	if
	:: (!co) -> goto accept_S4
	:: (!p0) -> goto accept_S7
	fi;
accept_S7:
	if
	:: (!p0) || (!co) -> goto accept_S7
	:: (!co && p0) -> goto accept_S8
	fi;
accept_S8:
	if
	:: (!co) -> goto accept_S8
	:: (!p0) -> goto accept_all
	fi;
accept_all:
	skip
}