Comment by uptodatenews

You run into Rices theorem if you try to apply it too heavily.

I made https://github.com/RCSnyder/tlaplus-process-studio

https://tlaplus-process-studio.com/

For local only high level modelling. Its not a full tie into the actual model checker, but its meant to serve as a first step into system modelling for state machine modelling for beginners