--- My solution to the Bakery protocol ---
-- Author : Ganesh --
--
-- PSEUDO-CODE:
--      choosing: array[1..N] of boolean initially 0;
--      number: array[1..N] of integer initially 0;
-- L1: while true do
--      Noncritical Section;
--      choosing [i] : = 1;
-- L2:  number[i] := 1 + maximum(number[1] ,..., number[N]);
-- L3:  choosing[i] := 0;
--      for each j in 1 to N do
-- L4:          if choosing[j] != 0 then goto L4;
-- L5:          if number[j] != 0 and (number[j], j) < (number[i], i) then goto L5;
--      end for;
-- L6:  CS;
--      number[i] := 0
-- od;

-------------------------------------------------------
-- The actual Murphi model --
-------------------------------------------------------
CONST
 Nprocs : 4;
 -- I checked up to ticket value of 10. Basically I allowed the tickets to climb up to 10
 -- even though we have only 4 processes.
 -- The sanity invariants checked out fine, as well.
 -- This is why you see a "+10" below
 Nprocs_1 : Nprocs+10; 
 
TYPE
 procT     : 1..Nprocs;
 nrT       : 0..Nprocs_1;
 pcT       : enum {L1, L2, L3, L4, L5, L6, Lexit};
 numarrayT : array[procT] of nrT;

VAR
 choosing  : array[procT] of Boolean;
 number    : numarrayT;
 pc        : array[procT] of pcT;
 cnt       : array [procT] of nrT;
-------------------------------------------------------
-- This function is used to stop modeling any process behavior
-- once it has seen a ticket value climb beyond Nprocs_1
-- Basically that process exits (goes to Lexit) and then
-- we don't do anything beyond that.
--
function noexit():Boolean;
Begin
 return (Forall p:procT Do pc[p] != Lexit Endforall)
End;
-------------------------------------------------------
-- Lexicographic less-than function
--
function lexlt(a:nrT; aa:nrT; b:nrT; bb:nrT):boolean;
begin
 if (a < b) then return true
 elsif (a = b) then return (aa < bb)
 else  return false
 endif;
end;

-------------------------------------------------------
-- The protocol model starts here. --
-------------------------------------------------------

-------------------------------------------------------
-- Start state
--
Startstate
For p:procT Do
 choosing[p] := false;
 number[p]   := 0;
 pc[p]       := L1;
 cnt[p]      := 1;
End;
Endstartstate;

-------------------------------------------------------
-- The behavior of each process
--
Ruleset p:procT Do
 --
 Rule "Non-crit to setting Choosing -- allowed only if nu number is > allowed!"
 pc[p] = L1
 & noexit()
   ==>
       choosing[p] := true;
       pc[p]       := L2;
 Endrule;
 --
  Rule "Choose Max"
  pc[p] = L2
  & noexit()   
  & cnt[p] <= Nprocs ==> if (number[cnt[p]] > number[p])
                        then number[p] := number[cnt[p]]
                        endif;
                        cnt[p] := cnt[p] + 1;
                        pc[p] := L2;
  Endrule;
 --
  Rule "Chosen Max; move to L3"
   pc[p] = L2
   & noexit()   
   & (cnt[p] > Nprocs)
   & (number[p] < Nprocs_1)
     ==>
     cnt[p] := 1;
     number[p] := number[p] + 1;
     pc[p] := L3;
  Endrule;
 --
 Rule "Clear choosing"
 pc[p] = L3
 & noexit() 
   ==> choosing[p] := false; pc[p] := L4; 
 Endrule;
 --
 Rule "check choosing, find true somewhere"
  pc[p] = L4
  & noexit()  
  &
  Exists q:procT Do
   choosing[q] 
  Endexists  ==> pc[p] := L4;
 Endrule;
 --
 Rule "check choosing, find false everywhere"
  pc[p] = L4
  & noexit()  
  &
  Forall q:procT Do
   !choosing[q] 
  Endforall  ==> pc[p] := L5;
 Endrule;
 --
 Rule "check number, find one j has less"
  pc[p] = L5
  & noexit()  
  &
  Exists q:procT Do
   number[q] != 0
   & lexlt(number[q],q,number[p],p)
  Endexists
   ==> pc[p] := L5;
 Endrule;
 --
 Rule "check number, find no one has j less"
  pc[p] = L5
  & noexit()  
  &
  Forall q:procT Do
   number[q] = 0
   | !lexlt(number[q],q,number[p],p)
  Endforall
   ==> pc[p] := L6; 
 Endrule; 
 --
 Rule "IN CRITICAL SECTION; set number to 0, and promptly leave"
 pc[p] = L6
 & noexit() 
   ==> number[p] := 0; pc[p] := L1;
 Endrule;


--=================================================================
-- We test the above protocol model till all remaining "bugs"
-- seem to be due to counters overflowing.
--
-- We then take care of that situation by exiting the protocol
-- as soon as some number[] counter reaches  Nprocs_1 
-- When that happens, a process goes to Lexit
--
  Rule "Chosen Max; move to L3"
   pc[p] = L2
   & noexit()   
   & (cnt[p] > Nprocs)
   & (number[p] >= Nprocs_1)
     ==>
     cnt[p] := 1;
     pc[p] := Lexit;
  Endrule;
  
 --
 -- When one process is in Lexit, all others are blocked.
 -- This process keeps flipping choosing[] because it wants
 -- to fool Murphi into thinking that there is no deadlock
 -- which, for Murphi, could be an epsilon loop!
 --
 Rule "Zombie after getting ticket"
 pc[p] = Lexit ==> choosing[p] := !choosing[p]; pc[p] := Lexit;
 Endrule; 
--=================================================================

Endruleset;

-----------------------------------------------------------------
-- This sanity invariant "Passes" in that we can falsify it.
-- This tells us that we can bring all tickets to 8 if we wish...
-- Thus we are making sure that all behaviors up to ticket values
-- equal to Nprocs_1 have been checked.
--
--Invariant "Sanity"
--  Exists p:procT Do
--    number[p] < 8
--  Endexists;
-----------------------------------------------------------------

-----------------------------------------------------------------
-- This is the main mutex invariant verified.
--
Invariant "Mutex"
 Forall p:procT Do
  Forall q:procT Do
   (p != q) -> (pc[p] != L6 | pc[q] != L6)
  Endforall 
 Endforall;
-----------------------------------------------------------------