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

[tlaplus] Proving refinement for specs with fairness properties


I would like to ask, if the current TLAPS can handle fairness properties when proving a refinement of specs containing liveness conditions. Maybe there is some special approach about that? Bellow I try to provide only relevant parts of the spec just to keep the mail short. If needed, I can share the specs.

Excerpt of the abstract spec:

    Spec == Init /\ [][Next]_sstate /\ WF_sstate(Next)

Excerpt from the refining spec:

    Live == WF_vars(Next)
    Spec == Init /\ [][Next]_vars /\ Live

Here is the refinement mapping:

    rmap == [ s \in S |-> sessions[s] = "ready" ]
    A0 == INSTANCE Abstract WITH SID <- S, sstate <- rmap

For now, I have proved the Init and the Next conjuncts for the refinement and added the following for the liveness part.

    <1>3. Live => (WF_(rmap) (A0!Next)) OMITTED

I wonder, if I can do something more about that, considering the current TLAPS limitations with temporal operators.

Karolis Petrauskas

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/CAFteovJ%3DcmHVwMBO5s3F3-rQYwOWdC26M%2B1udOLAUBF-uW1cqw%40mail.gmail.com.