#define N 5	
#define L 1

#define consent 0
#define deny 1
#define auth  2


mtype {pathcp,hcppat,hcpp2,p2hcp};

mtype  { one};

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

bool req_consent=0, tpo=0,auth_req=1 ,send_consent=0; 


proctype  business_associate(chan hcpin,hcpout)
{
    	byte mesg;
    
	end: do
             	:: hcpin?one(mesg) ->
                	printf("p2 gets mesg frm hcp\n");
			tpo=1;
                :: hcpout!one(mesg) -> 
     	                printf("p2 sends mesg to hcp\n");
                :: break
             od
}

proctype patient (chan hcpin,hcpout)
{	
	byte mesg;
	
	end: do
       		:: if 
                      :: mesg=consent  ; 
                      :: mesg=deny;
                      :: mesg = auth; 
                   fi ;
	           hcpout!one(mesg) ;
	           printf("patient  sends deny/consent/auth mesg %d to hcp\n",mesg);

                :: hcpin?one(mesg) ->
		   	printf("patient  gets request mesg frm hcp \n");
	        :: auth_req=1;
        	:: break
	    od
}



proctype hcp (chan patin, patout,p2in,p2out)
{	
	byte mesg;

 	end: do
	
		:: patin?one(mesg) ->
			printf("hcp gets mesg  %d frm patient \n",mesg);
			if
		 		::(mesg==consent)  -> req_consent=0; send_consent=1;
				:: (mesg==deny) -> req_consent=0; send_consent=0;
				:: (mesg==auth)-> auth_req=0;
			fi;
         	::patout!one(mesg) ->
			req_consent=1;	
			printf("hcp sends request for consent  to patient \n");                
               :: p2in?one(mesg) ->
	  		printf("hcp gets mesg frm p2\n");
	       :: p2out!one(mesg) ->
  			printf("hcp sends mesg to p2\n");                                                       
	       ::break
	    od
}



init {
	atomic{	
		run patient (q[hcppat],q[pathcp]);
		run business_associate(q[hcpp2],q[p2hcp]);
		run hcp(q[pathcp],q[hcppat],q[p2hcp],q[hcpp2])
	}	
}







/**************************************LTL*******************************************

[] ( (((req_consent || !req_consent) && tpo) && (auth_req -> !tpo ) )  -> (!send_consent -> ((!tpo U send_consent) || [] !tpo )) )



#define req_consent	req_consent
#define tpo tpo
#define auth_req	auth_req
#define send_consent	send_consent




*/