Re: [tlaplus] Proving refinement for specs with fairness properties

the current distribution of TLAPS does not support reasoning about liveness or fairness but this will be the main feature of the next release, which should see the light of the day before summer. If you are very adventurous you could play with the version available at the "updated_enabled_cdot" branch of the repository [1] but there is no documentation yet and only two examples (in particular examples_draft/SimpleExampleWF.tla) so I wouldn't recommend it.

[1] https://github.com/tlaplus/tlapm

On 11 Apr 2021, at 19:49, Karolis Petrauskas <k.petrauskas@xxxxxxxxx> wrote:

Hello,

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.