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

[Alen <451686157@xxxxxx>]

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.