This module provides Some UNITY properties as specifications for the One Bit Protocol:We actually use a PLPC specification. Since in PLGA we do not have process class, then the using parameter is ignored.
stability J: (SYSLAB.P.root ==> ((senderReady /\ recReady ==> (x=c) /\ (y=c)) /\ (~senderReady /\ recReady ==> ~(x=c) /\ (y=c)) /\ ( senderReady /\ ~recReady ==> (x=c) /\ ~(y=c)) /\ (~senderReady /\ ~recReady ==> ~(x=c) /\ ~(y=c)))) /\ (SYSLAB.P.mid ==> senderReady) /\ (SYSLAB.P.mid ==> (( recReady ==> ~(x=c) /\ (y=c)) /\ (~recReady ==> ~(x=c) /\ ~(y=c)))) simple progress 1: J,System |-- SYSLAB.P.root /\ senderReady /\ ~recReady ensures SYSLAB.P.root /\ senderReady /\ recReady using {senderReady, recReady}