a question about WF

[R Villemaire <villemai...@xxxxxxxxx>]

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)

=============================================================================