#define N	3	/* number of processes */

#define s1	((x1 == x2) && (x2 == x3)) || ((x1 == x2) && (x2 != x3)) || ((x1 != x2) && (x2 == x3))

#define s2	((x1 == x2) && (x2 == x3)) 


int x1 =1;
int x2 =2;
int x3 = 1;


/* [](<> s1) */

proctype process1 ()
{	
do
::atomic{ 	
 (x3 != ((x1+3) % 4)) -> x1 = (x3+1) % 4;
	}
od	
	 
}

proctype process2 ()
{	
do
::atomic{ 	(x1 != x2)  -> x2 = x1;
		}
od	
}


proctype process3 ()
{	
do
::atomic{ 	(x3 != x2)  -> x3 = x2;
		}
od	
}


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

}