int x1 =1;
int x2 =2;
int x3 = 1;
active proctype process1 ()
{	
do
::atomic{ 	
	 (x3 != ((x1+3) % 4)) -> x1 = (x3+1) % 4;
	}
od	
	 
}
active proctype process2 ()
{	
do
::atomic{
 	(x1 != x2)  -> x2 = x1;
	}
od	
}
active proctype process3 ()
{	
do
::atomic{
	(x3 != x2)  -> x3 = x2;
	}
od	
}