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

Re: [tlaplus] Rechecking safety and liveness properties without regenerating state space



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


On Feb 22, 2022, at 7:49 AM, Jones Martins <jonesmvc@xxxxxxxxx> wrote:

I see. I just ran a 3-hour-long verification and Storage says 3 GB. I assume this is mostly due to the fingerprint graph then?

Do you think it'd be useful to check properties while avoid rerunning the state-space exploration?

--
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.