Personally, I keep trying PlusCal and keep going back to plain TLA+. Every time I get bogged down trying to learn it, and instinctively switch back because it's

Personally, I keep trying PlusCal and keep going back to plain TLA+. Every time I get bogged down trying to learn it, and instinctively switch back because it's faster (or maybe it just clicks better for me). I got Hillel's book, so I'll probably give it another shot soon. 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]