#define N	3	/* number of processes */

mtype = { ready, exec, success };

mtype pc1=ready;
mtype pc2= ready;
mtype pc3= ready;

#define allReady	(pc1 == pc2) && (pc2 == pc3) && (pc3 == ready)
#define allSuccess	(pc1 == pc2) && (pc2 == pc3) && (pc3 == success)

#define inv ( ((pc1 != ready) && (pc2 != ready) && (pc3 != ready)) || ((pc1 != exec) && (pc2 != exec) && (pc3 != exec)) || ((pc1 != success) && (pc2 != success) && (pc3 != success)) )



/* [](allReady -> <>allSuccess) */


proctype process1 ()
{	
do
::atomic{
	inv && (pc1 == ready) && 
			(    
				((pc2 != success) && (pc3!=success)) ||		
				((pc2 == success) && (pc3==success)) 
			)	
				
	 -> pc1 = exec;  
	}
	 
::atomic{
	inv && (pc1 == exec) && (pc2 != ready) && (pc3 !=ready)
	
	 -> pc1 = success;  
	

	}	 
	
::atomic{
	inv && (pc1 == success)  && 
				( ((pc2 == ready) && (pc3 ==ready)) ||
					((pc2 == success) && (pc3 ==success)) )
	 -> pc1 = ready;  
	

	}	 
od	
	 
}


proctype process2 ()
{	
do

::atomic{
	inv && (pc2 == ready) && 
			(    
				((pc1 != success) && (pc3!=success)) ||		
				((pc1 == success) && (pc3==success)) 
			)	
				
	 -> pc2 = exec;  
	}
	 
::atomic{
	inv && (pc2 == exec) && (pc1 != ready) && (pc3 !=ready)
	
	 -> pc2 = success;  
	

	}	 
	
::atomic{
	inv && (pc2 == success)  && 
				( ((pc1 == ready) && (pc3 ==ready)) ||
					((pc1 == success) && (pc3 ==success)) )
	 -> pc2 = ready;  
	

	}	 od	
	 
}



proctype process3()
{	
do

::atomic{
	inv && (pc3 == ready) && 
			(    
				((pc2 != success) && (pc1!=success)) ||		
				((pc2 == success) && (pc1==success)) 
			)	
				
	 -> pc3 = exec;  
	}
	 
::atomic{
	inv && (pc3 == exec) && (pc2 != ready) && (pc1 !=ready)
	
	 -> pc3 = success;  
	

	}	 
	
::atomic{
	inv && (pc3 == success)  && 
			( ((pc2 == ready) && (pc1 ==ready)) ||
			  ((pc2 == success) && (pc1 ==success)) )
	
	 -> pc3 = ready;  
	

	}	 
od	
	 
}


init {
run process1();
run process2();
run process3()

}