Please help with temporal formula

[dominik...@xxxxxxxxx]

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