State_s2_ctl.smv

MODULE main
VAR
	p:   boolean;
	q:   boolean;
	r:   boolean;
	state:  {s0,s1,s2};
ASSIGN
	  init(state)    := s2;
	  next(state)  := case
		         p & q  :   {s1,s2};
		         q & r   :   {s0,s2};
		         r           :   {s2};
		         TRUE : state;
		       esac;	

 	 r:=case
		(state=s0) :FALSE;
		(state=s1) :TRUE;
		(state=s2) :TRUE;
	     esac;	

	 q:=case
		(state=s0) :TRUE;
		(state=s1) :TRUE;
		(state=s2) :FALSE;
	        esac;

	  p:=case
		(state=s0)  : TRUE;
	 	(state=s1)  : FALSE;
	 	(state=s2)  : FALSE;
	        esac;

CTLSPEC
	(p&q);
CTLSPEC	
	!(r);
CTLSPEC
	TRUE;
CTLSPEC
	EX(q&r);
CTLSPEC
	!(AX(q&r));
CTLSPEC
	!(EF(p&r));
CTLSPEC
	EG(r);
CTLSPEC
	AF(r);
CTLSPEC
	E[(p&q)U(r)];
CTLSPEC
	A[(p)U(r)];
CTLSPEC
	AG((p|q|r) -> (EF(EG(r))));