//-------- DECLARE VARIBLES ----------//
var	b_Patient : int ,
	b_PrimaryDoctor : int ,
	b_target : int ,
	b_SUPER_ROLE : int ,
	d_Patient : int ,
	d_PrimaryDoctor : int ,
	d_target : int ,
	d_SUPER_ROLE : int ,
	n_PrimaryDoctor_Patient : int ,
	n_SUPER_ROLE : int ,
	n_0Patient : int ,
	n_0PrimaryDoctor : int ,
	n_target : int ;

//-------------- BEGIN Program --------------------//
begin
	//-------------- Init VARS ------------------------//
	b_Patient = 0;
	b_PrimaryDoctor = 0;
	b_target = 0;
	b_SUPER_ROLE = 0;
	d_Patient = 0;
	d_PrimaryDoctor = 0;
	d_target = 0;
	d_SUPER_ROLE = 0;
	n_PrimaryDoctor_Patient = 0;
	n_SUPER_ROLE = 0;
	n_0Patient = 0;
	n_0PrimaryDoctor = 0;
	n_target = 0;
	// Initialize track variables in the system
	n_SUPER_ROLE = n_SUPER_ROLE + 1;
	n_0Patient = n_0Patient + 5;
	n_0PrimaryDoctor = n_0PrimaryDoctor + 5;

	while ( true )  do 

		//----- Non-deterministic assignment ------//
		b_Patient = random; assume b_Patient >= 0 and b_Patient <= 1;
		b_PrimaryDoctor = random; assume b_PrimaryDoctor >= 0 and b_PrimaryDoctor <= 1;
		b_target = random; assume b_target >= 0 and b_target <= 1;
		b_SUPER_ROLE = random; assume b_SUPER_ROLE >= 0 and b_SUPER_ROLE <= 1;

		d_Patient = random; assume d_Patient >= 0 and d_Patient <= 1;
		d_PrimaryDoctor = random; assume d_PrimaryDoctor >= 0 and d_PrimaryDoctor <= 1;
		d_target = random; assume d_target >= 0 and d_target <= 1;
		d_SUPER_ROLE = random; assume d_SUPER_ROLE >= 0 and d_SUPER_ROLE <= 1;

		//-------------- Simulation -------------------//
		//------------------ CAN_ASSIGN RULE NUMBER 0 -----------------
		// <SUPER_ROLE,PrimaryDoctor&Patient,target>
		//------------------------------------------------------------------
		if(brandom and d_SUPER_ROLE==1 and n_SUPER_ROLE>0 and b_PrimaryDoctor==1 and b_Patient==1 and n_PrimaryDoctor_Patient>0) then
			if(true) then
				n_target = n_target+1;
			endif;
		endif;

		//------------------ CAN_ASSIGN RULE NUMBER 1 -----------------
		// <SUPER_ROLE,-Patient,PrimaryDoctor>
		//------------------------------------------------------------------
		if(brandom and d_SUPER_ROLE==1 and n_SUPER_ROLE>0 and b_Patient==0 and n_0Patient>0) then
			if(b_Patient==1) then
				n_PrimaryDoctor_Patient = n_PrimaryDoctor_Patient+1;
			endif;
			if(b_PrimaryDoctor==0 and n_0PrimaryDoctor>0) then
				n_0PrimaryDoctor = n_0PrimaryDoctor-1;
			endif;
		endif;

		//------------------ CAN_ASSIGN RULE NUMBER 2 -----------------
		// <SUPER_ROLE,-PrimaryDoctor,Patient>
		//------------------------------------------------------------------
		if(brandom and d_SUPER_ROLE==1 and n_SUPER_ROLE>0 and b_PrimaryDoctor==0 and n_0PrimaryDoctor>0) then
			if(b_PrimaryDoctor==1) then
				n_PrimaryDoctor_Patient = n_PrimaryDoctor_Patient+1;
			endif;
			if(b_Patient==0 and n_0Patient>0) then
				n_0Patient = n_0Patient-1;
			endif;
		endif;

		//------------------- CAN_REVOKE RULE NUMBER 0 ---------------------
		// <SUPER_ROLE,PrimaryDoctor>
		//------------------------------------------------------------------
		if(brandom and d_SUPER_ROLE==1 and n_SUPER_ROLE>0 and b_PrimaryDoctor==1) then
			if(b_PrimaryDoctor==1 and b_Patient==1 and n_PrimaryDoctor_Patient>0) then
				n_PrimaryDoctor_Patient = n_PrimaryDoctor_Patient-1;
			endif;
			if(true) then
				n_0PrimaryDoctor = n_0PrimaryDoctor+1;
			endif;
		endif;

		//------------------- CAN_REVOKE RULE NUMBER 1 ---------------------
		// <SUPER_ROLE,Patient>
		//------------------------------------------------------------------
		if(brandom and d_SUPER_ROLE==1 and n_SUPER_ROLE>0 and b_Patient==1) then
			if(b_PrimaryDoctor==1 and b_Patient==1 and n_PrimaryDoctor_Patient>0) then
				n_PrimaryDoctor_Patient = n_PrimaryDoctor_Patient-1;
			endif;
			if(true) then
				n_0Patient = n_0Patient+1;
			endif;
		endif;

		//------------ ERROR Query ---------------//
		if (n_target>0) then
			skip;
		endif;
	done;  //End while loop
end  //End main