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

Re: a question about WF

Thanks Stephan,
you are indeed right! What confused me was that with additional variables the answer can be different. But then, these variables can make the action non-stuttering, as you said. Thanks for the help !
best wishes,

Le mercredi 28 octobre 2015 16:04:07 UTC-4, R Villemaire a écrit :
I am new to TLA and I encountered the following behaviour that I don't understand.

In the module below, I thought that the trace where perte=FALSE in every state would satisfy Spec and hence be a counter-example to property TEST. But TLA+ toolbox does not return any counter-example for this property.

I must have been missing something with the WF_vars, but my impression is that both should be true for the above trace as every step is a perte_canal and also a recepteur step.

best wishes,
Roger Villemaire

TLA+ Toolbox provides a user interface for TLA+ Tools.

This is Version 1.5.1 of 1 June 2015 and includes:
  - SANY Version 2.1 of 24 February 2014
  - TLC Version 2.07 of 1 June 2015
  - PlusCal Version 1.8 of 2 April 2013
  - TLATeX Version 1.0 of 12 April 2013
-------------------------------- MODULE jean --------------------------------


vars == << perte >>

Init == perte = FALSE

perte_canal == perte' = TRUE \/ perte' = FALSE

recepteur == perte' = perte

Next == perte_canal \/ recepteur

Spec == /\ Init /\ [][Next]_vars
        /\ WF_vars(perte_canal)
        /\ WF_vars(recepteur)

TEST == <>(perte)