MODULE main
VAR
	state : {s0,s1,s2};
	p : boolean;
	q : boolean;
ASSIGN
	init(state) := s0;
	init(p) := TRUE;
	init(q) := FALSE;
	next(state) := case
		state=s0 : s2;
		state=s1 : {s0,s1};
		state=s2 : {s0,s1};
	esac;
	next(p) := case
		next(state)=s0 : TRUE;
		next(state)=s1 : FALSE;
		next(state)=s2 : FALSE;
	esac;
	next(q) := case
		next(state)=s0 : FALSE;
		next(state)=s1 : TRUE;
		next(state)=s2 : FALSE;
	esac;
	SPEC E [p U q]