MODULE main
VAR
	state : { s0,s1,s2,s3 };
ASSIGN
	init(state) := s1;
	next(state) :=
		case
			state = s0 : { s0, s1 };
			state = s1 : { s2 };
			state = s2 : { s0 };
			state = s3 : { s3 };
		esac;
		
DEFINE
	p := state in { s0, s2 };
	q := state in { s1 };
	r := state in { s2 };
	t := state in { s3 };
	
SPEC
	--A[p U q]
	--test 2008-10-20
	--remove -- before the check and set the initial state
	--EX EX q --s0 true
	--EF AX t --s0 true
	--AG EF q --s1 false
	--A[(p | r) U q] --s2 false
	--EG EX EX t --s2 true
	
	--test 2008-12-10
	--remove -- before the check and set the initial state
	--EG (q | p) --s0 true
	--EF (r & AX t) --s0 false
	--E [ (p | !t) U (!q & !r) ] --s1 true
	--A[ (p | q | r) U t ] --s2 false
	--EG (p | !t) --s2 true
	
	--test 2009-05-05
	--remove -- before the check and set the initial state
	--EF (r & EX p) --s0 true
	AG EF p --s1 false
	--EF (!p & A[q U p]) --s2 true
	--AX AX (t & !r) --s2 false
	--EG A[t U r] --s3  false