#define N 3	
#define L 2

#define T 0
#define P 1
#define O 2

mtype {hcp1hcp2,hcp2hcp1};

mtype  { one};

chan q[N] = [L] of { mtype, int};

int msg12_type=4;
bool p2_is_covered=0,p2_is_hcp=1,p2_in_relation=0;  


proctype hcp (int id; chan hcpin,hcpout)
{	
	int mesg;

	end:	do
	
       		::skip->
         		 if
		            :: mesg=T;
		            :: mesg=P;
		            :: mesg=O;
	                 fi;
	                 hcpout!one(mesg);
		         if
         		    :: (id==0 )-> msg12_type=mesg;
 		            ::else  skip;
		         fi;
	                 printf("hcp %d sends mesg to another hcp type of mesg =%d\n",id, mesg); 
	                 hcpin?one(mesg) ->              
	        	 printf("hcp gets mesg %d frm another hcp \n",mesg);                      
	        ::break

	       od
}




init {
	atomic{
		if
			:: skip ->  p2_is_covered=1;
			:: skip ->  p2_is_covered=0;
		fi;
		if
			:: skip ->  p2_in_relation=1;
			:: skip ->  p2_in_relation=0;
		fi;

		run hcp(0,q[hcp2hcp1],q[hcp1hcp2]);
		run hcp(1, q[hcp1hcp2],q[hcp2hcp1])
	}
	
}




/*********************LTL formula **************************************************************************
/*[]hipaa -> []desired */

[] ( (msg_init || msgT || msgTPO || (msgP && (p2_is_hcp ||p2_is_covered)) || (p2_in_relation && msgTPO ) || (msgO  && p2_is_covered))   -> [] ( (msgTPO -> p2_is_covered)  )


#define msgT (msg12_type ==0) 
#define msgTPO (msg12_type==0 || msg12_type==1 || msg12_type==2) 
#define msgP  (msg12_type==1) 
#define msgO (msg12_type==2) 
#define p2_is_hcp p2_is_hcp
#define p2_in_relation p2_in_relation
#define p2_is_covered p2_is_covered
#define p2_is_hcp p2_is_hcp
#define msg_init (msg12_type==4)




*/