***
*** Qlock:
***
*** Loop {
***      Remainder Section
***  rs: atomic_enqueue(queue,i);
***  ws: repeat until top(queue) = i;
***      Critical Section
***  cs: atomic_dequeue(queue);
*** }
***
*** Initially, queue is empty,
***  and each process is at label rs.
***

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 Trans Obs Sys .
  subsorts Trans Obs < Sys .
*** Configurations
  op void : -> Sys .
  op _ _ : Sys Sys -> Sys [assoc comm id: void] .
*** Observers
  op pc[_]:_ : Pid Label -> Obs .
  op queue:_ : Queue -> Obs .
*** Transitions
*** Maude variables
  vars Q R : Queue .
  var I : Pid .
*** Rules
  rl  [want] : (pc[I]: rs) (queue: Q) => (pc[I]: ws) (queue: enq(Q,I)) .
  crl [try]  : (pc[I]: ws) (queue: Q) => (pc[I]: cs) (queue: Q) if top(Q) = I .
  rl  [exit] : (pc[I]: cs) (queue: Q) => (pc[I]: rs) (queue: deq(Q)) .
endm

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

***
*** search [1] in QLOCK-INIT : init
***   =>* (pc[I:Pid]: L1:Label) (pc[J:Pid]: L2:Label) (S:Sys)
***   such that not(L1:Label == cs and L2:Label == cs implies I:Pid == J:Pid) .
***
*** search [1] in QLOCK-INIT : init =>* (pc[I:Pid]: cs) (pc[J:Pid]: cs) (S:Sys)
***   such that not(I:Pid == J:Pid) .
***
*** search [1] in QLOCK-INIT : init =>* (pc[p1]: cs) (pc[p2]: cs) (S:Sys)
***   such that not(p1 == p2) .
***
*** search [1] in QLOCK-INIT : init =>* (pc[p1]: cs) (pc[p2]: cs) (S:Sys) .
***


***
*** Ticket0:
***
*** Loop {
***      Remainder Section
***  rs: ticket[i] := vm;
***  is: vm := vm + 1;
***  ws: repeat until ticket[i] = turn;
***      Critical Section
***  cs: turn := turn + 1;
*** }
***
*** Initially, vm, turn, and ticket[i] are 0 for each i.
*** and each process is at label rs.
***

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

fmod PID is
  sort Pid .
  ops p1 p2 : -> Pid .
endfm

mod TICKET is
  pr LABEL .
  pr PID .
  pr NAT .
  sorts Trans Obs Sys .
  subsorts Trans Obs < Sys .
*** Configurations
  op void : -> Sys .
  op _ _ : Sys Sys -> Sys [assoc comm id: void] .
*** Observers
  op vm:_ : Nat -> Obs .
  op turn:_ : Nat -> Obs .
  op ticket[_]:_ : Pid Nat -> Obs .
  op pc[_]:_ : Pid Label -> Obs .
*** Transitions
*** Maude variables
  var I : Pid .
  vars X N : Nat .
*** Rules
  rl [get]  : (pc[I]: rs) (ticket[I]: X) (vm: N)
              => (pc[I]: is) (ticket[I]: N) (vm: N) .
  rl [inc]  : (pc[I]: is) (vm: N)  => (pc[I]: ws) (vm: (N + 1)) .
  rl [try]  : (pc[I]: ws) (ticket[I]: N) (turn: N)
              => (pc[I]: cs) (ticket[I]: N) (turn: N) .
  rl [exit] : (pc[I]: cs) (turn: N)  => (pc[I]: rs) (turn: (N + 1)) .
endm

mod TICKET-INIT is
  pr TICKET .
  op init : -> Sys .
  eq init = (pc[p1]: rs) (ticket[p1]: 0) (pc[p2]: rs) (ticket[p2]: 0)
            (vm: 0) (turn: 0) .
endm

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


***
*** Ticket1:
***
*** Loop {
***      Remainder Section
***  rs: ticket[i] := vm + 1;
***  ws: repeat until ticket[i] = turn;
***      Critical Section
***  cs: turn := turn + 1;
*** }
***
*** Initially, vm, turn, and ticket[i] are 0 for each i.
*** and each process is at label rs.
***

mod TICKET1 is
  pr LABEL .
  pr PID .
  pr NAT .
  sorts Trans Obs Sys .
  subsorts Trans Obs < Sys .
*** Configurations
  op void : -> Sys .
  op _ _ : Sys Sys -> Sys [assoc comm id: void] .
*** Observers
  op vm:_ : Nat -> Obs .
  op turn:_ : Nat -> Obs .
  op ticket[_]:_ : Pid Nat -> Obs .
  op pc[_]:_ : Pid Label -> Obs .
*** Transitions
*** Maude variables
  var I : Pid .
  vars X N : Nat .
*** Rules
  rl [get]  : (pc[I]: rs) (ticket[I]: X) (vm: N)
              => (pc[I]: ws) (ticket[I]: N) (vm: (N + 1)) .
  rl [try]  : (pc[I]: ws) (ticket[I]: N) (turn: N)
              => (pc[I]: cs) (ticket[I]: N) (turn: N) .
  rl [exit] : (pc[I]: cs) (turn: N)  => (pc[I]: rs) (turn: (N + 1)) .
endm

mod TICKET1-INIT is
  pr TICKET1 .
  op init : -> Sys .
  eq init = (pc[p1]: rs) (ticket[p1]: 0) (pc[p2]: rs) (ticket[p2]: 0)
            (vm: 0) (turn: 0) .
endm

***
*** search [1] in TICKET1-INIT : init =>* (pc[p1]: cs) (pc[p2]: cs) (S:Sys) .
*** Does not terminate.
***
*** search [1,10] in TICKET1-INIT : init =>* (pc[p1]: cs) (pc[p2]: cs) (S:Sys) .
***