"As long as, eventually"

[dominik...@xxxxxxxxx]

Hello,

I have a question regarding a temporal formula. Let's assume I have the following Spec:

VARIABLE Objects

Foo_1 ==
  Objects' = Objects \cup {"a"}

Foo_2 ==
  Objects' = Objects \ {"a"}

Bar_1 ==
  /\ "a" \in Objects
  /\ Objects' = Objects \cup {"b"}

Bar_2 ==
  /\ "a" \in Objects
  /\ Objects' = Objects \cup {"b"}

Init ==
  Objects = {}

Next ==
  \/ Foo_1
  \/ Foo_2
  \/ Bar_1
  \/ Bar_2
  \/ UNCHANGED Objects

Spec == /\ Init /\ [][Next]_<< Objects >> /\ WF_<< Objects >>(Bar_1)

- Foo_1 adds "a" to Objects
- Foo_2 removes "a" from Objects
- Bar_1 adds "b" to Objects if "a" is in Objects
- Bar_2 removes "b" from Objects if "a" is not in Objects

For each behavior Objects could be {}, {"a"}, {"a", "b"}, {"b"}

I would like to use a temporal formula to document the behavior:

<>[]("a" \in Objects) => <>[]("b" \in Objects)

In words:

"Given that Bar_1 is weakly fair, If eventually "a" is continuously in Objects then eventually "b" is continuously in Objects"

My Questions:

- Is this temporal formula actually expressing what I put in words
- Does that make sense at all? Or is it more of a tautology (in logic and rhetoric)?

Thanks, Dominik