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

i am not sure if a lean port is important. TLA+ could do with a bit more TLC (pun intended) with regards its devEx.

Also congratulations to the author, I'll try and reproduce this over the weekend.