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

> Where is the detailed location of the code for state space traversal in TLC?

TLC's source code is on GitHub:

https://github.com/tlaplus/tlaplus/tree/master/tlatools/org.lamport.tlatools/src/tlc2

As Andrew said, the algorithm is breadth-first search. Today, the main components of the search are:

tlc2.tool.impl.Tool (enumerates initial and successor states)
tlc2.tool.queue.IStateQueue and its subclasses (stores the queue of not-yet-visited states)
tlc2.tool.fp.FPSet and its subclasses (stores the set of already-visited states; or rather, the 64-bit hashes of already-visited states)
tlc2.tool.Worker (in a loop: dequeues a state, checks properties, enumerates successors, and enqueues not-yet-visited successors)

Andrew wrote that "there really isn't much to optimize". This is only half true. There are many different ways to optimize state exploration: make successor-state enumeration faster, make the queue have lower thread contention, make the visited-state-set use less (or more) memory, etc.

However, many people much smarter than me have spent enormous effort making TLC as fast as possible. The truth in Andrew's statement is that "there really isn't much left to optimize, and what's left is very difficult to implement correctly". I don't want to discourage you---many people would be very grateful if you improved TLC's performance---but I don't know of any low-hanging fruit you can pick.

> Is there a good solution to the state space explosion problem in TLC?

It depends. Andrew alluded to my favorite solution: symmetry reduction. Symmetry reduction can exponentially decrease the number of states that TLC has to explore. You can check invariants and action properties under symmetry reduction, but unfortunately you cannot use it to check liveness properties faster.

If you are able to use symmetry reduction, I highly recommend it as the first line of defense against state space explosion. You can find information about it in Specifying Systems, section 14.3.4:

https://lamport.azurewebsites.net/tla/book-02-08-08.pdf

Calvin

On Thu, Sep 15, 2022 at 5:03 AM Andrew Helwer <andrew.helwer@xxxxxxxxx> wrote:

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.