In my experience the learning curve of tlaplus is very long.
Let's be clear. I don't want to discourage anybody to use tlaplus. I think it's a very
valuable tool and that specifying an algorithm with it will always bring you
deep insights.
I also think that if you use a subset of tlaplus (let's say TLC + PCAL) you will
be able to use it very quickly.
I just want to avoid discouragement among those that are not aware that it is
a large piece of software that allows to do many things (specifying algorithms
but also digital systems, classical but also parallel algorithms, proving
everything, model checking).
I think tlaplus is a nice trip do to. But it's just like China, maybe, sometimes, you can
consider something a bit longer than a two-day round trip.
So maybe (I just say maybe -- I hope it will prudent enough) you may want to take
your time to get acquainted with it.
--
FL