Re: [tlaplus] "As long as, eventually"

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

Hello Dominik,

your temporal formula corresponds to your informal explanation (modulo the fact that the fairness part of the explanation is part of the specification, not the property). It is quite easy to see that the property is true of your specification:

1. You assume "a" \in Objects to be persistently true in an execution.
2. This condition enables action <<Bar_1>>_Objects as long as "b" is not in Objects (this is actually a somewhat subtle point: Bar_1 is a stuttering action if both "a" and "b" are contained in Objects).
3. Using weak fairness for that action, we know that it must eventually execute and therefore establish "b" \in Objects.
4. No action ever removes "b" from Objects, and therefore it remains there persistently.

However, I suspect that item (4) actually does not correspond to your intuition and that you meant Bar_2 to remove "b" from set Objects rather than being a copy of Bar_1. Your property will not hold of the modified specification.

Regards,
Stephan


> On 15 Jan 2019, at 18:17, dominik...@xxxxxxxxx wrote:
> 
> 
> Hello,
> 
> I have a question regarding a temporal formula. Let's assume I have the following Spec:
> 
> VARIABLE Objects
> 
> Foo_1 ==
>  Objects' = Objects \cup {"a"}
> 
> Foo_2 ==
>  Objects' = Objects \ {"a"}
> 
> Bar_1 ==
>  /\ "a" \in Objects
>  /\ Objects' = Objects \cup {"b"}
> 
> Bar_2 ==
>  /\ "a" \in Objects
>  /\ Objects' = Objects \cup {"b"}
> 
> Init ==
>  Objects = {}
> 
> Next ==
>  \/ Foo_1
>  \/ Foo_2
>  \/ Bar_1
>  \/ Bar_2
>  \/ UNCHANGED Objects
> 
> Spec == /\ Init /\ [][Next]_<< Objects >> /\ WF_<< Objects >>(Bar_1)
> 
> - Foo_1 adds "a" to Objects
> - Foo_2 removes "a" from Objects
> - Bar_1 adds "b" to Objects if "a" is in Objects
> - Bar_2 removes "b" from Objects if "a" is not in Objects
> 
> For each behavior Objects could be {}, {"a"}, {"a", "b"}, {"b"}
> 
> I would like to use a temporal formula to document the behavior:
> 
> <>[]("a" \in Objects) => <>[]("b" \in Objects)
> 
> In words:
> 
> "Given that Bar_1 is weakly fair, If eventually "a" is continuously in Objects then eventually "b" is continuously in Objects"
> 
> My Questions:
> 
> - Is this temporal formula actually expressing what I put in words
> - Does that make sense at all? Or is it more of a tautology (in logic and rhetoric)?
> 
> Thanks, Dominik 
> 
> -- 
> 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 https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.