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

[Jones Martins <jonesmvc@xxxxxxxxx>]

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

On Mon, 21 Feb 2022 at 23:06, <tlaplus-google-group@xxxxxxxxxxx> wrote:

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 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/2F1BEF26-EE94-4572-A899-599E0E9C7BE2%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/CABW84KzEtUZtZnW1Nk94jHyy%3DjCGc_1z%2BJV2vZVywtNN8_mLng%40mail.gmail.com.