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

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

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

CONSTANTS Replica \* the set of nodes

here are some variable meanings.
,       \* uset[r]: the set of updates seen by replica r \in Replica
,      \* 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?



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.