Hi Yuri,
There are two good reasons to use PlusCal instead of TLA+.
1. Most people who don't know TLA+ find PlusCal easier to understand.
This can make a big difference if you're writing something to be read
by others. That's why I've published several algorithms in PlusCal
but I don't remember publishing one written in TLA+.
2. Traditional multiprocess synchronization algorithms involve
control state. I usually find it more natural to describe that
control state using PlusCal's programming-language structures rather
than explicitly introducing the pc variable. (This applies as well to
sequential programs.)
Related to 1 is the fact that you can write f[x] := e instead of the
uglier
f' = [f EXCEPT ![x] = e]
I believe that most uses of procedures are not the best way to express
the desired algorithm. As Stephan suggested, if a procedure has only
a single label at the beginning, then it is almost always better to
either replace it with a macro or else define a TLA+ operator that
allows you to replace the procedure call with a simple assignment
statement. People who are not used to programming with functional
languages often don't understand how anything computed with a loop
can easily be computed by a recursively defined TLA+ operator.
Leslie