[tlaplus] Question about "Temporal formula is a tautology" in fairness

[钱晨 <allenhandora@xxxxxxxxx>]

I have recently written a 2pc protocol with fairness, I first write all request/response handlers as the strong fairness(except reboot and exception events) in order to pass the liveness check:

the liveness check is as below:





2PCLivevess == \A r \in RM: 1 = 1 ~> (2pcState[r] = "aborted" \/ 2pcState[r] = "committed")

the spec is something like below:

================== start====================

Fairness == 

    /\ WF_vars(TMRcv2PC)

    /\ SF_vars(TMDecideToAbort)

    /\ SF_vars(TMDecideToCommit)

    /\ \A rm \in RM:

            SF_vars(TMRcvPreparedOK(rm))

    /\ \A rm \in RM:

            SF_vars(TMRcvPreparedNO(rm))

    /\ \A rm \in RM:

            SF_vars(TMRcvCommitted(rm))   

    /\ \A rm \in RM:

            SF_vars(TMRcvAborted(rm))   

    /\ \A rm \in RM:                            

            SF_vars(RMRcvPrepareOK(rm))

    /\ \A rm \in RM:             

            SF_vars(RMRcvPrepareNO(rm))

    /\ \A rm \in RM:

            SF_vars(RMRcvCommit(rm))   

    /\ \A rm \in RM:

            SF_vars(RMRcvAbort(rm))              

    /\ \A rm \in RM:

            SF_vars(OrphanRMRcvMsg(rm))   

    /\ \A rm \in RM:                                 

            SF_vars(RMForgetCtx(rm))

    /\ SF_vars(TMForgetCtx)

================== end ====================

While the model check reports "Temporal formula is a tautology (its negation is unsatisfiable).". Can any tell me why my fairness check reports the errors.

-- 
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/9e859fd3-6d18-43f6-81b0-ed329f780047n%40googlegroups.com.

Attachment: TradTwoPhase.tla
Description: Binary data