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

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.