I feel like PlusCal and TLA+ operate at a different level. I use PlusCal primarily when what I'm modeling has a lot of sequential "A then B then C..." steps. With PlusCal a program counter is implied and it maps more directly to sequential algorithms.

When I write regular TLA+, it's usually for things that aren't nearly as "order-dependent".