I haven't worked in TLA+ (yet) but designed a lot of state machine architectures for industrial controls and safety systems and the real art is system and sub-system decomposition, but getting this right is the key to avoiding state explosions.
In the context of Moore machines, which are more prone to state explosion than Mealy machines, in my practical uses, but Moore machines are easier to design for creating expected known behaviours, I suggest the following.
Generally, if you have a state explosion in a machine then you often 'fix' this by creating a group of hierarchal machines.
First thing to look for is do you have modes you can break out? In my world that is often a piece of equipment (subsystem) can have conditioning modes of Auto, Manual, Off, Remote. You then use the state of the mode machine as discrete boolean inputs into your main machine.
I use a nomlaclature whereby the state machine name prefixes the variable, seperated by a dot or underscore eg "stackermode.auto" as a boolean etc etc, this works out well for generating class based language equivelents when define your variables as class variables, eg if you want to generate python or java for simulation or demo purposes, because maybe you want to bolt an OPC server onto it, or similar.
I find also that carefully chosen hierarchies can enable creating "encapsulation by architecture" and also reduce your possible credibly needed test cases by making a rule that, for example, in the heirarchy you can only talk to/from one level up or down, and no sideways communication, thus vastly reducing number of test cases, assuming implementation prevents any possible side effects to other machines on the same layer.
As I said, the system/subsystem decomposition is where the black art is and it seems surprisngly difficult to teach/artitculate a general methodology, it seems to something you learn like German, one day you are all at sea and then one day all of a sudden the word order just sort of clicks,
Hope this is helpful.
When I use TLA+ for verification projects, I always encounter the problem of state space explosion, which causes the machine to crash or take a long time. Therefore, I want to look at the TLC state space traversal algorithm to see if the state traversal algorithm can be optimized.
question:
1. Where is the detailed location of the code for state space traversal in TLC?
2. Is there a good solution to the state space explosion problem in TLC? thanks