mod INV1 {
   inc(QLOCK)
-- declare a predicate to verify to be an invariant
   pred inv1 : Sys Pid Pid
-- CafeOBJ variables
   var S :  Sys .
   vars I J : Pid . 
-- define inv1 to be the mutual exclusion property
   eq inv1(S,I,J) 
       = (((pc(S,I) = cs) and (pc(S,J) = cs)) implies I = J) .
}