While some people prefer writing PlusCal, I don't think it's the majority. Most people I know just write TLA+. PlusCal is more suitable for "code-level" problems, like specifying low-level operations on concurrent data structures.
As to your point about TLC's sometimes surprising behaviour, I agree, but "mysteriousness" is common in software tools. These are things that are learned through experience. One way to estimate how things are going, even with no experience, is to look at the graphs of newly discovered states that the Toolbox draws. If they're trending down, you're in the process of converging; if they're still going up -- you're not.
While some people prefer writing PlusCal, I don't think it's the majority. Most people I know just write TLA+. PlusCal is more suitable for "code-level" problems, like specifying low-level operations on concurrent data structures.
As to your point about TLC's sometimes surprising behaviour, I agree, but "mysteriousness" is common in software tools. These are things that are learned through experience. One way to estimate how things are going, even with no experience, is to look at the graphs of newly discovered states that the Toolbox draws. If they're trending down, you're in the process of converging; if they're still going up -- you're not.