// ============================================================================
// Name:        BarberShop
// Description: The barber problem illustrates the client/server relationship
//                between processes and contains rendezvous-like synchronization.
// References:  G.R. Andrews. Concurrent Programming - Principles and Practice.
//              The Benjamin/Cummings Publishing Company, 1991.
// Parameters:  size (number of processes)
// ============================================================================

package Communication.MutexProtocols.BarberShop;

macro size = 3;

module BarberShop(nat{size()} ?go,
                  int cinchair,cleave,bavail,bbusy,bdone)
{
      for(i=1 ..size()) do ||
         suspend
            loop
               GetHaircut(cinchair,cleave,bavail,bdone);
         when(go!=i);
   ||
      suspend
         loop {
            NextCustomer(cinchair,bavail,bbusy);
            pause;
            FinishHairCut(cleave, bdone);
         }
      when(go!=0);
}satisfies {
  S1: assert A G (cinchair>=cleave & bavail>=bbusy & bbusy>=bdone);
  S2: assert A G (cinchair<=bavail & bbusy<=cinchair);
  S3: assert A G (cleave<=bdone);
}