[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Rechecking safety and liveness properties without regenerating state space
Which state-space serialization optimizations would you find more useful? Is there a list for them?
Also, a bit unrelated: GPU SSC algorithms would help with verifying liveness instead of safety, is that right?
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.
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 a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/c32aT6Div1I/unsubscribe.
To unsubscribe from this group and all its topics, 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.
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/CABW84KxoC2QA%3DW%2BCj%2BH0MsvzJEb%2B1tcCSprLCn6mQNWbVMF-Pw%40mail.gmail.com.