Rechecking safety and liveness properties without regenerating state space

[Jones Martins]

Hi everyone,

I know there are checkpoints in TLC, which allow the user to continue running the model checker after stopping it.

I'd like to know if there's a way to check safety and liveness properties without regenerating the state space. I'm assuming TLC stores the state space in a `states` directory, so running an invariance checker would be possible, at least...?

Thanks!

Jones

[tlaplus-go...@lemmster.de]

The states/ folder contains the queue of unexplored states and, for some properties, also a fingerprint graph.  However, this fingerprint graph is specific to the properties and cannot even be converted into a state graph without rerunning state-space exploration.

Markus

On Feb 21, 2022, at 3:39 PM, Jones Martins <jone...@gmail.com> wrote:

I'd like to know if there's a way to check safety and liveness properties without regenerating the state space. I'm assuming TLC stores the state space in a `states` directory, so running an invariance checker would be possible, at least…?

[Jones Martins]

Hi Markus,

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?

Jones

--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/2F1BEF26-EE94-4572-A899-599E0E9C7BE2%40lemmster.de.

[tlaplus-go...@lemmster.de]

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

[Jones Martins]

Hi Markus,

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?

Jones

--
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+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/9A4348E4-2A56-42D8-B398-6C6376D8FEBB%40lemmster.de.