(mod! LABEL{
  
  [Label]

  ops rm cs wt : -> Label {constr} .
  op  _=_ : Label Label -> Bool .

  vars Lc1 Lc2 : Label .

  eq (Lc1 = Lc2 ) = true .

})

(
mod* PID {

  [Pid]
  
  vars Pc1 Pc2 : Pid .
  op _=_ : Pid Pid -> Bool .
  
  eq (Pc1 = Pc1) = true .
})

(mod! QUEUE {

  inc(PID) 

  [Queue]

  vars Q1 Q2 : Queue . 
  vars X Y : Pid .
  vars P1 P2 : Pid .
  
 
  op empty : -> Queue {constr} .
  op _;_ : Queue Pid -> Queue {constr} .
  op _=_ : Queue Queue -> Bool .

  eq (empty = empty) = true .
  eq (Q1 ; P1 = Q2 ; P2) = ((Q1 = Q2) and (P1 = P2)) .

  var Q : Queue .
  

  op put : Pid Queue -> Queue .
  eq put(X, empty) = (empty ; X) .
  eq put(X, (Q ; Y)) = (put(X, Q) ; Y) .


  op get : Queue -> Queue .

  eq get((Q ; X)) = Q .
  

  op top : Queue -> Pid .
  eq top((Q ; X)) = X .
  

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

(mod* QLOCK {
  inc(LABEL)
  inc(QUEUE)

  *[Sys]*

  op init : -> Sys {constr} .
  ops p q : -> Pid .
  
  bop want : Sys Pid -> Sys {constr} .
  bop try  : Sys Pid -> Sys {constr} .
  bop exit : Sys Pid -> Sys {constr} .

  bop pc : Sys Pid -> Label  .  
  bop queue : Sys -> Queue .


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


  var S : Sys .
  vars I J : Pid .
  

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


  op c-try : Sys Pid -> Bool .
  eq c-try(S,I) = (pc(S,I) = wt) .

  ceq pc(try(S,I), J) = 
  	  if I = J then cs else pc(S,J) fi if c-try(S,I) .
  ceq queue(try(S,I)) = queue(S) if c-try(S,I) .
  ceq try(S, I)       = S     if not c-try(S,I)  .

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