-- ==========================================================
--> file: qlock.cafe
-- ==========================================================

--> LABELconst
mod! LABELconst {
 [LabelConst]
 ops rm wt cs : -> LabelConst {constr}
 
-- equality over LabelConst
 op _=_ : LabelConst LabelConst -> Bool {comm}
 vars Lc1 Lc2 : LabelConst
 eq (Lc1 = Lc1) = true .
 ceq Lc1 = Lc2 if Lc1 = Lc2 .
--
 eq (Lc1 = Lc2) = (Lc1 == Lc2) .
-- This equation is the abbreviation of the following three
-- equations:
--  eq (rm = wt) = false .
--  eq (rm = cs) = false .
--  eq (wt = cs) = false .

-- We suppose that we will not declare any more operators whose
-- sort is LabelConst even when we write proof scores.
-- 
}

--> LABEL
mod* LABEL {
 pr(LABELconst)
 [LabelConst < Label]
--
-- We may declare operators whose sort is Label.
--
 op _=_ : Label Label -> Bool {comm}
 vars L1 L2 : Label
 eq (L1 = L1) = true .
 ceq L1 = L2 if L1 = L2 .
}

--> PID
-- generic set of objects with constants and errors
mod* PID {
 [PidConst < Pid,  Pid Err < PidErr]
-- equality over PidErr
 op _=_ : PidErr PidErr -> Bool {comm}
 vars Pe1 Pe2 : PidErr
 eq (Pe1 = Pe1) = true .
 ceq Pe1 = Pe2 if Pe1 = Pe2 .
-- equality over constants
 vars Pc1 Pc2 : PidConst
 eq (Pc1 = Pc2) = (Pc1 == Pc2) .
-- error declaration
 var P : Pid
 var E : Err
 eq (E = P) = false .
}

--> TRIV=
-- generic set of objects with constants and errors
mod* TRIV= {
 [EltConst < Elt, Elt Err < EltErr]
--
 op _=_ : EltErr EltErr -> Bool {comm}
 vars Ee1 Ee2 : EltErr
 eq (Ee1 = Ee1) = true .
 ceq Ee1 = Ee2 if Ee1 = Ee2 .
--
 vars Ec1 Ec2 : EltConst
 eq (Ec1 = Ec2) = (Ec1 == Ec2) .
--
 var El : Elt
 var Er : Err
 eq (Er = El) = false .
}

--> QUEUE
mod! QUEUE (D :: TRIV=) {
 [Empty NeQueue < Queue, Queue Err < Qerr]

 -- constructors of Queue
 op empty :             -> Empty {constr}
 op _,_   : Queue Elt.D -> NeQueue {constr}

 -- equality over QueueErr
 op _=_ : Qerr Qerr -> Bool {comm}
 eq (Qe:Qerr = Qe) = true .
 ceq Qe1:Qerr = Qe2:Qerr if Qe1 = Qe2 .
 --
 eq (empty = Q1:Queue , X:Elt.D) = false .
 eq (Q1:Queue , X:Elt.D = Q2:Queue , Y:Elt.D) 
              = (Q1 = Q2) and (X = Y) .
 -- error declaration
 eq (Er:Err.QUEUE = Q:Queue) = false .

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

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

 -- get
 op get : Queue -> Qerr
 op get : NeQueue -> Queue
 op get : Empty -> Err.QUEUE
 op get : Err.QUEUE -> Err.QUEUE
 eq get((Q,X)) = Q .

 -- top
 op top : Queue -> EltErr.D
 op top : NeQueue -> Elt.D
 op top : Empty -> Err.D
 op top : Err.QUEUE -> Err.D
 op top : Qerr -> EltErr.D
 eq top((Q,X)) = X .

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

-- (_ in _)
  pred (_in_) : Elt.D Queue 
  eq (X in empty) = false .
  eq (X in (Q,Y)) = ((X = Y) or (X in Q)) .

}

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

 -- state space of QLOCK
 [Sys]

 -- observations
 op pc    : Sys Pid -> Label
 op queue : Sys -> Queue

 -- initial state of QLOCK
 op init : -> Sys {constr}
 -- actions
 op want : Sys Pid -> Sys {constr}
 op try  : Sys Pid -> Sys {constr}
 op exit : Sys Pid -> Sys {constr}

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

-- ==========================================================