Re: [tlaplus] How to express liveness in my spec?Why TLC cannot handle this temporal formula?

Hello,

you have not shown what the status of identifier Oid is. TLC can only evaluate quantification over finite constant sets [1]. If you have a constant parameter Oid that represents (a superset of) all potential object identifiers [2] then your first formulation

\A oid \in Oid, r \in Replica: oid \in doset[r] ~> (\A s \in Replica : oid \in uset[s])

should be fine since both Replica and Oid will be instantiated by finite sets in your model. The second formulation

[](\A r \in Replica: \A oid \in doset[r]:<>(\A s \in Replica: oid \in uset[s]))

cannot be evaluated because the range of the second quantifier `doset[r]' is not a constant set.

Regards,

Stephan

[1] Please see section 14.2.4 of Specifying Systems for the precise definition of temporal formulas that TLC can handle.

[2] Since you can only submit finite instances to TLC anyway, you must have bounded this set for model checking. This will probably mean that at some point no new object ID is available and the action that introduces new IDs will be disabled.

On 26 Aug 2019, at 17:01, Alen <451686157@xxxxxx> wrote:

hello, I am writing a spec to describe a network with many nodes,

CONSTANTS Replica \* the set of nodes

here are some variable meanings.
VARIABLES uset, \* uset[r]: the set of updates seen by replica r \in Replica doset, \* doset[r]: the set of updates made by replica r \in Replica

I want to express liveness as every operation made must be delivered to every replica.

At first I write as this(oid means operation ID):

Fairness == \A r \in Replica: WF_vars(Send(r)) /\ WF_vars(Deliver(r)) Spec == Init /\ [][Next]_vars /\ Fairness Liveness == \A oid \in Oid, r \in Replica: oid \in doset[r] ~> (\A s \in Replica : oid \in uset[s])

But it's hard to enumerate Oid. I have to override nat by hand.So I want to know how to solve this question at usual?
I write another version later:

Liveness == [](\A r \in Replica: \A oid \in doset[r]:<>(\A s \in Replica: oid \in uset[s]))

But Unfortunately, my TLC(1.5.7) cannot handle this temporal formula.I want to know why and how to rewrite it?

THANKS
Alen

--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/1daed939-2987-4871-a059-9c223d0dd1a3%40googlegroups.com.

--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/F8997554-7C5B-4D00-807E-D162C74AFBD1%40gmail.com.