Re: [tlaplus] a question about WF

[Stephan Merz <stepha...@xxxxxxxxx>]

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



> On 28 oct. 2015, at 20:54, R Villemaire <villemai...@xxxxxxxxx> wrote:
> 
> 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)
> 
> =============================================================================
> 
> -- 
> 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.