[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] a question about WF
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,
> On 28 oct. 2015, at 20:54, R Villemaire <villemai...@xxxxxxxxx> wrote:
> 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)
> 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+u...@xxxxxxxxxxxxxxxx.
> To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
> Visit this group at http://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.