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.