***
*** 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

in model-checker .

mod QLOCK-PREDS is
  pr QLOCK .
  inc SATISFACTION .
  subsort Sys < State .
  ops (_@rs) (_@ws) (_@cs) : Pid -> Prop .
  var I : Pid .
  var S : Sys .
  var P : Prop .
  eq (pc[I]: rs) S |= (I @rs) = true .
  eq (pc[I]: ws) S |= (I @ws) = true .
  eq (pc[I]: cs) S |= (I @cs) = true .
  eq S |= P = false [owise] .
endm

mod QLOCK-CHECK is
  pr QLOCK-PREDS .
  inc MODEL-CHECKER .
  inc LTL-SIMPLIFIER .
*** Initial states  
  op init : -> Sys .
  eq init = (pc[p1]: rs) (pc[p2]: rs) (queue: empty) .
*** Properties to be checked  
  ops mutex lofree : -> Formula .
  eq mutex = [] ~((p1 @cs) /\ (p2 @cs)) .
  eq lofree = ((p1 @ws) |-> (p1 @cs)) /\((p2 @ws) |-> (p2 @cs)) .
endm  

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


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  [idle] : (pc[I]: rs) => (pc[I]: rs) .
  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-PREDS' is
  pr QLOCK' .
  inc SATISFACTION .
  subsort Sys < State .
  ops (_@rs) (_@ws) (_@cs) (_@top): Pid -> Prop .
  var I : Pid .
  var S : Sys .
  var P : Prop .
  eq (pc[I]: rs) S |= (I @rs) = true .
  eq (pc[I]: ws) S |= (I @ws) = true .
  eq (pc[I]: cs) S |= (I @cs) = true .
  eq S |= P = false [owise] .
endm

mod QLOCK-CHECK' is
  pr QLOCK-PREDS' .
  inc MODEL-CHECKER .
  inc LTL-SIMPLIFIER .
*** Initial states  
  op init : -> Sys .
  eq init = (pc[p1]: rs) (pc[p2]: rs) (queue: empty) .
*** Properties to be checked  
  ops mutex lofree fair : -> Formula .
  eq mutex = [] ~((p1 @cs) /\ (p2 @cs)) .
  eq lofree = ((p1 @ws) |-> (p1 @cs)) /\((p2 @ws) |-> (p2 @cs)) .
  eq fair = ([] <> (p1 @ws)) /\ ([] <> (p2 @ws)) .
endm  

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


***
*** 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 .
  op b[_]:_ : Pid Nat -> Obs .
*** Transitions
*** Bounds
  op Bound : -> Nat .
  eq Bound = 3 .
*** Maude variables
  var I : Pid .
  vars X N Z : Nat .
*** Rules
  rl [get]  : (pc[I]: rs) (ticket[I]: X) (b[I]: Z) (vm: N)
              => if Z < Bound
                 then (pc[I]: ws) (ticket[I]: N) (b[I]: (Z + 1)) (vm: (N + 1))
                 else (pc[I]: rs) (ticket[I]: X) (b[I]: Z) (vm: N) fi .
  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-PREDS is
  pr TICKET1 .
  inc SATISFACTION .
  subsort Sys < State .
  ops (_@rs) (_@ws) (_@cs) : Pid -> Prop .
  var I : Pid .
  var S : Sys .
  var P : Prop .
  eq (pc[I]: rs) S |= (I @rs) = true .
  eq (pc[I]: ws) S |= (I @ws) = true .
  eq (pc[I]: cs) S |= (I @cs) = true .
  eq S |= P = false [owise] .
endm

mod TICKET1-CHECK is
  pr TICKET1-PREDS .
  inc MODEL-CHECKER .
  inc LTL-SIMPLIFIER .
*** Initial states  
  op init : -> Sys .
  eq init = (pc[p1]: rs) (ticket[p1]: 0) (b[p1]: 0)
            (pc[p2]: rs) (ticket[p2]: 0) (b[p2]: 0)
            (vm: 0) (turn: 0) .
*** Properties to be checked  
  ops mutex lofree fair : -> Formula .
  eq mutex = [] ~((p1 @cs) /\ (p2 @cs)) .
  eq lofree = ((p1 @ws) |-> (p1 @cs)) /\((p2 @ws) |-> (p2 @cs)) .
  eq fair = ([] <> (p1 @ws)) /\ ([] <> (p2 @ws)) .
endm  

*** 
*** red in TICKET1-CHECK : modelCheck(init,mutex) .
*** red in TICKET1-CHECK : modelCheck(init,lofree) .
*** red in TICKET1-CHECK : modelCheck(init,fair -> lofree) .
***