Re: [tlaplus] Please help with temporal formula

[dominik...@xxxxxxxxx]

On Friday, February 1, 2019 at 9:25:56 AM UTC-8, Stephan Merz wrote:
> Hello,
> 
> 
> first note that the bound of your quantifier does not correspond to what you have in mind: the formula
> 
> 
>  \A foo \in {Object \in Objects : Object.Type = "Foo"} : ...
> 
> 
> 
> only talks about the objects of type "Foo" that are initially present – which is the empty set. You want to quantify over the objects of type "Foo" that may potentially exist during the course of the execution. Then, your property can be expressed as
> 
> 
> Liveness == \A d \in 1 .. 3 : 
>   <>[]([Type |-> "Foo", Data |-> d] \in Objects) =>
>   <>[]([Type |-> "Bar", Data |-> d] \in Objects)
> 
> 
> You can check that property using TLC, and you'll get a meaningful counter-example. If in your spec you replace the weak fairness condition on Next by a weak fairness condition on Bar, you'll get a different meaningful counter-example.
> 
> 
> Regards,
> Stephan
> 
> 
> 
> 
> On 1 Feb 2019, at 15:25, domin...@xxxxxxxxx wrote:
> 
> 
> 
> Hello,
> 
> I have a question regarding temporal formulas: Let's say I have the following Spec:
> 
> VARIABLE Objects
> 
> Foo ==
>   \/ \E i \in 1..3:
>        Objects' = Objects \cup { [Type |-> "Foo", Data |-> i] }
>   \/ \E i \in 1..3:
>        Objects' = Objects \ { [Type |-> "Foo", Data |-> i] }
> 
> Bar ==
>   \/ \E foo \in { Object \in Objects : Object.Type = "Foo"}:
>        /\ ~ [Type |-> "Bar", Data |-> foo.Data] \in Objects
>        /\ Objects' = Objects \cup { [Type |-> "Bar", Data |-> foo.Data] }
>   \/ \E bar \in { Object \in Objects : Object.Type = "Bar"}:
>        /\ ~ [Type |-> "Foo", Data |-> bar.Data] \in Objects
>        /\ Objects' = Objects \ { bar }
> 
> Init ==
>   Objects = {}
> 
> Next ==
>   \/ Foo
>   \/ Bar
> 
> Spec ==
>   Init /\ [][Next]_<< Objects >> /\ WF_<< Objects >>(Next)
> 
> In prose Bar is responsible for
> - adding an Record [Type |-> Bar, Data |-> d] if there is an record [Type |-> Foo, Data |-> d] and 
> - removing a Record [Type |-> Bar, Data |-> d] if there is no an record [Type |-> Foo, Data |-> d]
> 
> Since Foo may add and remove any record [Type |-> Foo, Data |-> d] I can only state that "if forever there is a record [Type |-> Foo, Data |-> d] there will eventually forever be a record [Type |-> Bar, Data |-> d]" .
> 
> But I'm having trouble capturing that in a TLA+ formula:
> 
> Does_Not_Evaluate ==
>   \A foo \in {Object \in Objects : Object.Type = "Foo"}:
>     []([Type |-> "Foo", Data |-> foo.Data] \in Objects) => <>[]([Type |-> "Bar", Data |-> foo.Data] \in Objects)
> 
> My questions:
> - Is this formula correct (even though TLA+ cannot handle the temporal formula)
> - Is there a possible rewrite so TLA+ can handle the temporal formula
> 
> Thank you,
> 
> 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 tlaplu...@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.

Thank you for your help Stephan, great!!