/* MODEX Version 1.0 - 20 January 2003; extended for Unified Parallel C (UPC) in February 2011 */
/* extracted from Locks.c */

#define THREADS	3

int barr = THREADS;
int proc = 0;
bool lk[THREADS];

bit read_A[THREADS];  /* THREADS */
bit write_A[THREADS];	/* THREADS */

#define race0  (read_A[0] && write_A[0])
#define race1  (read_A[1] && write_A[1])
#define race2  (read_A[2] && write_A[2])


#define fin0  (main[0]@P)
#define fin1  (main[1]@P)
#define fin2  (main[2]@P)


/*
<> fin0


#define race3  (read_A[3] && write_A[3])
#define race4  (read_A[4] && write_A[4])

#define crSec0  (main[0]@CS1 || main[0]@CS2)
#define crSec1  (main[1]@CS1 || main[1]@CS2)
#define crSec2  (main[2]@CS1 || main[2]@CS2)
#define crSec3  (main[3]@CS1 || main[3]@CS2)
#define crSec4  (main[4]@CS1 || main[4]@CS2)

#define race0 (crSec0 && (crSec1 || crSec2 || crSec3 || crSec4))
#define race1 (crSec1 && (crSec0 || crSec2 || crSec3 || crSec4))
#define race2 (crSec2 && (crSec0 || crSec1 || crSec3 || crSec4))
#define race3 (crSec3 && (crSec0 || crSec1 || crSec2 || crSec4))
#define race4 (crSec4 && (crSec0 || crSec1 || crSec2 || crSec3))
*/

active [THREADS] proctype main(    	/* D: int argc */   	/* D: char **argv */ )
{

int i, s;

      	/* 27: D: int i,s,t; */ 
      /* forall-loop: */
      atomic{ barr = barr -1;  proc=0;}  (barr == 0) || (proc == 1) -> proc = 1;  barr = barr + 1  ; 	 (barr == THREADS) || (proc == 0) -> proc = 0;  ; 	/* line  39 */ 
      skip; 	/* line  44 */ 
      /* for-loop: */
       i=_pid;  	/* line  50 */ 
	   
	   printf("i of Process %d is %d \n",_pid,i);
L_0:
      do
      ::  (i<((_pid+1)))  -> {	/* line  50 */ 
          if 		 :: {true -> s = 0;}  :: {true -> s = 1;}  :: {true -> s = 2;}  
		  /*:: {true -> s = 3;}  :: {true -> s = 4;}*/  fi     ; 	/* line  53 */ 
        /*  printf("Swap %d and %d \n",i,s);  	 line  54 */ 
          if
          ::  (s<i)  -> { 	/* line  54 */ 
              atomic{ !lk[i] -> lk[i] = 1}; 	/* line  59 */ 
              atomic{ !lk[s] -> lk[s] = 1}; 	/* line  60 */ 
       	  
			  read_A[i]=1;	 /* line  62 */ 
			  read_A[i]=0;	 		

			  read_A[s]=1;	 /* line  63 */ 	
			  read_A[s]=0;	 		
			  write_A[i]=1;	 
			  write_A[i]=0;	

			  write_A[s]=1;	  /* line  64 */ 
			  write_A[s]=0;	  
	  			  
              lk[i] = 0; 	/* line  66 */ 
              lk[s] = 0; 	/* line  67 */ 
			}
          :: else; 	/* line  67 */ 
          fi;
		  
          if
          ::  (s>i) -> { 	/* line  67 */ 
              atomic{ !lk[s] -> lk[s] = 1}; 	/* line  70 */ 
              atomic{ !lk[i] -> lk[i] = 1}; 	/* line  71 */ 
      	  
			  read_A[i]=1;	 /* line  73 */ 
			  read_A[i]=0;	 		

			  read_A[s]=1;	 /* line  74 */ 	
			  read_A[s]=0;	 		
			  write_A[i]=1;	 
			  write_A[i]=0;	

			  write_A[s]=1;	 /* line  75 */ 
			  write_A[s]=0;	  
			  
              lk[i] = 0; 	/* line  77 */ 
              lk[s] = 0; 	/* line  78 */ 
			}
          :: else; 	/* line  78 */ 
          fi;
			i = i + 1; 	/* line  78 */ 
			}
      :: else; 	/* line  78 */  -> break
      od;
      atomic{ barr = barr -1;  proc=0;}  (barr == 0) || (proc == 1) -> proc = 1;  barr = barr + 1  ; 	 (barr == THREADS) || (proc == 0) -> proc = 0;  ; 	/* line  83 */ 
     
P: skip;

/* function-calls:
	srand48()	44 
	lrand48()	53 
	printf()	89 90 99 101 54 
	upc_lock()	60 70 71 59 
	upc_unlock()	67 77 78 66 
*/
}