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

mod! PNAT {
  [Nat]
  op 0 : -> Nat
  op s : Nat -> Nat
  op _<_ : Nat Nat -> Bool
  op _=_ : Nat Nat -> Bool {comm}
  vars X Y : Nat 
  eq 0 < 0 = false .
  eq 0 < s(X) = true .
  eq s(X) < s(Y) = X < Y .
  eq (X = X) = true .
  eq (s(X) = 0) = false .
  eq (s(X) = s(Y)) = (X = Y) .
--
  -- used in proof12.mod
  eq (s(X) = X) = false .
}

mod* EQTRIV {
  [Elt]
  op _=_ : Elt Elt -> Bool {comm}
}

mod! QUEUE(D :: EQTRIV) principal-sort Queue {
  pr(PNAT)
  [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 top : Queue -> Elt.D
  op empty? : Queue -> Bool
  op _\in_ : Elt.D Queue -> Bool
  op howmany : Queue Elt.D -> Nat
  op where : Queue Elt.D -> Nat
-- CafeOBJ variables
  var Q : Queue
  vars X Y Z : Elt.D
  var N : Nat
-- 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) .
  eq howmany(empty,Y) = 0 .
  ceq howmany((X Q),Y) = s(howmany(Q,Y)) if X = Y .
  ceq howmany((X Q),Y) = howmany(Q,Y)    if not(X = Y) .
  ceq where((X Q),Y) = 0             if X = Y .
  ceq where((X Q),Y) = s(where(Q,Y)) if not(X = Y) .
--
  -- 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 .
  -- used in proof5.mod
  ceq X \in put(Q,Y) = false if not(X \in Q) and not(X = Y) .
  ceq X \in get(Q) = false if not(X \in Q) .
  -- used in proof6.mod
  ceq (howmany(Q,X) = 0) = false if X \in Q .
  -- used in proof7.mod
  ceq howmany(put(Q,X),X) = s(0) if not(X \in Q) .
  ceq howmany(put(Q,X),Y) = howmany(Q,Y) if not(X = Y) .
  -- used in proof9.mod
  ceq (top(Q) = X) = true if X \in Q and where(Q,X) = 0 .
  -- used in proof10.mod
  ceq top(Q) \in Q = true if not empty?(Q) .
  -- used in proof12.mod
  ceq (X = top(Q)) = false if 0 < where(Q,X) .
  ceq X \in get(Q) = true if X \in Q and not(X = top(Q)) .
  ceq (where(get(Q),X) = N) = true if where(Q,X) = s(N) .
  ceq (where(Y put(Q,Z),X) = N) = true if where((Y Q),X) = N .
  ceq X \in (Y put(Q,Z)) = true if X \in (Y Q) .
  ceq (where(Q,X) = s(N)) = false if top(Q) = X .
}

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 {strat: (0 1 2)}
  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 {strat: (0 1 2)}
  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 {strat: (0 1 2)}
  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) .
}