import java.util.*;
import gov.nasa.jpf.jvm.Verify;

  public class TPoolBarrier {   
    // Define number of threads used in threadpool model    
  public static int THREADSFORPOOL = 2;
    
    // number of jobs	
  public static int HEIGHT;     
    // Define maximum number of iterations    
  public static int MAXITERS = 2;    
    // Threadpool object   
  ThreadPool pool;   
  BarrierForPool barrierForPool;    
  public TPoolBarrier() {	
    HEIGHT = 3;   
    pool = new   ThreadPool(THREADSFORPOOL);
        barrierForPool = new BarrierForPool(HEIGHT, pool);    
  }    
    // construct the barrier and the job objects     
  public static void main(String[]args) {        
    TPoolBarrier tPoolBarrier = new TPoolBarrier();	
    Work[] work = new Work[HEIGHT];	        for(int i = 0; i < HEIGHT; i++) {
       work[i] = new Work(i, tPoolBarrier.barrierForPool);			       
       tPoolBarrier.pool.addJob(work[i]);                
    }    
  }
}
  //This class implements the job computation for the grid simulation
class Work implements GenericJob{    
  int id;    int pc;    BarrierForPool barrier;    
  int iters = 0;    
  public Work(int id, BarrierForPool barrier){        
    this.pc = 0;       
    this.id = id;        
    this.barrier = barrier;    
  }    
  //This entry is called by threads to execute the job     
  public synchronized boolean execute() {        
    switch(pc) {            
      case 0:pc = 1;               	             
             iters = 1;                
             if(!barrier.pass(id, this, iters)) return false;
      case 1:                             if(iters >= TPoolBarrier.MAXITERS) {  /*compute*/                  
             pc = 3;     
             return true;                
    }                pc = 2;               
        iters++;		
          
        if(!barrier.pass(id, this, iters))                return false;            
      case 2:  /*copy*/              
            pc = 1;                
            iters++;		            
            if(!barrier.pass(id, this, iters))                    
               return false;                
           else return true;            
      case 3: break;		
    }       return false;    
 } 
}
class BarrierForPool {    
  boolean[] arrived;     
  int size;     
  Vector queue;    
  ThreadPool pool; 
  int[] time; 

  public BarrierForPool(int size, ThreadPool pool) {            this.size = size; 
    this.pool = pool; 
    arrived = new boolean[size]; 
    time = new int[size];
    queue = new Vector(); 
    for(int i = 0; i < size; i++) {			
      arrived[i] = false;        
    }
  }      //This is where the jobs wait in the barrier    
  synchronized public boolean pass(int id, GenericJob job, int iters) {
    time[id]=iters;
    arrived[id] = true;
    boolean go = true; 
    for(int i = 0; i < size; i++) {            
      if (!arrived[i]) {                
        go = false; break;           
    }        
  }	
  if(go) {
               for (int i = 0; i < size; i++) {			    
    arrived[i] = false;            
  }              while(!queue.isEmpty()) {            	
    pool.addJob((GenericJob)queue.remove(0));            
  }
  return true;     }        
  else {queue.add(job);  return false;        
  }    
  }
}