#define N 7	
#define L 2

mtype {patfrnd,frndpat,patpharma,pharmapat,pharmafrnd,frndpharma};

mtype  { one};

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

bool pharma_frnd,asa,obj_disclosure,pr_jd,phil_is_hcp,fred_is_friend,fred_is_identified,msg_sent; 


proctype pharmacist (chan patin, patout,friendin,friendout)
{	
	byte mesg;
                   
   end:	do

	:: patin?one(mesg) ->
		printf("pharmacist gets mesg frm patient \n");
 	::friendin?one(mesg) ->
		printf("pharmacist gets mesg frm friend \n");
        :: patout!one(mesg) ->
         	printf("pharmacist sends mesg  to patient \n");  
        ::friendout!one(mesg) ->
                printf("pharmacist sends mesg to friend \n");
        ::break

	od
}


proctype patient (chan pharmain,pharmaout,friendin,friendout)
{	
	byte mesg;
	
	end: do

            :: friendin?one(mesg) ->
		    printf("patient  gets mesg frm friend \n");
            :: pharmain?one(mesg) ->
		    printf("patient  gets mesg frm pharmacist\n");
	    :: pharmaout!one(mesg) ->
            	   printf(" patient  sends mesg to pharmacist \n");
                   if
             		:: skip -> fred_is_identified=1; 
	                :: skip -> fred_is_identified=0;
        	        :: skip -> atomic{ obj_disclosure=1; pharma_frnd=0;}
                	:: skip -> obj_disclosure=0;
                   fi
           :: friendout!one(mesg) ->
         	   printf(" patient  sends mesg to friend \n"); 
           :: d_step{ asa =0; pr_jd=1;}
           :: d_step{asa =1; pr_jd=0; }
       	   :: break
    
	od
}



proctype friend (chan patin, patout, pharmain,pharmaout)
{	
	byte mesg;

	end: do

	     :: patin?one(mesg) ->
		     printf("friend gets mesg frm patient \n");
             ::pharmain?one(mesg) ->
		     pharma_frnd=1;
		     printf("friends gets mesg frm pharmacist \n");                                
             :: patout!one(mesg) ->
              	     printf("friend sends mesg  to patient \n");              
 	     ::pharmaout!one(mesg) ->
		     printf("friend sends mesg to pharmacist \n");                      
	     ::break
	od
}



init {
	atomic{
	 	asa=1;                         /*patient is available-sane and authorised */
		phil_is_hcp=1; 
		fred_is_friend=1;              /* fred is patients' friend */
		fred_is_identified=0;          /* patient has identified fred */   
		pharma_frnd=0;                 /* pharacist disclosed phi to fred */
		obj_disclosure=0;              /* patient objects to disclosure of his phi */ 
		pr_jd=0;                       /* hcp uses his professional judgement */
		msg_sent=1;                    /* some message communication took place */

               	run friend(q[patfrnd],q[frndpat],q[pharmafrnd],q[frndpharma]);  
                run patient (q[pharmapat],q[patpharma],q[frndpat],q[patfrnd]); 
		run pharmacist(q[patpharma],q[pharmapat],q[frndpharma],q[pharmafrnd])

		}
}


/************************** LTL property ********************************************************


#define pharma_frnd	pharma_frnd
#define phil_is_hcp	phil_is_hcp
#define fred_is_friend	fred_is_friend
#define fred_is_identified	fred_is_identified
#define asa	asa
#define pr_jd	pr_jd
#define obj_disclosure	obj_disclosure

/* []HIPAA -> []Desired */


[]((( !pharma_frnd || (phil_is_hcp && pharma_frnd && fred_is_friend) || (phil_is_hcp && pharma_frnd && fred_is_identified ) || ( phil_is_hcp && ! asa && pr_jd && pharma_frnd ) )&& ((phil_is_hcp && asa && obj_disclosure) -> [](!pharma_frnd) ))  -> (pharma_frnd -> fred_is_identified) )

*********************************************************************/