-- ==========================================================
--> cafeobj codes for lecture06 of i613-0912
-- ==========================================================

--> LABEL
mod! LABEL {
  -- EQL is a meta module 
  -- and is imported for making _=_ predicate available
  -- by including EQL
  -- including does not have any semantic intention
  inc(EQL) 

  [LabelConst < Label]
  ops rm wt cs : -> LabelConst {constr}
  vars Lc1 Lc2 : LabelConst
  eq (Lc1 = Lc2) = (Lc1 == Lc2) .
}

-- test for LABEL
open LABEL
red (rm = rm) .
red (wt = wt) .
red (cs = cs) .

red (rm = wt) .
red (rm = cs) .
red (wt = cs) .

ops l1 l2 : -> Label .
red (rm = l1) .
red (l1 = l1) .
red (l1 = l2) .
close

--> PID
mod* PID {
  inc(EQL) 
  [PidConst < Pid < PidErr]
  vars Pc1 Pc2 : PidConst
  eq (Pc1 = Pc2) = (Pc1 == Pc2) .
}

-- test for PID
open PID
ops pc1 pc2 : -> PidConst .
red (pc1 = pc1) .
red (pc2 = pc2) .
red (pc1 = pc2) .

ops p1 p2 : -> Pid .
red (p1 = p1) .
red (p1 = p2) .
red (pc1 = p1) .
close

--> TRIV=
mod* TRIV= {
  inc(EQL) 
  [EltConst < Elt < EltErr]
}

--> QUEUE
mod! QUEUE (D :: TRIV=) {
  inc(EQL) 
  -- EQL needs not be imported because
  -- it is already imported by (D :: TRIV=)

  -- sort Queue and its constructors
  [Queue < QueueErr]
  op empty :             -> Queue {constr}
  op _,_   : Queue Elt.D -> Queue {constr}

  -- equality over Queue
  eq (empty = empty) = true .
  eq (Q1:Queue,E1:Elt = Q2:Queue,E2:Elt) = (Q1 = Q2) and (E1 = E2) .

  -- CafeOBJ variables
  var Q : Queue 
  vars X Y : Elt.D

-- put
  op put : EltErr.D QueueErr -> QueueErr
  op put : Elt.D Queue -> Queue
  eq put(X,empty) = empty,X .
  eq put(X,(Q,Y)) = put(X,Q),Y .

-- get
  op get : QueueErr -> QueueErr
  eq get((Q,X)) = Q .
  eq (get(empty) = Q:Queue) = false .

-- top
  op top : QueueErr -> EltErr.D
  eq top((Q,X)) = X .
  eq (top(empty) = E:Elt.D) = false .

-- empty?
  op empty? : QueueErr -> Bool
  eq empty?(empty) = true .
  eq empty?((Q,X)) = false .
}

open QUEUE
op q : -> Queue .
op e : -> Elt .

red get(empty) = q .
red top(empty) = e .
close

--> QLOCK
mod* QLOCK {
  inc(LABEL)
  inc(QUEUE(PID{sort Elt -> Pid,
               sort EltConst -> PidConst,
               sort EltErr -> PidErr}))

-- state space of QLOCK
  *[Sys]*

-- initial state of QLOCK
  op init : -> Sys {constr}
-- actions
  bop want : Sys Pid -> Sys {constr}
  bop try  : Sys Pid -> Sys {constr}
  bop exit : Sys Pid -> Sys {constr}
-- observations
  bop pc    : Sys Pid -> Label
  bop queue : Sys -> Queue

-- initial state
  eq pc(init,I:Pid)  = rm .
  eq queue(init) = empty .

-- CafeOBJ variables
  var S : Sys
  vars I J : Pid
  
-- want
  op c-want : Sys Pid -> Bool
  eq c-want(S,I) = (pc(S,I) = rm) .
  --
  ceq pc(want(S,I),J)  
      = (if I = J then wt else pc(S,J) fi) if c-want(S,I) .
  ceq queue(want(S,I)) = put(I,queue(S))   if c-want(S,I) .
  ceq want(S,I)        = S                 if not c-want(S,I) .

-- try
  op c-try : Sys Pid -> Bool
  eq c-try(S,I) = (pc(S,I) = wt 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) .

-- 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 rm 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) .
}