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,
Roger
Le mercredi 28 octobre 2015 16:04:07 UTC-4, R Villemaire a écrit :
Hi,
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 --------------------------------
VARIABLES perte
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)
=============================================================================