I had a lot of fun with Problem 7.7 and bikeshedded a bit on the style. I submit the following for your critique. This passes checks with ISpec as temporal invariant and A!ISpec as a property, where A is "OneBitProtocol."
------------------------- MODULE OneBitTwoProcesses -------------------------
EXTENDS Integers
(******************************************************************
--algorithm OneBit
{ variable x = [i \in {0,1} |-> FALSE] ;
fair process (Proc \in {0,1})
{ ncs: while (TRUE)
\* This is the model for my non-critical processing.
{ skip ;
\* Ok, I'm done with that and I want in to the
\* critical section!
e1: x[self] := TRUE ;
e2: if (~x[1-self])
\* If the other guy isn't in, I'm in!
{ cs: skip (* Model for my critical code! *) }
else
\* Oops, the other guy is in. What do I do?
{ if (self = 0)
\* If I'm process 0, I'll keep trying.
{ goto e2 }
\* But, if I'm process 1, I'll be the nice guy;
\* I'll stop trying and spin while process 0 is in.
else
{ e3: x[1] := FALSE ;
e4: while ( x[0] )
{ skip (* spin *) } ;
goto e1
} } ;
\* Ok, I'm done. I don't need the critical section now.
f: x[self] := FALSE
} } }
******************************************************************)
\* BEGIN TRANSLATION
\* END TRANSLATION
PC0Labels == {"ncs", "f", "e1", "e2", "cs"}
ExtraLabels == {"e3", "e4"}
PC1Labels == PC0Labels \cup ExtraLabels
TypeOK == /\ pc \in [{0} -> PC0Labels] \cup [{1} -> PC1Labels]
/\ x \in [{0, 1} -> BOOLEAN]
InCS(i) == pc[i] = "cs"
MutualExclusion == ~(InCS(0) /\ InCS(1))
Fairness == \A i \in {0,1} : WF_vars(Proc(i))
Coordination == \A i \in {0,1} : InCS(i) \/ (pc[i] = "e2") => x[i]
Trying(i) == pc[i] \in {"e1", "e2"}
DeadlockFreedom == (Trying(0) \/ Trying(1)) ~> (InCS(0) \/ InCS(1))
Inv == /\ Init
/\ TypeOK
/\ MutualExclusion
/\ Fairness
/\ Coordination
/\ DeadlockFreedom
ISpec == Inv /\ [][Next]_<<x, pc>>
(* This algorithm implements the OneBitProtocol under the following
refinement mapping; check "ISpec" in module "OneBitProtocol." *)
A == INSTANCE OneBitProtocol
WITH pc <- [i \in {0, 1} |->
IF pc[i] \in {"ncs", "f", "e3", "e4"} THEN "r" ELSE pc[i]]