if you look at the TLA+ produced by the PlusCal translator, you'll see that
B1 == b1
/\ b1' = TRUE
/\ b2' = TRUE
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.