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

Narayanan

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