[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

How about writing:

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

Guessing the liveness interpreter doesn't like the 1 = 1 statement.

Andrew

On Sunday, June 26, 2022 at 4:35:50 AM UTC-4 allenh...@xxxxxxxxx wrote:
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/8a0b5701-692a-4a1b-9942-cab0458c958dn%40googlegroups.com.

• References: