[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: zhi niu <zhiniu28@xxxxxxxxx>*Date*: Wed, 14 Sep 2022 20:09:41 -0700 (PDT)

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/2ce0d4cb-94bb-4735-97b7-ccadf311c2f1n%40googlegroups.com.

**Follow-Ups**:**[tlaplus] Re: Where is the code for the state space traversal algorithm in TLC?***From:*Gareth Smith

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

- Prev by Date:
**[tlaplus] Re: How do we use the transaction api in spec？** - Next by Date:
**[tlaplus] Re: Where is the code for the state space traversal algorithm in TLC?** - Previous by thread:
**[tlaplus] Re: How do we use the transaction api in spec？** - Next by thread:
**[tlaplus] Re: Where is the code for the state space traversal algorithm in TLC?** - Index(es):