#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 {
newinit:
	if
        :: (1) -> goto newinit
	:: ((! (co) && ! (p0) && (r0)) || ((co) && ! (p0) && (r0))) -> goto q2
	:: ((! (co) && (p0) && (r0))) -> goto q3
	fi;


accept_q1:
q1:
	if
	:: ((! (co) && ! (p0) && (r0)) || ((co) && ! (p0) && (r0))) -> goto q2
	:: ((! (co) && (p0) && (r0))) -> goto q3
	fi;
accept_q2:
q2:
	if
	:: ((! (co) && ! (p0) && ! (r0)) || (! (co) && ! (p0) && (r0)) || ((co) && ! (p0) && ! (r0)) || ((co) && ! (p0) && (r0))) -> goto q2
	:: ((! (co) && (p0) && ! (r0)) || (! (co) && (p0) && (r0))) -> goto q3
	fi;
accept_q3:
q3:
	if
	:: ((! (co) && (p0) && ! (r0)) || (! (co) && (p0) && (r0))) -> goto q3
	:: ((! (co) && ! (p0) && ! (r0)) || (! (co) && ! (p0) && (r0)) || ((co) && ! (p0) && ! (r0)) || ((co) && ! (p0) && (r0))) -> goto q4
	fi;
accept_q4:
q4:
	if
	:: ((! (co) && ! (p0) && ! (r0)) || (! (co) && ! (p0) && (r0)) || ((co) && ! (p0) && ! (r0)) || ((co) && ! (p0) && (r0))) -> goto q4
	:: ((! (co) && (p0) && ! (r0)) || (! (co) && (p0) && (r0))) -> goto q5
	fi;
accept_q5:
q5:
	if
	:: ((! (co) && (p0) && ! (r0)) || (! (co) && (p0) && (r0))) -> goto q5
	:: ((! (co) && ! (p0) && ! (r0)) || (! (co) && ! (p0) && (r0)) || ((co) && ! (p0) && ! (r0)) || ((co) && ! (p0) && (r0))) -> goto q6
	fi;
accept_q6:
q6:
	if
	:: ((! (co) && ! (p0) && ! (r0)) || (! (co) && ! (p0) && (r0)) || (! (co) && (p0) && ! (r0)) || (! (co) && (p0) && (r0)) || ((co) && ! (p0) && ! (r0)) || ((co) && ! (p0) && (r0)) || ((co) && (p0) && ! (r0)) || ((co) && (p0) && (r0))) -> goto q6
	fi;
}
/* type, nba, -nba, wdba, min:  safety, 6, 6, 8, 7 */