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