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

[tlaplus-google-group@xxxxxxxxxxx]

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 <jonesmvc@xxxxxxxxx> 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…?

--
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/2F1BEF26-EE94-4572-A899-599E0E9C7BE2%40lemmster.de.