fmod NODEID is
  pr NAT .
  sort NodeID .
  subsorts NodeID < NzNat .
--- Parameters  
  op N : -> NzNat . --- the number of nodes
  op M : -> Nat .   --- the number of requests each node makes
---
  eq N = 2 .
  eq M = 2 .
  mb 1 : NodeID .
  mb 2 : NodeID .
endfm

fmod QUEUE is
  pr NODEID .
  sort NeQueue Queue .
  subsort NeQueue < Queue .
  op empty : -> Queue .
  op _|_ : NodeID Queue -> NeQueue .
  op top : NeQueue -> NodeID .
  op put : Queue NodeID -> Queue .
  op get : Queue -> Queue .
  op _\in_ : NodeID Queue -> Bool .
  op empty? : Queue -> Bool .
  vars I J : NodeID .
  var Q : Queue .
  eq top(I | Q) = I .
  eq put(empty,I) = I | empty .
  eq put(J | Q,I) = J | put(Q,I) .
  eq get(empty) = empty .
  eq get(I | Q) = Q .
  eq I \in (I | Q) = true .
  eq I \in Q = false [owise] .
  eq empty?(empty) = true .
  eq empty?(I | Q) = false .
endfm

fmod ARRAY is
  pr NODEID .
  sort AElm Array .
  subsort AElm < Array .
  op ia : -> Array .
  op _:_ : NodeID Nat -> AElm .
  op _,_ : Array Array -> Array [assoc comm id: ia] .
  op _[_] : Array NodeID -> Nat .
  op _[_] :=_ : Array NodeID Nat -> Array .
  var A : Array .
  vars I J : NodeID .
  vars X Y : Nat .
  eq ((I : X) , A)[I] = X .
  eq A[I] = 0 [owise] .
  eq (((I : X) , A)[I] := Y) = (I : Y) , A .
  eq (A[I] := Y) = (I : Y) , A [owise] .
endfm

fmod REQUEST is
  pr NODEID .
  sort Request .
  op req : NodeID Nat -> Request .
  op node : Request -> NodeID .
  op sn : Request -> Nat .
  var J : NodeID .
  var X : Nat .
  eq node(req(J,X)) = J .
  eq sn(req(J,X)) = X .
endfm

fmod PRIVILEGE is
  pr QUEUE .
  pr ARRAY .
  sort Privilege .
  op priv : Queue Array -> Privilege .
  op q : Privilege -> Queue .
  op ln : Privilege -> Array .
  var Q : Queue .
  var A : Array .
  eq q(priv(Q,A)) = Q .
  eq ln(priv(Q,A)) = A .
endfm

fmod MESSAGE is
  pr REQUEST .
  pr PRIVILEGE .
  sort Message .
  op msg : NodeID Request -> Message .
  op msg : NodeID Privilege -> Message .
endfm

fmod NETWORK is
  pr MESSAGE .
  sort Network .
  subsort Message < Network .
  op void : -> Network .
  op _ _ : Network Network -> Network [assoc comm id: void] .
  op _\in_ : Message Network -> Bool .
  op del : Network Message -> Network .
  var M : Message .
  var N : Network .
  eq M \in (M N) = true .
  eq M \in N = false [owise] .
  eq del((M N),M) = N .
  eq del(N,M) = N [owise] .
endfm

fmod LABEL is
  sort Label .
  ops rem l1 l2 l3 l4 l5 cs l6 l7 l8 l9 l10 : -> Label .
endfm

mod SK is
  pr NETWORK .
  pr LABEL .
  sort Trans Obs Sys .
  subsort Trans Obs < Sys .
--- Configurations
  op none :             -> Sys .
  op _ _   : Sys Sys -> Sys [assoc comm id: none] .
--- Observers
  op numOfReq[_]:_   : NodeID Nat   -> Obs . --- for model-checking
  op pc[_]:_         : NodeID Label  -> Obs .
  op requesting[_]:_ : NodeID Bool  -> Obs .
  op havePriv[_]:_   : NodeID Bool  -> Obs .
  op rn[_]:_         : NodeID Array -> Obs .
  op ln[_]:_         : NodeID Array -> Obs .
  op queue[_]:_      : NodeID Queue -> Obs .
  op idx[_]:_        : NodeID Nat   -> Obs .
  op nw:_            : Network      -> Obs .
--- transitions
--- Maude variables
  var S : Sys .
  vars I J : NodeID . 
  vars X Max : Nat .
  vars F F' C : Bool .
  vars RN LN LN' : Array .
  vars Q Q' : Queue .
  var NW : Network .
  var L : Label .
--- try
  rl [try] : 
    (numOfReq[I]: X)
    (pc[I]: rem) 
    => (numOfReq[I]: (if X < M then X + 1 else X fi))
       (pc[I]: (if X < M then l1 else rem fi)) .
--- setReq
  rl [setReq] : 
    (pc[I]: l1) 
    (requesting[I]: F) 
    => (pc[I]: l2) 
       (requesting[I]: true) .
--- checkPriv
  rl [checkPriv] :
    (pc[I]: l2) 
    (havePriv[I]: F)
    => (pc[I]: (if F then cs else l3 fi)) 
       (havePriv[I]: F) .
--- incRecNo
  rl [incRecNo] :
    (pc[I]: l3) 
    (rn[I]: RN) 
    (idx[I]: X) 
    => (pc[I]: l4) 
       (rn[I]: RN[I] := (RN[I]) + 1)
       (idx[I]: 1) .
