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

[tlaplus] Do liveness properties only get evaluated at the end of a TLC run

My TLC run is taking a while and I have several liveness properties. 

I do see output like
Checking 5 branches of temporal properties for the current state space with 81961030 total distinct states at (2020-03-15 11:52:09)

        Finished checking temporal properties in 22min 09s at 2020-03-15 12:14:18

Does it mean that even TLC run is not complete, it did evaluate some liveness properties ?  Or does it evaluate only at the end ?

I want to find out what level of confidence I can get out of a TLC run if I abort it after sometime.


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/f326393e-5e34-4359-af31-4cec6a6600ee%40googlegroups.com.