Re: [tlaplus] Confidence in passing liveness properties after a TLC run

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

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

Hi,

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

Markus

[1] https://lamport.azurewebsites.net/tla/current-tools.pdf
[2]
https://github.com/tlaplus/tlaplus/blob/64140e5940f5449833f0ed50f362f4c3b22579be/tlatools/src/tlc2/output/MP.java#L1017-L1023

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