Most often, you’re not interested in checking temporal properties. If you are, though, here are some things to watch out for.
It’s easy to check that reachable states satisfy invariants. But to check liveness, how you reach those states also matters. If a thousand routes lead through state S, that’s 1,000 routes that need to be checked for liveness and only one state that needs to be checked for safety. So liveness is intrinsically much, much slower than checking invariants.
The Toolbox has a number of optimizations to make it easier to check invariants: multithreading, model symmetry sets, cloud computing, etc. These all assume, though, that we only care about individual states. None of these apply to temporal properties. So it’s even slower to check than you’d think at first.
An especially important one to watch out for are symmetric models. TLC can check them for temporal properties. However, the symmetry properties can provide false negatives: it can say that your spec satisfies the properties when it actually doesn’t.
Regular processes can stutter. Sometimes this is part of what you expect in your system- maybe you can’t rely on the message queue always being available. If not, though, you need to explicitly use fair process.