#define N	6    /* number of elements in each thread's region */
#define THREADS	3
#define sectionSize 3  /* is N/2 */

int barr = THREADS;
int proc = 0;

bit read_t[18];  /* N * THREADS */
bit write_t[18];	/* N * THREADS */

bool locks[6]; /* 2 * THREADS */

#define race (read_t[0] && write_t[0])

/* [] !race  */


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


active [THREADS] proctype main( ) {

int i;	/* mapped */
int j;	/* mapped */
int l;	/* mapped */
int mc;	/* mapped */
int firsttime;	/* mapped */
int done;	/* mapped */
int curlock;	/* mapped */
int oldlock;	/* mapped */

int cnt = 1;

		
		curlock=_pid*2;  /* line  50 */ 
	    printf("curlock of Process %d is: %d", _pid, curlock);
		
      i=_pid; 	/* line  83 */ 
      j=(N*_pid);  	/* line  84 */ 
      mc=0;  	/* line  84 */ 
      firsttime=1; 	/* line  85 */ 
      done=0; 	/* line  85 */ 
	  
      atomic{ !locks[curlock] -> locks[curlock] = 1}; 	/* line  86 */ 
	  
      atomic{ barr = barr -1;  proc=0;}  
	  (barr == 0) || (proc == 1) -> proc = 1;  barr = barr + 1  ; 	 
	  (barr == THREADS) || (proc == 0) -> proc = 0;  ; 	/* line  94 */ 
      
L_0:
     	/* do-while */
     {   if
      :: (j==(N*_pid)) -> {  	/* line 100 */ 
          if
          :: firsttime -> 	/* line 100 */ 
              firsttime=0;  	/* line 103 */ 

          :: else -> { 	/* line 103 */ 
            if
            :: (mc==0) -> {  	/* line 103 */ 
                done=1;  	/* line 106 */ 
                locks[curlock] = 0; 	/* line 107 */ 
				}
            :: else -> skip; 	/* line 107 */ 
            fi;
            mc=0;  	/* line 109 */
				}
          fi;
		}
      :: else -> skip; 	/* line 109 */ 
      fi;
		}
      { if
      :: (!done) -> {  	/* line 109 */ 
         { if
          :: ((j%sectionSize)==(sectionSize-1))  -> {	/* line 109 */ 
               oldlock = curlock;  	/* line 116 */ 
              curlock=((curlock+1)%(THREADS*2));  	/* line 117 */ 
              atomic{ !locks[curlock] -> locks[curlock] = 1}; 	/* line 120 */ 
			}
          :: else -> skip; 	/* line 120 */ 
          fi;
		  }
          l= i+THREADS; 	/* line 126 */ 
          {
		  if
          ::  (l >= (N*THREADS)) -> 	/* line 126 */ 
              l=((l%(N*THREADS))+1); 	/* line 128 */ 

          :: else -> skip; 	/* line 128 */ 
          fi;
		  }
		 { 
		if
			:: (cnt > 0) -> { read_t[i]=1;	 read_t[i]=0;	 ; 	/* line 131 */ 
          read_t[l]=1;	 read_t[l]=0;	 write_t[i]=1;	 write_t[i]=0;	 ; 	/* line 132 */ 
          write_t[l]=1;	 write_t[l]=0;	 ; 	/* line 133 */ 
          mc=1;  	/* line 134 */ 
		  cnt = cnt -1;
         }
			:: else-> skip;
		fi;	
		  }
		  {
          if
          ::  ((j%sectionSize)==(sectionSize-1)) -> 	/* line 134 */ 
               locks[oldlock] = 0;  	/* line 139 */ 

          :: else-> skip; 	/* line 139 */ 
          fi;
		  }
		  
           i = i + THREADS;  	/* line 144 */ 
          {
		  if
          :: (i >= (N*THREADS)) -> 	/* line 144 */ 
              i=((i%(N*THREADS))+1);  	/* line 146 */ 

          :: else-> skip; 	/* line 146 */ 
          fi;
          }
		  {
		  if
          ::  (i==((N*THREADS)-1)) -> 	/* line 146 */ 
              i=0;  	/* line 147 */ 

          :: else-> skip; 	/* line 147 */ 
          fi;
		  }
		  
          j=((j+1)%(N*THREADS));  	/* line 148 */ 
          {
		  if
          :: (j==((N*THREADS)-1)) -> 	/* line 148 */ 
              j=0;  	/* line 149 */ 

          :: else-> skip; 	/* line 149 */ 
          fi;
		  }
		}
      :: else-> skip; 	/* line 149 */ 
      fi;
	  }
	  
	  
	  
       if
          :: (!done) -> goto L_0; 	/* line 149 */ 

          :: else -> 	/* line 149 */ skip;
          fi;
		  
      
	  
	  
      atomic{ barr = barr -1;  proc=0;}  
	  (barr == 0) || (proc == 1) -> proc = 1;  barr = barr + 1  ; 	 
	  (barr == THREADS) || (proc == 0) -> proc = 0;   	
	   /*line 154 */ 
	
R: skip;	
      	/* goto Return;  198: R: return 0 
Return:	skip;  */


}