[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.
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.