[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

# Please help with temporal formula

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