import java.util.Hashtable;
import java.util.Enumeration;
import gov.nasa.jpf.jvm.Verify;
class AlarmClock
{ 
  private Object countMon=new Object(); //monitor for count 
  private int count=0; 
  private int now=0; // current time 
  public Hashtable clockList = new Hashtable(); 

  ////////////////////////////////////////////////

  public AlarmClock()
    {}
  /////////////////////////////////////////////////

    private Object get_mon(int time) { 
    Integer alarmSetting = new Integer(time); 
    if(clockList.containsKey(alarmSetting)) { 

    return clockList.get(alarmSetting); 
    } else { 

      Object monitor = new Object(); 
      clockList.put(alarmSetting, monitor); 
      return monitor; 
      } 
  } 

  public void wakeme(int n) { 
    int alarmsetting; 
    Object waitMonitor = null; 
    if (n > 0) { 
      synchronized (this) { 
        alarmsetting = now + n; // calculate the waken time 
	if (alarmsetting > AlarmDeadlock.maxtime) return;
        waitMonitor = get_mon(alarmsetting); // get the monitor waited 
        synchronized (waitMonitor){
          try{waitMonitor.wait();
          } catch(InterruptedException e){}
        }
      } 

    } 
  } 

  public synchronized void tick() { 
    now++;
    Integer nowInt = new Integer(now); 
    
    if(clockList.containsKey(nowInt)) { 
      Object nextMonitor = clockList.remove(nowInt); 
      synchronized (nextMonitor) { 
	nextMonitor.notifyAll(); }    
    }
  }
}    

class Client extends Thread
{
  private int id;
  private AlarmClock clock;
  private int time;

  public Client(int id,AlarmClock ck,int t)
    {
      clock=ck;
      this.id=id;
      time=t;
      start();
    }
  
  public void run() 
    {
      clock.wakeme(time);	
    }
}

class Update extends Thread 
{
  private AlarmClock clock;

  public Update(AlarmClock ck)
    {
      clock=ck;
      start();
    }
  
  public void run() 
    {
      for (int i=0;i<AlarmDeadlock.maxtime;i++)
	clock.tick();
   /////// verification ///////
      boolean rr=true;
      Enumeration test=clock.clockList.keys();
      while (test.hasMoreElements()) rr=((Integer)test.nextElement()).intValue()>=AlarmDeadlock.maxtime;
      Verify.assertTrue(rr);
    ////////////////////////////
    }
}

class AlarmDeadlock
{
  public final static int tickInterval=3;  //time intervall between each call of tick (in millisecond)
  public final static int maxtime=3;        //maximum time reached by the clock
  public final static int sleeper=2;  
  public static void main(String[] args)
    {
      // Verify.assert("test",true);
      Update up;
      Client ct;  
      AlarmClock clock=new AlarmClock();
      int[] sleepingTime = new int[sleeper];
      
      sleepingTime[0]=1;
      sleepingTime[1]=2;

      up = new Update(clock);
      for (int i=0;i<sleeper;i++)
      {ct = new Client(i,clock,sleepingTime[i]);}
    }
}