/* This program simulates several client processes who */
/* are competing for access to the disk head to read   */
/* or write (mutual exclusion of readers and writers)  */
/* The high-level scenario is:                         */
/* 1. while not done                 */
/* 2.   {request disk to read or write                 */
/* 3.    read or write mutually exclusively     */
/* 4.    release disk                           */
/* 5.   }                                       */
/* This specific model schedules access to the disk  */
/* in a monotonically increasing nature. That is, if */
/* the newest request cylinder is greater than or equal */
/* to the current cylinder being service, we put the */
/* new request in the "current" queue. If the new    */
/* request is less than the current cylinder, put the */
/* new request in the "next" queue. Both queues are */
/* priority queues order from smallest to largest */
/* request cylinder. The queues also contain the "myId" */
/* of the process requesting the cylinder.            */
/* See Andrews (1991) Section 6.4 for details.         */
#define maxCyl 255
#define numClients 3
#define numCycles 5
chan ReqQue [2] = [maxCyl] of {byte};
int currCyl = -1; 
int currScan = 0; 
int count =0;
proctype client(byte myId){
  byte j = 0; 
  byte myReqCyl = 0;
  do
  :: (j<=numCycles) -> j=j+1;
    myReqCyl = 0 ;
    atomic {
    if
    :: (currCyl == -1) -> currCyl = myReqCyl
    :: (currCyl != -1 && myReqCyl > currCyl) -> 
	      ReqQue[currScan]!!myReqCyl
    :: (currCyl != -1 && myReqCyl <= currCyl) ->
	      ReqQue[1-currScan]!!myReqCyl
    fi;
    (myReqCyl == currCyl)
	      -> count++;
    }
/*read or write the disk in a mutually exclusive fashion  */
    assert(count ==1);
    atomic{count--;
    if
    :: nempty(ReqQue[currScan]) -> ReqQue[currScan]?currCyl;
    :: empty(ReqQue[currScan]) && nempty(ReqQue[1-currScan])-> 
	       currScan=1-currScan; ReqQue[currScan]?currCyl;
    :: (empty(ReqQue[currScan]) && empty(ReqQue[1-currScan]))->
	       currCyl =-1; 
    fi
    }
  :: (j>numCycles)-> break;
  od
}
init
  {byte j=0;
    atomic{
      do
      :: (j<numClients) -> run client(j);
	 j=j+1
      :: (j>=numClients) -> break
      od
      }
 }