[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
> 12:14:18
> Does it mean that TLC check liveness properties at this time ?
> thanks
> Narayanan


from [1]:

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

[2] 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).


[1] https://lamport.azurewebsites.net/tla/current-tools.pdf

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.