fmod LABELS is sort Labels . ops rm wt cs : -> Labels [ctor]. op _~_ : Labels Labels -> Bool [comm]. var L : Labels . eq L ~ L = true . eq (rm ~ wt) = false . eq (rm ~ cs) = false . eq (wt ~ cs) = false . --- ceq true = false if rm = wt . ceq true = false if rm = cs . ceq true = false if wt = cs . endfm fth PID is inc BOOL . sort Pid . op _~_ : Pid Pid -> Bool [comm]. vars I J : Pid . eq I ~ I = true . ceq I = J if I ~ J [nonexec]. endfth fmod SEQUENCE{X :: PID} is sort Sequence . subsorts X$Pid < Sequence . --- constructors op empty : -> Sequence [ctor] . op _`,_ : Sequence Sequence -> Sequence [ctor id: empty assoc]. vars Q Q' : Sequence . var I : X$Pid . --- op top : Sequence -> X$Pid . eq top(empty) = empty . eq top(I,Q) = I . --- op get : Sequence -> Sequence . eq get(empty) = empty . eq get(I,Q) = Q . --- ceq true = false if Q,I,Q' := empty . ceq [lemma-top]: top(Q,I) = top(Q) if top(Q) :: X$Pid . endfm fmod QLOCK{X :: PID} is inc SEQUENCE{X} . inc LABELS . sort Sys . --- actions op init : -> Sys [ctor]. ops want try exit : Sys X$Pid -> Sys [ctor]. --- observers op pc : Sys X$Pid -> Labels . op sq : Sys -> Sequence . --- var S : Sys . vars I J K : X$Pid . var Q : Sequence . --- init --- eq pc(init,I) = rm . eq sq(init) = empty . --- want --- ceq pc(want(S,I),J) = wt if pc(S,I) = rm /\ J = I [metadata "CA-w1"]. ceq pc(want(S,I),J) = pc(S,J) if pc(S,I) = rm /\ J ~ I = false [metadata "CA-w2"]. ceq pc(want(S,I),J) = pc(S,J) if pc(S,I) ~ rm = false [metadata "CA-w3"]. ceq sq(want(S,I)) = sq(S),I if pc(S,I) = rm . ceq sq(want(S,I)) = sq(S) if pc(S,I) ~ rm = false . --- try --- ceq pc(try(S,I),J) = cs if pc(S,I) = wt /\ I,Q := sq(S) /\ J = I[metadata "CA-t1"]. ceq pc(try(S,I),J) = pc(S,J) if (J ~ I) = false [metadata "CA-t2"]. ceq pc(try(S,I),J) = pc(S,J) if pc(S,I) ~ wt = false [metadata "CA-t3"]. ceq pc(try(S,I),J) = pc(S,J) if top(sq(S)) ~ I = false [metadata "CA-t4"]. eq sq(try(S,I)) = sq(S) . --- exit --- ceq pc(exit(S,I),J) = rm if pc(S,I) = cs /\ J = I [metadata "CA-e1"]. ceq pc(exit(S,I),J) = pc(S,J) if pc(S,I) = cs /\ I ~ J = false [metadata "CA-e2"]. ceq pc(exit(S,I),J) = pc(S,J) if pc(S,I) ~ cs = false [metadata "CA-e3"]. ceq sq(exit(S,I)) = get(sq(S)) if pc(S,I) = cs . ceq sq(exit(S,I)) = sq(S) if pc(S,I) ~ cs = false . endfm