/* A Discrete Event Simulation Clock */
/* This is a Promela program to model a simulation clock.*/
/* A clock should manage time for processes so */
/* the process whose clock value is smallest is the next */
/* one to be scheduled.If more than one process is ready */
/* these processes should be scheduled concurrently.*/
/*The goal is to verify that the alarm*/
/* clock is correctly updated. The correctness criterion is :  */
/* When a CPU process is run, its localClock is */
/*    less than or equal to all other localClock values */

#define maxtime 5
#define numcpu 3
#define clockord simClock<=minclock
byte simClock = 0, minclock;
byte awakeTime[numcpu] = 0;

proctype cpu(byte i, waittime) 
{awakeTime[i]=waittime;
  do
  ::(awakeTime[i] < maxtime) ->
        atomic{   
             simClock == awakeTime[i]; 
             awakeTime[i]=simClock+waittime;
	}
  :: (awakeTime[i]>=maxtime) -> break
  od
}


proctype clockMonitor() 
{
	do
	:: timeout; 
	     	if
		:: (simClock < maxtime)->
		     simClock = simClock +1;
		:: (simClock >= maxtime) -> break;
		fi
	od
}
init
{ 
  atomic{ run cpu(0,1); run cpu(1,2); run cpu(2,3); 
          run clockMonitor(); 
  }
}