// --------------------------------------------------------------------	
// This file is the same as Ticket.qrz except that the default is to
// use unbounded integers and that the specifications were given in
// mu-calculus.
//				
//  References:
//	G.R. Andrews' book, Concurrent Programming, chapter 3.3, 1991
// --------------------------------------------------------------------	

package Communication.MutexProtocols.TicketMu;

// number of processes
macro NumProc = 4;


module TicketProtocol
   (event ?leave_cs,			// instructs to leave the critical section
    nat{NumProc()} ?go,	  		// used to control interleaved execution
    nat{4} crit_var,			// shared variable used in critic section
    int{NumProc()} next_ticket,		// ticket to be drawn by next customer
    int{NumProc()} served_ticket,	// ticket number of currently served customer
    [NumProc()] int{NumProc()} ticket,	// tickets already drawn by customers
    [NumProc()] bool !done,		// to check successful termination
    [NumProc()] bool spin)		// to see that process applies for CS
{
   for(i=0 .. (NumProc()-1)) do ||
      suspend
         loop {
	    pause;
	    EntryProtocol(served_ticket,ticket[i],next_ticket);
	    CriticalSection(leave_cs,crit_var);
	    ExitProtocol(served_ticket,done[i]);
         }
      when(go!=i);
}satisfies {
   // ============================================================
   MutualExclusive:
   // ------------------------------------------------------------
   // at most one process can enter critical section
   // ------------------------------------------------------------
	assert nu z.( (crit_var<=1) & [] z);
   // ============================================================
   EnterLemma:
   // ------------------------------------------------------------
   // a process will enter its critical section if it currently
   // is enabled by the scheduler in a stage where it applies
   // for the critical section and the critical section is free
   // note that
   // ------------------------------------------------------------
	assert nu z.( 
	   forall(i = 0 .. (NumProc()-1))
	      ( spin[i] & (ticket[i]==served_ticket) & (go==i) -> [] !spin[i] )
	   & [] z);
   // ============================================================
   NoDeadlock:
   // ------------------------------------------------------------
   // if several processes apply for accessing the critical section
   // and the critical section is free, then one of them enters it
   // ------------------------------------------------------------
	assert nu z.( 
	  ((crit_var == 0)
           ->
	   forall(i = 0 .. (NumProc()-1))
	      (spin[i] & (go==i) -> [] (!spin[i] & (crit_var > 0)))
	  )
	   & [] z);
   // ============================================================
   EventualEntry:
   // ------------------------------------------------------------
   // fairness is very hard to achieve: it only holds if the
   // scheduler does not always choose the same process out of
   // the processes that are applying for the critical section
   // ------------------------------------------------------------
	assert A (
	   G forall(i = 0 .. (NumProc()-1))
	      (F(leave_cs & (go==i)))
	   ->
	   G forall(i = 0 .. (NumProc()-1))
	      (F done[i])
	  );
   // ============================================================
}