The 3 GB can probably be attributed to the set of fingerprints (of explored states). Try increasing the memory allocated to TLC on the TLC Options page of the Toolbox. There are countless optimizations to make model-checking faster. My feeling is that the proposed optimization doesn’t justify the effort. That said, efficient state-graph serialization alone would be useful infrastructure for other features. Thus, I’m happy to advise anybody who wants to do the heavy lifting. Markus
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/9A4348E4-2A56-42D8-B398-6C6376D8FEBB%40lemmster.de. |