While I'm reading this, I feel more and more like asking: Am I the only one that finds TLA+ much easier to read and write than PlusCal? It's an odd thing to say, with PlusCal positioned as the easier option.
Personally, if I'm not writing teaching or workshop materials, I write specs in raw TLA+. Some of that is due to fixable limitations in PlusCal, but a lot is because it's fundamentally a really elegant way of expressing specifications.
The one thing I really like about PlusCal is that variable updates don't need to be complete, so you don't have to write stuff like:
foo' = [foo EXCEPT ![i] = bar]
Mathematical notation is a concise, time tested language for enhancing thought. People should use that to their advantage. As an added advantage, unlike PlusCal, facility in the language of propositional logic generalizes widely to other tools used in formal methods, as well as other technical fields.
Objectively, PlusCal is a higher level language. So it should be easier than TLA+ right? More specifically, look at https://pastebin.com/cwZaApmH. The top half is PlusCal and bottom half (after \* BEGIN TRANSLATION) is the translated TLA+ code. PlusCal reads more like pseudocode. Maybe with some more training/effort the TLA+ would be obvious as well.