--
-- the MCS mutual exclusion protocol
--

-- Variables:
--   glock : Pid, initially nop, shared with all processes
--   next_p : Pid, initially nop
--   lock_p : Bool, initially false
--   pred_p : Pid, initially nop
-- 
-- A pseudo-code of the MCS protocol for each process p:
-- 
-- rs:  \"Remainder Section\"
-- l1:  next_p := nop;
-- l2:  pred_p := fetch&store(glock,p);
-- l3:  if pred_p =/= nop {
-- l4:    lock_p := true;
-- l5:    next_{pred_p} := p;
-- l6:    repeat while lock_p; }
-- cs:  \"Critical Section\"
-- l7:  if next_p = nop {
-- l8:    if comp&swap(glock,p,nop)
-- l9:      goto rs;
-- l10:   repeat while next_p = nop; }
-- l11: locked_{next_p} := false;
-- l12: goto rs;
-- 
-- where
-- 
-- fetch&store(x,v) does the following atomically:
-- tmp := x, x := v, and tmp is returned.
-- 
-- comp&swap(x,v1,v2) does the following atomically:
-- if x = v1, then x := v2 and true is returned,
-- Otherwise, false is returned.
--

mod! LABEL {
  [Label]
  ops l1 l2 l3 l4 l5 l6 l7 l8 l9 l10 l11 l12 rs cs : -> Label {constr} .
  eq (l1 = l2) = false .
  eq (l1 = l3) = false .
  eq (l1 = l4) = false .
  eq (l1 = l5) = false .
  eq (l1 = l6) = false .
  eq (l1 = l7) = false .
  eq (l1 = l8) = false .
  eq (l1 = l9) = false .
  eq (l1 = l10) = false .
  eq (l1 = l11) = false .
  eq (l1 = l12) = false .
  eq (l1 = rs) = false .
  eq (l1 = cs) = false .
  eq (l2 = l3) = false .
  eq (l2 = l4) = false .
  eq (l2 = l5) = false .
  eq (l2 = l6) = false .
  eq (l2 = l7) = false .
  eq (l2 = l8) = false .
  eq (l2 = l9) = false .
  eq (l2 = l10) = false .
  eq (l2 = l11) = false .
  eq (l2 = l12) = false . 
  eq (l2 = rs) = false .
  eq (l2 = cs) = false .
  eq (l3 = l4) = false .
  eq (l3 = l5) = false .
  eq (l3 = l6) = false .
  eq (l3 = l7) = false .
  eq (l3 = l8) = false .
  eq (l3 = l9) = false .
  eq (l3 = l10) = false .
  eq (l3 = l11) = false .
  eq (l3 = l12) = false .
  eq (l3 = rs) = false .
  eq (l3 = cs) = false .
  eq (l4 = l5) = false .
  eq (l4 = l6) = false .
  eq (l4 = l7) = false .
  eq (l4 = l8) = false .
  eq (l4 = l9) = false .
  eq (l4 = l10) = false .
  eq (l4 = l11) = false .
  eq (l4 = l12) = false .
  eq (l4 = rs) = false .
  eq (l4 = cs) = false .
  eq (l5 = l6) = false .
  eq (l5 = l7) = false .
  eq (l5 = l8) = false .
  eq (l5 = l9) = false .
  eq (l5 = l10) = false .
  eq (l5 = l11) = false .
  eq (l5 = l12) = false .
  eq (l5 = rs) = false .
  eq (l5 = cs) = false .
  eq (l6 = l7) = false .
  eq (l6 = l8) = false .
  eq (l6 = l9) = false .
  eq (l6 = l10) = false .
  eq (l6 = l11) = false .
  eq (l6 = l12) = false .
  eq (l6 = rs) = false .
  eq (l6 = cs) = false .
  eq (l7 = l8) = false .
  eq (l7 = l9) = false .
  eq (l7 = l10) = false .
  eq (l7 = l11) = false .
  eq (l7 = l12) = false .
  eq (l7 = rs) = false .
  eq (l7 = cs) = false .
  eq (l8 = l9) = false .
  eq (l8 = l10) = false .
  eq (l8 = l11) = false .
  eq (l8 = l12) = false .
  eq (l8 = rs) = false .
  eq (l8 = cs) = false .
  eq (l9 = l10) = false .
  eq (l9 = l11) = false .
  eq (l9 = l12) = false .
  eq (l9 = rs) = false .
  eq (l9 = cs) = false .
  eq (l10 = l11) = false .
  eq (l10 = l12) = false .
  eq (l10 = rs) = false .
  eq (l10 = cs) = false .
  eq (l11 = l12) = false .
  eq (l11 = rs) = false .
  eq (l11 = cs) = false .
  eq (l12 = rs) = false .
  eq (l12 = cs) = false .
  eq (rs = cs) = false .
}

