[tlaplus] Re: Where is the code for the state space traversal algorithm in TLC?

[Andrew Helwer <andrew.helwer@xxxxxxxxx>]

It's breadth-first search that works pretty much the way you would expect: first generating all successor states to the current state, using those states' hashes to check whether they've already been visited, and pushing them onto the state queue if not. There is some extra logic when symmetry is involved but that's about it; there really isn't much to optimize. The best solution to state space explosion is probably to use small model sizes (3, at most 5 elements) and avoid using operations that add permutations (like recording order of operations) or subset-selection to your spec. Also avoid defining extremely large sets, like powersets of records and stuff like that.

If all that fails you can also try Apalache, which uses symbolic instead of finite state model checking.

Andrew

On Wednesday, September 14, 2022 at 11:09:41 PM UTC-4 zhin...@xxxxxxxxx wrote:

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

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/1fbed6b5-7955-4f0c-af44-a16b1ca79237n%40googlegroups.com.