***
*** Loop {
***      Remainder Section
***  rs: atomic_enqueue(queue,i);
***  ws: repeat until top(queue) = i;
***      Critical Section
***  cs: atomic_dequeue(queue);
*** }
***

fmod LABEL is
  sort Label .
  ops rs ws cs : -> Label .
endfm

fmod PID is
  sort Pid .
  ops p1 p2 nop : -> Pid .
  *** nop is used as a dummy ID.
endfm

fmod  QUEUE is
  pr PID .
  sort Queue .
  op empty : -> Queue .
  op __ : Pid Queue -> Queue .
  op enq : Queue Pid -> Queue .
  op deq : Queue -> Queue .
  op top : Queue -> Pid .
  var Q : Queue .
  vars X Y : Pid .
  eq enq(empty,X) = X empty .
  eq enq((Y Q),X) = Y enq(Q,X) .
  eq deq(empty) = empty .
  eq deq((X Q)) = Q .
  eq top(empty) = nop .
  eq top((X Q)) = X .
endfm

mod QLOCK is
  pr LABEL .
  pr PID .
  pr QUEUE .
  sorts Val Sys .
  subsorts Val < Sys .
*** Configurations
  op __ : Sys Sys -> Sys [assoc comm] .
*** State components
  op pc[_]:_ : Pid Label -> Val .
  op queue:_ : Queue -> Val .
*** Maude variables
  vars Q R : Queue .
  var I : Pid .
*** Rules
  rl [eq] : (pc[I]: rs) (queue: Q) => (pc[I]: ws) (queue: enq(Q,I)) .
  crl [wt] : (pc[I]: ws) (queue: Q) => (pc[I]: cs) (queue: Q) if top(Q) = I .
  rl [dq] : (pc[I]: cs) (queue: Q) => (pc[I]: rs) (queue: deq(Q)) .
endm

in model-checker .

mod QLOCK-PREDS is
  pr QLOCK .
  inc SATISFACTION .
  subsort Sys < State .
  op wait : Pid -> Prop .
  op crit : Pid -> Prop .
  var P : Pid .
  var S : Sys .
  eq (pc[P] : ws) S |= wait(P) = true .
  eq (pc[P] : cs) S |= crit(P) = true .
endm

mod QLOCK-CHECK is
  inc QLOCK-PREDS .
  inc MODEL-CHECKER .
  inc LTL-SIMPLIFIER .
  op init : -> Sys .
  ops mutex lofree : -> Formula .
  eq init = (pc[p1]: rs) (pc[p2]: rs) (queue: empty) .
  eq mutex = ([] ~(crit(p1) /\ crit(p2))) .
  eq lofree = (wait(p1) |-> crit(p1)) /\(wait(p2) |-> crit(p2)) .
endm  

*** 
*** red in QLOCK-CHECK : modelCheck(init,mutex) .
*** red in QLOCK-CHECK : modelCheck(init,lofree) .
***