--- sendReq
  rl [sendReq] :
    (pc[I]: l4) 
    (idx[I]: X) 
    (rn[I]: RN) 
    (nw: NW)
    => (pc[I]: if X == N then l5 else l4 fi)
       (idx[I]: if X == N then 1 else X + 1 fi) 
       (rn[I]: RN) 
       (nw: (if X == I then NW else msg(X,req(I,RN[I])) NW fi)) .
  --- waitPriv
  rl [waitPriv] :
    (pc[I]: l5)
    (havePriv[I]: F)
    (ln[I]: LN')
    (queue[I]: Q')
    (nw: (msg(I,priv(Q,LN)) NW))
    => (pc[I]: cs)
       (havePriv[I]: true)
       (ln[I]: LN)
       (queue[I]: Q)
       (nw: NW) .
  --- exit
  rl [exit] :
    (pc[I]: cs)
    => (pc[I]: l6) .
  --- completeReq
  rl [completeReq] :
    (pc[I]: l6)
    (rn[I]: RN)
    (ln[I]: LN)
    (idx[I]: X)
    => (pc[I]: l7)
       (rn[I]: RN)
       (ln[I]: LN[I] := RN[I])
       (idx[I]: 1) .
  --- updateQueue
  rl [updateQueue] :
    (pc[I]: l7)
    (idx[I]: X)
    (rn[I]: RN)
    (ln[I]: LN)
    (queue[I]: Q)
    => (pc[I]: if X == N then l8 else l7 fi)
       (idx[I]: if X == N then 1 else X + 1 fi)
       (rn[I]: RN)
       (ln[I]: LN)
       (queue[I]: if X =/= I and not(X \in Q) and (RN[X] == (LN[X]) + 1)
                  then put(Q,X)
                  else Q
                  fi) .
  --- checkQueue
  rl [checkQueue] :
    (pc[I]: l8)
    (queue[I]: Q)
    => (pc[I]: if empty?(Q) then l10 else l9 fi)
       (queue[I]: Q) .
  --- transferPriv
  rl [transferPriv] :
    (pc[I]: l9)
    (havePriv[I]: F)
    (ln[I]: LN)
    (queue[I]: Q)
    (nw: NW)
    => (pc[I]: l10)
       (havePriv[I]: false)
       (ln[I]: LN)
       (queue[I]: Q)
       (nw: (msg(top(Q),priv(get(Q),LN)) NW)) .
  --- resetReq
  rl [resetReq] :
    (pc[I]: l10)
    (requesting[I]: F)
    => (pc[I]: rem)
       (requesting[I]: false) .
  --- receiveReq
  crl [receiveReq] :
    (pc[I]: L)
    (requesting[I]: F)
    (havePriv[I]: F')
    (rn[I]: RN)
    (ln[I]: LN)
    (queue[I]: Q)
    (nw: (msg(I,req(J,X)) NW))
    => (pc[I]: L)
       (requesting[I]: F)
       (havePriv[I]: if C then false else F' fi)
       (rn[I]: RN[J] := Max)
       (ln[I]: LN)
       (queue[I]: Q)
       (nw: if C then (msg(J,priv(Q,LN)) NW) else NW fi)
    if I =/= J /\ L =/= l10 /\ 
       Max := if (RN[J]) < X then X else RN[J] fi /\
       C := F' and not(F) and Max == (LN[J]) + 1 .
endm

in model-checker .

mod SK-PREDS is
  pr SK .
  inc SATISFACTION .
  subsort Sys < State .
  op wait : Nat -> Prop .
  op crit : Nat -> Prop .
  op existPriv : Nat -> Prop .
  op existReq : Nat Nat -> Prop .
  vars I J : NodeID .
  var S : Sys .
  var P : Privilege .
  var X : Nat .
  var NW : Network .
  var PR : Prop .
  eq (pc[I]: l5) S |= wait(I) = true .
  eq (pc[I]: cs) S |= crit(I) = true .
  eq (nw: (msg(I,P) NW)) S |= existPriv(I) = true .
  eq (nw: (msg(I,req(J,X)) NW)) S |= existReq(I,J) = true .
  eq S |= PR = false [owise] .
endm

mod SK-CHECK is
  pr SK-PREDS .
  inc MODEL-CHECKER .
  inc LTL-SIMPLIFIER .
--- initial states
  op node : Nat -> Sys .
  op init : -> Sys .
  var I : NodeID .
  eq node(I) = (numOfReq[I]: 0)
               (pc[I]: rem)
               (requesting[I]: false)
               (havePriv[I]: (I == 1))
               (rn[I]: ia) 
               (ln[I]: ia)
               (queue[I]: empty)
               (idx[I]: 1) .
  eq init = node(1) node(2) (nw: void) .
--- properties
  op mutex : -> Formula .
  op lofree : -> Formula .
  op fairness : -> Formula .
  eq mutex = [] ~(crit(1) /\ crit(2)) .
  eq lofree = (wait(1) |-> crit(1)) /\ (wait(2) |-> crit(2)) .
  eq fairness = (existPriv(1) |-> ~(existPriv(1))) /\ 
                (existReq(1,2) |-> ~(existReq(1,2))) /\ 
                (existPriv(2) |-> ~(existPriv(2))) /\ 
                (existReq(2,1) |-> ~(existReq(2,1))) .
endm

eof --- tells Maude that the rest of the file is ignored.

--- Checking no deadlock states.
search [1] in SK-CHECK : init =>! S:Sys .

--- Checking the mutual exclusion property.
red in SK-CHECK : modelCheck(init,mutex) .

-- Checking the lockout freedom property.
red in SK-CHECK : modelCheck(init,(fairness -> lofree)) .