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

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

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



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/8bc290a6-7201-453e-b531-387822f7022en%40googlegroups.com.