#define MAXN	3
#define THREADS	3

int barr = THREADS;
int proc = 0;

bit read_t[9];
bit write_t[9];


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

/* [] !race */

active [THREADS] proctype main()
{

int base ;	/* mapped */
int i ;	/* mapped */
int j ;	/* mapped */

      	/* 22: D: int i,j; */ 
      	/* 24: D: int base; */ 
      atomic{ barr = barr -1;  proc=0;}  (barr == 0) || (proc == 1) -> proc = 1;  barr = barr + 1  ; 	 (barr == THREADS) || (proc == 0) -> proc = 0;  ; 	/* line  50 */ 
      
	/*   c_code { Pmain->base=(Pmain->_pid*MAXN); };   line  55 */ 
	  
	  base = _pid * MAXN;  
	  
	  printf("Process %d has a base: %d", _pid, base);
      /* for-loop: */
      c_code { Pmain->j=0; }; 	/* line  60 */ 
L_0:
      do
      :: c_expr { (Pmain->j<(MAXN+1)) }; 	/* line  60 */ 
          if
          :: c_expr { (Pmain->_pid==0) }; 	/* line  60 */ 
              read_t[0]=1;	 read_t[0]=0;	 ; 	/* line  64 */ 

          :: else; 	/* line  64 */ 
            read_t[base-1] = 1; 	 read_t[base] = 1;		 read_t[base+1] = 1;		 atomic{read_t[base-1] = 0; 	read_t[base] = 0;	read_t[base+1] = 0;}	 ; 	/* line  68 */ 
            read_t[base]=1;	 read_t[base]=0;	 ; 	/* line  69 */ 
          fi;
          /* for-loop: */
        /*  c_code { Pmain->i=(Pmain->base+1); }; 	 line  71 */ 
		  i = base +1;
L_1:
          do
       /*   :: c_expr { (Pmain->i<((Pmain->base+MAXN)-1)) }; 	 line  71 */ 
		  :: ( i < base+MAXN-1) -> {
              read_t[i-1] = 1; 	 read_t[i] = 1;		 read_t[i+1] = 1;		 atomic{read_t[i-1] = 0; 	read_t[i] = 0;	read_t[i+1] = 0;}	 ; 	/* line  73 */ 
              read_t[base]=1;	 read_t[base]=0;	 ; 	/* line  74 */ 
              write_t[i-1] = 1;  write_t[i-1] = 0;  ; 	/* line  76 */ 

			/*  c_code { ++Pmain->i; }; 	 line  76 */ 
			  i = i +1;
   }
          :: else; 	/* line  76 */  -> break
          od;
          if
          :: c_expr { (Pmain->_pid<(THREADS-1)) }; 	/* line  76 */ 
              read_t[((base+MAXN)-2)] = 1; 	 read_t[((base+MAXN)-1)] = 1;		 read_t[(base+MAXN)] = 1;		 atomic{read_t[((base+MAXN)-2)] = 0; 	read_t[((base+MAXN)-1)] = 0;	read_t[(base+MAXN)] = 0;}	 ; 	/* line  81 */ 
              read_t[((base+MAXN)-1)]=1;	 read_t[((base+MAXN)-1)]=0;	 ; 	/* line  83 */ 
              write_t[((base+MAXN)-1)]=1;	 write_t[((base+MAXN)-1)]=0;	 ; 	/* line  87 */ 

          :: else; 	/* line  87 */ 
          fi;
          atomic{ barr = barr -1;  proc=0;}  (barr == 0) || (proc == 1) -> proc = 1;  barr = barr + 1  ; 	 (barr == THREADS) || (proc == 0) -> proc = 0;  ; 	/* line  89 */ 
          write_t[base+MAXN-2]=1;	 write_t[base+MAXN-2]=0;	 ; 	/* line  91 */ 
c_code { ++Pmain->j; }; 	/* line  91 */ 

      :: else; 	/* line  91 */  -> break
      od;


/* function-calls:
	fabs()	74 83 69 
*/
}