#include "dtime.h"

/* A model of Fischer's mutual exclusion protocol */
/* The protocol ensures mutual exclusion iff deltaB < deltaC */


#define	N	5		/* number of processes */

#define deltaB  1		/* timing parameters */
#define deltaC  2


byte	x,         /* shared synchronization variable */
        in_crit;  /* auxiliary variable */

proctype P(byte id)
{

timer y,       /* local clock for mutual exclusion */
      y1;      /* auxiliary local clock */

do 
::
        udelay(y);                     /* unbounded start delay */
           x==0 ->
        atomic{bdelay(y,deltaB,y1) ->         /* y <= deltaB */
           x=id+1;} 
	atomic{delay(y, deltaC); udelay(y)} -> /* y >= deltaC */
           atomic{x==id+1; in_crit++;} ->
        udelay(y);     /*critical section*/ 
	   atomic{ x=0; in_crit--}	
od
}


never{
       do
       :: in_crit > 1 -> break; /* error - more than one process in
                                   the critical section */
       :: skip 
       od
}


init 
{
        atomic{
                run P(0); run P(1); run P(2); run P(3); run P(4); 
              }
}