mod* PID {
  [Nop Pid < Pid&Nop]
  op nop : -> Nop {constr} .
    var P : Pid .
    eq (P = nop) = false .
}

mod* MCS {
  pr(LABEL)
  pr(PID)
  [Sys]
  -- initial states
  op init : -> Sys {constr} .
  -- transitions
  -- st: set, ch: check, nxt: next, prd: pred, lck: lock
  -- npr: next & pred, glk: glock, lnx; lock & next
  op want : Sys Pid -> Sys {constr} .
  op stnxt : Sys Pid -> Sys {constr} .
  op stprd : Sys Pid -> Sys {constr} .
  op chprd : Sys Pid -> Sys {constr} .
  op stlck : Sys Pid -> Sys {constr} .
  op stnpr : Sys Pid -> Sys {constr} .
  op chlck : Sys Pid -> Sys {constr} .
  op exit : Sys Pid -> Sys {constr} .
  op chnxt : Sys Pid -> Sys {constr} . -- rpnxt
  op chglk : Sys Pid -> Sys {constr} .
  op go2rs : Sys Pid -> Sys {constr} .
  op chnxt2 : Sys Pid -> Sys {constr} .
  op stlnx : Sys Pid -> Sys {constr} .
  op go2rs2 : Sys Pid -> Sys {constr} .
  -- observers
  op glock : Sys -> Pid&Nop .
  op pc : Sys Pid -> Label .
  op next : Sys Pid -> Pid&Nop .
  op lock : Sys Pid -> Bool .
  op pred : Sys Pid -> Pid&Nop .
  --
  -- variables
  var S : Sys .
  vars P Q : Pid .
  --
  -- init
  eq glock(init) = nop .
  eq pc(init,P) = rs .
  eq next(init,P) = nop .
  eq lock(init,P) = false .
  eq pred(init,P) = nop .

  -- want
  ceq glock(want(S,P)) = glock(S) if pc(S,P) = rs .
  ceq pc(want(S,P),Q)
   = (if P = Q then l1 else pc(S,Q) fi)
   if pc(S,P) = rs .
  ceq next(want(S,P),Q) = next(S,Q) if pc(S,P) = rs .
  ceq lock(want(S,P),Q) = lock(S,Q) if pc(S,P) = rs .
  ceq pred(want(S,P),Q) = pred(S,Q) if pc(S,P) = rs .
  ceq want(S,P) = S if not pc(S,P) = rs .


  -- stnxt
  ceq glock(stnxt(S,P)) = glock(S) if pc(S,P) = l1 .
  ceq pc(stnxt(S,P),Q)
   = (if P = Q then l2 else pc(S,Q) fi)
   if pc(S,P) = l1 .
  ceq next(stnxt(S,P),Q)
   = (if P = Q then nop else next(S,Q) fi)
   if pc(S,P) = l1 .
  ceq lock(stnxt(S,P),Q) = lock(S,Q) if pc(S,P) = l1 .
  ceq pred(stnxt(S,P),Q) = pred(S,Q) if pc(S,P) = l1 .
  ceq stnxt(S,P) = S if not pc(S,P) = l1 .

  -- stprd

  ceq pc(stprd(S,P),Q)
   = (if P = Q then l3 else pc(S,Q) fi)
   if pc(S,P) = l2 .
  ceq next(stprd(S,P),Q) = next(S,Q) if pc(S,P) = l2 .
  ceq lock(stprd(S,P),Q) = lock(S,Q) if pc(S,P) = l2 .
  ceq pred(stprd(S,P),Q)
   = (if P = Q then glock(S) else pred(S,Q) fi)
   if pc(S,P) = l2 .
  ceq glock(stprd(S,P)) = P if pc(S,P) = l2 .
  ceq stprd(S,P) = S if not pc(S,P) = l2 .


  -- chprd
  ceq glock(chprd(S,P)) = glock(S) if pc(S,P) = l3 .
  ceq pc(chprd(S,P),Q)
   = (if P = Q
      then (if pred(S,P) = nop then cs else l4 fi)
      else pc(S,Q)
      fi)
   if pc(S,P) = l3 .
  ceq next(chprd(S,P),Q) = next(S,Q) if pc(S,P) = l3 .
  ceq lock(chprd(S,P),Q) = lock(S,Q) if pc(S,P) = l3 .
  ceq pred(chprd(S,P),Q) = pred(S,Q) if pc(S,P) = l3 .
  ceq chprd(S,P) = S if not pc(S,P) = l3 .


  -- stlck
  ceq glock(stlck(S,P)) = glock(S) if pc(S,P) = l4 .
  ceq pc(stlck(S,P),Q)
   = (if P = Q then l5 else pc(S,Q) fi)
   if pc(S,P) = l4 .
  ceq next(stlck(S,P),Q) = next(S,Q) if pc(S,P) = l4 .
  ceq lock(stlck(S,P),Q)
   = (if P = Q then true else lock(S,Q) fi )
   if pc(S,P) = l4 .
  ceq pred(stlck(S,P),Q) = pred(S,Q) if pc(S,P) = l4 .
  ceq stlck(S,P) = S if not pc(S,P) = l4 .


  -- stnpr
  ceq glock(stnpr(S,P)) = glock(S) if pc(S,P) = l5 .
  ceq pc(stnpr(S,P),Q)
   = (if P = Q then l6 else pc(S,Q) fi)
   if pc(S,P) = l5 .
  ceq next(stnpr(S,P),Q)
   = (if pred(S,P) = Q then P else next(S,Q) fi)
   if pc(S,P) = l5 .
  ceq lock(stnpr(S,P),Q) = lock(S,Q) if pc(S,P) = l5 .
  ceq pred(stnpr(S,P),Q) = pred(S,Q) if pc(S,P) = l5 .
  ceq stnpr(S,P) = S if not pc(S,P) = l5 .

  -- chlck
  ceq glock(chlck(S,P)) = glock(S) if pc(S,P) = l6 .
  ceq pc(chlck(S,P),Q)
   = (if P = Q
      then (if lock(S,P) then l6 else cs fi)
      else pc(S,Q)
      fi)
   if pc(S,P) = l6 .
  ceq next(chlck(S,P),Q) = next(S,Q) if pc(S,P) = l6 .
  ceq lock(chlck(S,P),Q) = lock(S,Q) if pc(S,P) = l6 .
  ceq pred(chlck(S,P),Q) = pred(S,Q) if pc(S,P) = l6 .
  ceq chlck(S,P) = S if not pc(S,P) = l6 .

  -- exit 
  ceq glock(exit(S,P)) = glock(S) if pc(S,P) = cs .
  ceq pc(exit(S,P),Q)
   = (if P = Q then l7 else pc(S,Q) fi)
   if pc(S,P) = cs .
  ceq next(exit(S,P),Q) = next(S,Q) if pc(S,P) = cs .
  ceq lock(exit(S,P),Q) = lock(S,Q) if pc(S,P) = cs .
  ceq pred(exit(S,P),Q) = pred(S,Q) if pc(S,P) = cs .
  ceq exit(S,P) = S if not pc(S,P) = cs .

  -- chnxt
  ceq glock(chnxt(S,P)) = glock(S) if pc(S,P) = l7 .
  ceq pc(chnxt(S,P),Q)
   = (if P = Q
      then (if next(S,P) = nop then l8 else l11 fi)
      else pc(S,Q)
      fi)
   if pc(S,P) = l7 .
  ceq next(chnxt(S,P),Q) = next(S,Q) if pc(S,P) = l7 .
  ceq lock(chnxt(S,P),Q) = lock(S,Q) if pc(S,P) = l7 .
  ceq pred(chnxt(S,P),Q) = pred(S,Q) if pc(S,P) = l7 .
  ceq chnxt(S,P) = S if not pc(S,P) = l7 .

  -- chglk
  ceq glock(chglk(S,P))
   = (if P = glock(S) then nop else glock(S) fi)
   if pc(S,P) = l8 .
  ceq pc(chglk(S,P),Q)
   = (if P = Q
      then (if P = glock(S) then l9 else l10 fi)
      else pc(S,Q)
      fi)
   if pc(S,P) = l8 .
  ceq next(chglk(S,P),Q) = next(S,Q) if pc(S,P) = l8 .
  ceq lock(chglk(S,P),Q) = lock(S,Q) if pc(S,P) = l8 .
  ceq pred(chglk(S,P),Q) = pred(S,Q) if pc(S,P) = l8 .
  ceq chglk(S,P) = S if not pc(S,P) = l8 .

  -- go2rs
  ceq glock(go2rs(S,P)) = glock(S) if pc(S,P) = l9 .
  ceq pc(go2rs(S,P),Q)
   = (if P = Q then rs else pc(S,Q) fi)
   if pc(S,P) = l9 .
  ceq next(go2rs(S,P),Q) = next(S,Q) if pc(S,P) = l9 .
  ceq lock(go2rs(S,P),Q) = lock(S,Q) if pc(S,P) = l9 .
  ceq pred(go2rs(S,P),Q) = pred(S,Q) if pc(S,P) = l9 .
  ceq go2rs(S,P) = S if not pc(S,P) = l9 .
  -- chnxt2
  ceq glock(chnxt2(S,P)) = glock(S) if pc(S,P) = l10 .
  ceq pc(chnxt2(S,P),Q)
   = (if P = Q
      then (if next(S,P) = nop then l10 else l11 fi)
      else pc(S,Q)
      fi)
   if pc(S,P) = l10 .
  ceq next(chnxt2(S,P),Q) = next(S,Q) if pc(S,P) = l10 .
  ceq lock(chnxt2(S,P),Q) = lock(S,Q) if pc(S,P) = l10 .
  ceq pred(chnxt2(S,P),Q) = pred(S,Q) if pc(S,P) = l10 .
  ceq chnxt2(S,P) = S if not pc(S,P) = l10 .


  -- stlnx
  ceq glock(stlnx(S,P)) = glock(S) if pc(S,P) = l11 .
  ceq pc(stlnx(S,P),Q)
   = (if P = Q then l12 else pc(S,Q) fi)
   if pc(S,P) = l11 .
  ceq next(stlnx(S,P),Q) = next(S,Q) if pc(S,P) = l11 .

  ceq lock(stlnx(S,P),Q)
   = (if Q = next(S,P) then false else lock(S,Q) fi)
   if pc(S,P) = l11 .

  ceq pred(stlnx(S,P),Q) = pred(S,Q) if pc(S,P) = l11 .
  ceq stlnx(S,P) = S if not pc(S,P) = l11 .

  -- go2rs2
  ceq glock(go2rs2(S,P)) = glock(S) if pc(S,P) = l12 .
  ceq pc(go2rs2(S,P),Q)
   = (if P = Q then rs else pc(S,Q) fi)
   if pc(S,P) = l12 .
  ceq next(go2rs2(S,P),Q) = next(S,Q) if pc(S,P) = l12 .
  ceq lock(go2rs2(S,P),Q) = lock(S,Q) if pc(S,P) = l12 .
  ceq pred(go2rs2(S,P),Q) = pred(S,Q) if pc(S,P) = l12 .
  ceq go2rs2(S,P) = S if not pc(S,P) = l12 .

}


