--
-- Qlock: a mutual exclustion protocol
-- based on an atomic queue and an abstract
-- version of the Dijkstra's binary semaphore
-- 
-- PidQueue queue = empty;
-- ...
-- Loop: Remainder Section
--  rs: enq(queue,i);
--  ws: repeat until top(queue) = i;
--    Critical Section
--  cs: deq(queue);
--
-- Note that queue is an atomic queue,
-- where enq, top and deq are atomic, and
-- queue is used in neither Remainder Section
-- nor Critical Section.
--

mod! LABEL {
  [Label]
  ops rs ws cs : -> Label {constr}
  eq (rs = ws) = false .
  eq (rs = cs) = false .
  eq (ws = cs) = false .
}

mod* PID {
  [ErrPid Pid < Pid&Err]
  op none : -> ErrPid
  var I : Pid
  var EI : ErrPid
  eq (I = EI) = false .
}

mod* TRIVerr {
  [ErrElt Elt < Elt&Err]
  op err : -> ErrElt
}

mod! QUEUE(E :: TRIVerr) {
  [EQueue NeQueue < Queue]
  op empty :             -> EQueue {constr}
  op __   : Elt.E Queue -> NeQueue {constr}
  op enq : Queue Elt.E -> NeQueue
  op deq : Queue -> Queue
  op top : EQueue -> ErrElt.E
  op top : NeQueue -> Elt.E
  op top : Queue -> Elt&Err.E
  op _\in_ : Elt Queue -> Bool
  op del : Queue Elt.E -> Queue
  var Q : Queue
  vars X Y : Elt.E
  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) = err.E .
  eq top(X Q) = X .
  eq X \in empty = false .
  eq X \in (Y Q) = (if X = Y then true else X \in Q fi) .
  eq del(empty,Y) = empty .
  eq del(X Q,Y) = (if X = Y then Q else X del(Q,Y) fi) .
  -- Lemmas
  eq X \in enq(Q,Y) = (if X = Y then true else X \in Q fi) .
  ceq X \in del(enq(Q,X),X) = false if not X \in Q .
  ceq X \in del(enq(Q,Y),X) = X \in del(Q,X) if not X = Y .
  ceq X \in del(Q,X) = false if not X \in Q .
}

view TRIVerr2PID from TRIVerr to PID {
  sort Elt -> Pid,
  sort ErrElt -> ErrPid,
  sort Elt&Err -> Pid&Err,
  op err -> none,
}

mod* QLOCK {
  pr(LABEL + PID)
  pr(QUEUE(E <= TRIVerr2PID))
  [Sys]
-- any initial state
  op init : -> Sys {constr}
-- transitions
  op want : Sys Pid -> Sys {constr}
  op try  : Sys Pid -> Sys {constr}
  op exit : Sys Pid -> Sys {constr}
-- observations
  op pc    : Sys Pid -> Label
  op queue : Sys -> Queue
-- CafeOBJ variables
  var S : Sys
  vars I J : Pid
  var Q : Queue
-- for any initial state
  eq pc(init,I)  = rs .
  eq queue(init) = empty .
-- for want
  op c-want : Sys Pid -> Bool
  eq c-want(S,I) = (pc(S,I) = rs) .
  --
  ceq pc(want(S,I),J)  = (if I = J then ws else pc(S,J) fi) if c-want(S,I) .
  ceq queue(want(S,I)) = enq(queue(S),I)                    if c-want(S,I) .
  ceq want(S,I)        = S                                  if not c-want(S,I) .
-- for try
  op c-try : Sys Pid -> Bool
  eq c-try(S,I) = (pc(S,I) = ws and top(queue(S)) = I) .
  --
  ceq pc(try(S,I),J)  = (if I = J then cs else pc(S,J) fi) if c-try(S,I) .
  eq  queue(try(S,I)) = queue(S) .
  ceq try(S,I)        = S                                  if not c-try(S,I) .
-- for exit
  op c-exit : Sys Pid -> Bool
  eq c-exit(S,I) = (pc(S,I) = cs) .
  -- 
  ceq pc(exit(S,I),J)  = (if I = J then rs else pc(S,J) fi) if c-exit(S,I) .
  ceq queue(exit(S,I)) = deq(queue(S))                      if c-exit(S,I) .
  ceq exit(S,I)        = S                                  if not c-exit(S,I) .
--
-- Properties to prove
--
  op inv1 : Sys Pid Pid -> Bool
  op inv2 : Sys Pid -> Bool
  op inv3 : Sys Pid -> Bool
  op inv4 : Sys Pid -> Bool
  op inv5 : Sys Pid -> Bool
  op inv6 : Sys Pid -> Bool
  op inv7 : Sys Pid -> Bool
  -- op inv7 : Sys Pid Queue -> Bool
  eq inv1(S,I,J)
     = ((pc(S,I) = cs and pc(S,J) = cs) implies I = J) .
  eq inv2(S,I) = (pc(S,I) = cs implies top(queue(S)) = I) .
  eq inv3(S,I) = (pc(S,I) = rs implies (not I \in queue(S))) .
  eq inv4(S,I) = ((not I \in queue(S)) implies pc(S,I) = rs) .
  eq inv5(S,I) = (pc(S,I) = ws or pc(S,I) = cs implies I \in queue(S)) .
  eq inv6(S,I) = (I \in queue(S) implies pc(S,I) = ws or pc(S,I) = cs) .
  -- eq inv7(S,I,Q) = (pc(S,I) = cs implies queue(S) = I Q and (not I \in Q)) .
  eq inv7(S,I) = (not I \in del(queue(S),I)) .
}