***
*** 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 [ctor] .
endfm

fmod PID is
  sorts Pid DummyPid Pid&Dummy .
  subsorts Pid < Pid&Dummy .
  subsorts DummyPid < Pid&Dummy .
  ops p1 p2 p3 p4 p5 : -> Pid [ctor] .
  op dummy : -> DummyPid [ctor ] .
endfm

fmod  QUEUE is
  pr PID .
  pr NAT .
  sort Queue .
  op empty : -> Queue [ctor] .
  op __ : Pid Queue -> Queue [ctor] .
  op _\in_ : Pid Queue -> Bool .
  op enq : Queue Pid -> Queue .
  op top : Queue -> Pid&Dummy .
  op deq : Queue -> Queue .
  op del : Queue Pid -> Queue .
  var Q : Queue .
  vars X Y : Pid .
  eq X \in empty = false .
  eq X \in (Y Q) = (X == Y) or (X \in Q) .
  eq enq(empty,X) = X empty .
  eq enq((Y Q),X) = Y enq(Q,X) .
  eq top(empty) = dummy .
  eq top((X Q)) = X .
  eq deq(empty) = empty .
  eq deq((X Q)) = Q .
  eq del(empty,Y) = empty .
  eq del(X Q,Y) = (if X == Y then Q else X del(Q,Y) fi) .
endfm

mod QLOCK is
  pr LABEL .
  pr PID .
  pr QUEUE .
  sorts OComp Sys Config .
  subsorts OComp < Sys .
*** Configurations
  op void : -> Sys [ctor] .
  op __ : Sys Sys -> Sys [ctor assoc comm id: void] .
  op {_} : Sys -> Config [ctor] .
*** Variables
  op pc[_]:_ : Pid Label -> OComp [ctor] .
  op queue:_ : Queue -> OComp [ctor] .
*** Maude variables
  vars Q R : Queue .
  vars I J : Pid .
  vars L1 L2 : Label .
  var S : Sys .
*** Rules
  rl [eq] : {(pc[I]: rs) (queue: Q) S} => {(pc[I]: ws) (queue: enq(Q,I)) S} .
  rl [wt] : {(pc[I]: ws) (queue: (I Q)) S} => {(pc[I]: cs) (queue: (I Q)) S} .
  rl [dq] : {(pc[I]: cs) (queue: Q) S} => {(pc[I]: rs) (queue: deq(Q)) S} .
*** Initial state
  op init : -> Sys .
  eq init = (queue: empty) (pc[p1]: rs) (pc[p2]: rs)
            (pc[p3]: rs) (pc[p4]: rs) (pc[p5]: rs) .
endm

***(

search [1] in QLOCK : {init} =>* {(pc[I]: L1) (pc[J]: L2) S}
such that not (L1 == cs implies not (L2 == cs)) .

search [1] in QLOCK : {init} =>* {(queue: Q) (pc[I]: L1) S}
such that not (L1 == cs implies top(Q) == I) .

search [1] in QLOCK : {init} =>* {(pc[I]: L1) (queue: Q) S}
such that not (L1 == rs implies (not I \in Q)) .

search [1] in QLOCK : {init} =>* {(pc[I]: L1) (queue: Q) S}
such that not ((not I \in Q) implies L1 == rs) .

search [1] in QLOCK : {init} =>* {(pc[I]: L1) (queue: Q) S}
such that not (L1 == ws or L1 == cs implies I \in Q) .

search [1] in QLOCK : {init} =>* {(pc[I]: L1) (queue: Q) S}
such that not (I \in Q implies L1 == ws or L1 == cs) .

search [1] in QLOCK : {init} =>* {(pc[I]: L1) (queue: Q) S}
such that not (not I \in del(Q,I)) .

)