--
-- Mutual Exclusion Algorithm using Queue
--
-- We write a program called QLOCK that allows at most one process to
-- execute the critical section at any given time. 
-- QLOCK uses a queue where processes wait for entering the critical
-- section.  
-- all operations of the queue are supposed to be atomic.
--
--   - put(queue,i) atomically puts process i into the queue at the end.
--   - get(queue)   atomically deletes the top process of the queue if any.
--   - top(queue)   atomically returns the top process of the queue if any.
--
-- The queue is initially empty.
--
-- QLOCK is as follows:
--
--   l1: put(queue,i);
--   l2: if (i != top(queue)) goto l2;
--       Critical Section
--   cs: get(queue);
--
-- The formal model of the program:
--   - Three transition rules are used.
--     * 'want_i' corresponds to 'put(queue,i)'.
--     * 'try_i'  corresponds to 'if (i != top(queue)) goto l2'.
--     * 'exit_i' corresponds to 'get(queue)'.
--   - Two observable values are used.
--     * 'queue' denotes the queue.
--     * 'pc_i'   indicates where process i is at.
--
-- In the formal model, we use three kinds of data types: lables,
-- process IDs and queues.
-- If we prove QLOCK mutually exclusive, we need lemmas on queues.
-- Here we take a careful look at module QUEUE where queues are
-- defined. 
--

mod! LABEL {
  [Label]
  ops l1 l2 cs : -> Label
  op _=_ : Label Label -> Bool {comm}
  var L : Label
  eq (L = L) = true .
  eq (l1 = l2) = false .
  eq (l1 = cs) = false .
  eq (l2 = cs) = false .
}

mod* PID {
  [Pid]
  op _=_ : Pid Pid -> Bool {comm}
  var I : Pid
  eq (I = I) = true .
}

--
-- Instead of queues of a specific data type, queues of an any data
-- type is defined. 
-- Therefore, we use a parameterized module to define such generic
-- queues. 
-- First module EQTRIV that is used as a formal parameter of the
-- parameterized module.
-- EQTRIV declares that an actual parameter with which the
-- parametrized module is instantiated should have one visible sort
-- and operator _=_.
--
mod* EQTRIV {
  [Elt]
  op _=_ : Elt Elt -> Bool {comm}
}

--
-- Then, the parameterized module for generic queues can be declared.
--
mod! QUEUE (D :: EQTRIV) {
  [Queue]
-- constructors
  op empty :            -> Queue
  op __   : Elt.D Queue -> Queue
-- operators
  op put : Queue Elt.D -> Queue
  op get : Queue -> Queue
  op top : Queue -> Elt.D
  op empty? : Queue -> Bool
  op _\in_ : Elt.D Queue -> Bool
-- CafeOBJ variables
  var Q : Queue
  vars X Y : Elt.D
-- equations
  eq put(empty,X) = X empty .
  eq put((Y Q),X) = Y put(Q,X) .
  eq get(empty) = empty .
  eq get((X Q)) = Q .
  eq top((X Q)) = X .
  eq empty?(empty) = true .
  eq empty?((X Q)) = false .
  eq X \in empty = false .
  eq X \in (X Q) = true .
  ceq X \in (Y Q) = X \in Q if not(X = Y) .
--
-- The following equations are needed for the verification that QLOCK
-- is mutually exclusive.
-- The equations can be deduced from the above equations.
-- You can find the proofs in queue.mod.
--
  -- used in proof2.mod
  ceq (top(put(Q,Y)) = X) = true if not empty?(Q) and top(Q) = X .
  -- used in proof3.mod
  eq empty?(put(Q,X)) = false .
  ceq X \in Q = false if empty?(Q) .
  -- used in proof4.mod
  eq X \in put(Q,X) = true .
  ceq X \in put(Q,Y) = true if X \in Q .
}

mod* QLOCK {
  pr(LABEL + PID)
  pr(QUEUE(PID))
  *[Sys]*
-- any initial state
  op init : -> Sys
-- observations
  bop pc    : Sys Pid -> Label
  bop queue : Sys -> Queue
-- actions
  bop want : Sys Pid -> Sys
  bop try  : Sys Pid -> Sys
  bop exit : Sys Pid -> Sys
-- CafeOBJ variables
  var S : Sys
  vars I J : Pid
-- for any initial state
  eq pc(init,I)  = l1 .
  eq queue(init) = empty .
-- for want
  op c-want : Sys Pid -> Bool
  eq c-want(S,I) = (pc(S,I) = l1) .
  --
  ceq pc(want(S,I),J)  = (if I = J then l2 else pc(S,J) fi) if c-want(S,I) .
  ceq queue(want(S,I)) = put(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) = l2 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 l1 else pc(S,J) fi) if c-exit(S,I) .
  ceq queue(exit(S,I)) = get(queue(S))                      if c-exit(S,I) .
  ceq exit(S,I)        = S                                  if not c-exit(S,I) .
}