Re: Please help with temporal formula

[dominik...@xxxxxxxxx]

On Friday, February 1, 2019 at 6:52:28 AM UTC-8, 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

Clarification: Rewrite of the formula, not rewrite of TLA+ :)