// -------------------------------------------------------------------
// Dekker's mutual exclusion algorithm
// -------------------------------------------------------------------
// The idea is that the competing threads write their id to a variable
// "last" when they leave the critical section. This determines a dynamic
// priority that breaks the symmetry. It is also possible to extend
// the algorithm to an arbitrary number of processes.
// -------------------------------------------------------------------


module Dekker(event ?start1,?start2,crit1,crit2)
{
   bool req1,req2;
   nat{4} last;
   last = 1;	// to break the symmetry, the threads write their
		// index to this variable when leaving the crit. sec.
   {
      loop {
	 await(start1);
         next(req1) = true;
         pause;
         while(req2) {
            if(last==2) {
               next(req1) = false;
               await(last==1);
               next(req1) = true;
            }
         }
         // critical section starts here
	 emit(crit1);
         pause;
         // critical section ends here
         next(last) = 2;
         next(req1) = false;
      }
   ||
      loop {
	 await(start2);
         next(req2) = true;
         pause;
         while(req1) {
            if(last==1) {
               next(req2) = false;
               await(last==2);
               next(req2) = true;
            }
         }
         // critical section starts here
	 emit(crit2);
         pause;
         // critical section ends here
         next(last) = 1;
         next(req2) = false;
      }
   }
}satisfies {
  Mutex : assert A G !(crit1 & crit2);
  Fair  : assert A ((G F start1 -> G F crit1) &
             (G F start2 -> G F crit2) );
}