mod! INV {
pr(MCS)

-- invariants

op mutex : Sys Pid Pid -> Bool

op inv1 : Sys Pid Pid -> Bool
op inv2 : Sys Pid Pid -> Bool
op inv3 : Sys Pid Pid -> Bool
op inv4 : Sys Pid  -> Bool
op inv5 : Sys Pid Pid -> Bool
op inv6 : Sys Pid  -> Bool
op inv7 : Sys Pid Pid -> Bool
op inv8 : Sys Pid Pid -> Bool
op inv9 : Sys Pid  -> Bool
op inv10 : Sys Pid Pid -> Bool
op inv11 : Sys Pid Pid Pid -> Bool
op inv12 : Sys Pid  -> Bool
op inv13 : Sys Pid Pid  -> Bool
op inv14 : Sys Pid   -> Bool
op inv15 : Sys Pid Pid  -> Bool
op inv16 : Sys Pid   -> Bool
op inv17 : Sys Pid   -> Bool
op inv18 : Sys Pid   -> Bool
op inv19 : Sys Pid Pid Pid -> Bool

var S : Sys
vars P Q R Z A B : Pid

-- -------------------------------------------- property mutex  ----------------------------

eq mutex(S,P,Q) = (pc(S,P) = cs and pc(S,Q) = cs implies (P = Q)) .

-- -------------------------------------------- invariants      ----------------------------

eq inv1(S,P,Q) =  (( (pc(S,Q) = l3 and pred(S,Q) = nop)  and (not P = Q))
                implies not(pc(S,P) = l7 or pc(S,P) = l8 or pc(S,P) = l10 or pc(S,P) = l11 or pc(S,P) = cs)) .


eq inv2(S,P,Q) = ((((pc(S,P) = cs or pc(S,P) = l11 or pc(S,P) = l10 or pc(S,P) = l8 or pc(S,P) = l7)
                or (pc(S,P) = l3 and pred(S,P) = nop)) and (pc(S,Q) = l6))
                implies (lock(S,Q) = true)) .

eq inv3(S,P,Q) = ( ((pc(S,Q) = l11 or pc(S,Q) = l10 or pc(S,Q) = cs or pc(S,Q) = l8 or pc(S,Q) = l7 ) and (not P = Q))
                    implies (not(pc(S,P) = l11 or pc(S,P) = l10 or pc(S,P) = l8 or pc(S,P) = l7 or pc(S,P) = cs))) .

eq inv4(S,P) = ((glock(S) = nop) implies (pc(S,P) = l1 or pc(S,P) = l2 or pc(S,P) = l9 or pc(S,P) = l12 or pc(S,P) = rs) ) .

eq inv5(S,P,Q)  =  ( ((pc(S,Q) = l4 or pc(S,Q) = l5 or pc(S,Q) = l3 ) and (not P = Q)
                    and (pc(S,P) = l5 or pc(S,P) = l4 or pc(S,P) = l3 ))
                    implies not(pred(S,Q) = pred(S,P)) ) .

eq inv6(S,P) = (pc(S,P) = l5  implies lock(S,P) = true) .

eq inv7(S,P,Q) = (((pc(S,Q) = l6 and lock(S,Q) = false)  and (not P = Q) and (pc(S,P) = l6))
                    implies lock(S,P) = true ) .


eq inv8(S,P,Q) = (( ( (pc(S,Q) = l8 or pc(S,Q) = l7 or pc(S,Q) = cs)
                or (pc(S,Q) = l6 and lock(S,Q) = false) or (pc(S,Q) = l3 and pred(S,Q) = nop))
                and (glock(S) = Q)  and (not P = Q))
                implies (pc(S,P) = l1 or pc(S,P) = l2 or pc(S,P) = l9 or pc(S,P) = l12 or pc(S,P) = rs) ) .

eq inv9(S,P)  = ( (pc(S,P) = l3 or pc(S,P) = l4 or pc(S,P) = l5) implies (not (glock(S) = pred(S,P))) )  .

eq inv10(S,P,Q) = ( ( not(pc(S,Q) = l12 or pc(S,Q) = l1 or pc(S,Q) = rs) and (next(S,Q) = P)  )
                    implies ( pc(S,P) = l6 and lock(S,P) = true and pred(S,P) = Q) ) .

eq inv11(S,P,Q,R) = (( ((pc(S,R) = l11 or pc(S,R) = l7 or pc(S,R) = l10 or pc(S,R) = cs or pc(S,R) = l8)
                    or (pc(S,R) = l6 and lock(S,R) = false) or (pc(S,R) = l3 and pred(S,R) = nop))
                    and (pc(S,Q) = l6 and lock(S,Q) = true) and (glock(S) = Q)
                    and (not P = R) and (not P = Q)
                    and (next(S,R) = Q or not(pc(S,P) = l6 or pc(S,P) = l5 or pc(S,P) = l4 or pc(S,P) = l3 )) )
                    implies (pc(S,P) = l1 or pc(S,P) = l2 or pc(S,P) = l9 or pc(S,P) = l12 or pc(S,P) = rs) ) .


eq inv12(S,P) = ((pc(S,P) = l2 or pc(S,P) = l1 or pc(S,P) = rs or pc(S,P) = l9 or pc(S,P) = l12 or pc(S,P) = l11 or pc(S,P) = l10)
                    implies (not glock(S) = P)  ) .

eq inv13(S,P,Q)  = (((pc(S,Q) = l4 or pc(S,Q) = l5 or pc(S,Q) = l3 ) and (not P = Q) and (pred(S,Q) = P))
                    implies (not(pc(S,P) = l2 or pc(S,P) = l1 or pc(S,P) = rs or pc(S,P) = l9 or  pc(S,P) = l12 or pc(S,P) = l11)
                                and (next(S,P) = nop))) .

eq inv14(S,P) = (not pred(S,P) = P ) .


eq inv15(S,P,Q) =  (( (not(pc(S,P) = l1 or pc(S,P) = l12 or pc(S,P) = rs)) and (not P = Q) and not(next(S,Q) = nop)
                    and (not(pc(S,Q) = l1 or pc(S,Q) = l12 or pc(S,Q) = rs) ))
                    implies not(next(S,P) = next(S,Q))) .

eq inv16(S,P)  =  ((glock(S) = P) implies (next(S,P) = nop)) .

eq inv17(S,P)  = ((pc(S,P) = l2 or pc(S,P) = l9)   implies ( next(S,P) = nop)  ) .

eq inv18(S,P) = (not next(S,P) = P ) .

eq inv19(S,P,Q,R) = ((((pc(S,R) = l11 or pc(S,R) = l7 or pc(S,R) = l10 or pc(S,R) = cs or pc(S,R) = l8)
                        or (pc(S,R) = l6 and lock(S,R) = false) or (pc(S,R) = l3 and pred(S,R) = nop))
                        and (pc(S,Q) = l5 or pc(S,Q) = l4 or pc(S,Q) = l3 ) and (glock(S) = Q)
                        and (not P = R) and (not P = Q) and (pred(S,Q) = R) )
                        implies (pc(S,P) = l1 or pc(S,P) = l2 or pc(S,P) = l9 or pc(S,P) = l12 or pc(S,P) = rs)) .



}