| Hi Giuliano, if you look at the TLA+ produced by the PlusCal translator, you'll see that B1 == b1 l1 == /\ b1' = TRUE /\ B1 /\ ... l2 == /\ b2' = TRUE /\ b2' /\ ... The translator notices that the await statement in l2 refers to the variable b2 that has been assigned to before, and that the _expression_ b2 should therefore be translated as b2' rather than b2. However, it doesn't notice that B1 involves b1; this would require a finer syntactic analysis than what the translator appears to do. I had a quick look at the PlusCal manual and did not see a clear description of how exactly expressions are translated. (There is a sentence that says that the expressions in TLA+ are mostly like the ones in the PlusCal algorithm except for some changes, including adding primes.) I do not think that anybody ever attempted to write up a more abstract operational semantics of PlusCal than what is implemented in the PlusCal translator. Best, Stephan
|