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.
/\ SF_vars(
/\ tmState = "aborted"
/\ tmConfirmed /= RM
/\ \A rm \in RM:
/\ [type |-> "RMABORTED", rm |-> rm] \in msgs
/\ tmConfirmed' = RM
/\ UNCHANGED <<rmState, tmState, tmParticipants, tmPrepared, msgs>>
)
--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/09eb6219-9a8b-4f35-ad5a-e522cf160e05n%40googlegroups.com.
/\ \A rm \in RM:
SF_vars(TMRcvAborted(rm) /\ tmConfirmed' = RM)
```