----------------------------- MODULE attention -----------------------------
(* Roger Villemaire (C) 2015. *)

(* Il faut faire attention au point de détail suivant.
   de Stephan Merz 2015-10-28
   "Hello Roger, 

    welcome to the TLA+ group. The formula WF_v(A) requires that whenever an <<A>>_v action is continuously enabled, 
    it will eventually be taken. In particular, any such action changes the variable v, which explains the result that you observe. 
    TLA+ will not let you specify that a non-observable (stuttering) action must occur, since this would violate closure under 
    addition or removal of stuttering. 

    Hope this helps, 
    Stephan "

Donc si on enlève la variable bidon, TEST est vraie et sinon fausse.
*)

VARIABLES perte, bidon

vars == << perte, bidon >>

Init == perte = FALSE /\ bidon = FALSE

perte_canal == (perte' = TRUE \/ perte' = FALSE) /\ bidon' = ~bidon

recepteur == perte' = perte /\ bidon' = ~bidon

Next == perte_canal \/ recepteur

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


TEST == <>(perte)

=============================================================================
\* Modification History
\* Last modified Wed Oct 28 17:22:57 EDT 2015 by villem
\* Created Wed Oct 28 17:15:54 EDT 2015 by villem