***
*** Loop {
***      Remainder Section
***  rs: tmp := enqueue(queue,i);
***  es: queue := tmp;
***  ws: repeat until top(queue) = i;
***      Critical Section
***  cs: tmp := dequeue(queue);
***  ds: queue := tmp
*** }
***
*** rs, es, ws, cs and ds stand for remainder section,  enqueuing section,
*** waiting section, critical section and dequeuing section.
***

fmod LABEL is
  sort Label .
  ops rs es ws cs ds : -> 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 .
  op tmp[_]:_ : Pid Queue -> Val .
*** Maude variables
  vars Q R : Queue .
  var I : Pid .
*** Rules (Transitions)
  rl [eq1] : (pc[I]: rs) (queue: Q) (tmp[I]: R)
     => (pc[I]: es) (queue: Q) (tmp[I]: enq(Q,I)) .
  rl [eq2] : (pc[I]: es) (queue: Q) (tmp[I]: R)
     => (pc[I]: ws) (queue: R) (tmp[I]: R) .
  crl [wt] : (pc[I]: ws) (queue: Q)
     => (pc[I]: cs) (queue: Q) if top(Q) = I .
  rl [dq1] : (pc[I]: cs) (queue: Q) (tmp[I]: R)
     => (pc[I]: ds) (queue: Q) (tmp[I]: deq(Q)) .
  rl [dq2] : (pc[I]: ds) (queue: Q) (tmp[I]: R)
     => (pc[I]: rs) (queue: R) (tmp[I]: R) .
endm

mod QLOCK-INIT is
  pr QLOCK .
  op init : -> Sys .
  eq init = (pc[p1]: rs) (pc[p2]: rs) (queue: empty) (tmp[p1]: empty) (tmp[p2]: empty) .
endm

***
*** search [1] in QLOCK-INIT : init =>* (pc[p1]: cs) (pc[p2]: cs) (S:Sys) .
*** show path 33 .
***

***
*** search [1] in QLOCK-INIT : init =>* (S:Sys) such that false .
*** Seems non-terminating.
***