[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Confidence in passing liveness properties after a TLC run
On 15.03.20 12:23, narganapathy@xxxxxxxxx wrote:
> If a TLC run didn't finish to completion, does it mean that I can't get
> any confidence on whether the model passed liveness properties ? (i.e.,
> are liveness properties evaluated only at the end ?).
> I see statements like below,
> 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
> Does it mean that TLC check liveness properties at this time ?
"-lncheck param: If this is omitted or param equals default, TLC
performs liveness checking periodically, when the number of distinct
states it finds increases by 10%. If param equals final, TLC does
liveness checking only after it has computed the complete state graph."
 shows what TLC shows for a partial liveness check of the state graph
(TLC_CHECKING_TEMPORAL_PROPS) and what it shows for a liveness check of
the complete state graph (TLC_CHECKING_TEMPORAL_PROPS_END).
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/47b243c2-8863-a98f-2d0d-2a1c9c7c9936%40lemmster.de.