Re: [tlaplus] Please help with temporal formula

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

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, dominik...@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 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.