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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Tue, 28 Jun 2022 09:07:06 +0200*References*: <9e859fd3-6d18-43f6-81b0-ed329f780047n@googlegroups.com>

Hello, I believe that TLC is wrong when it claims that your liveness property is a tautology. Your fairness conditions include \A rm \in RM : SF_vars(TMRcvPreparedNO(rm)) where TMRcvPreparedNO is a stuttering action (as the comment above the action definition confirms). Therefore, ENABLED <<TMRcvPreparedNO(rm)>>_vars is equivalent to FALSE (for any value of rm), and the fairness condition is equivalent to TRUE – but that just means that this condition is trivial, not that the entire liveness property is a tautology. When I comment out this useless fairness condition, TLC throws an exception that appears to indicate that some internal tables become too big. Trying to reduce the size of the fairness condition, I defined formulas TMNext and RMNext(rm) corresponding to the disjunctions of all actions of the transaction manager and of the resource managers, respectively [1]. I then replaced your fairness conditions by /\ WF_vars(TMNext) /\ \A rm \in RM : WF_vars(RMNext(rm)) Now TLC produces what appears to be a sensible counter-example in which the TM reboots very frequently. I therefore adjusted that condition by removing the TMReboot action from the fairness condition [2], i.e. Fairness == /\ WF_vars(TMRcv2PC \/ TMDecideToCommit \/ TMDecideToAbort \/ TMForgetCtx) /\ \A rm \in RM : WF_vars(RMNext(rm)) For this specification, TLC says that the liveness property is satisfied. (Note in particular that weak fairness appears to be enough for this specification.) Of course, it is up to you to decide if that corresponds to a reasonable fairness hypothesis for your algorithm. Lessons learnt: 1. Do not assert fairness conditions for stuttering actions – although I believe that TLC should be able to handle those. 2. Prefer few fairness hypotheses for disjunctions of actions (that correspond to progress of individual actors) over conjuncts of many individual fairness conditions. Hope this helps, Stephan [1] Probably you do not want to include all actions in these disjuncts, but I didn't have time to understand your specification in detail. [2] I am assuming that rebooting corresponds to an error in the execution, which the algorithm has to be prepared to handle, but which you do not request to occur. 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/2C070E7E-A900-4476-B102-808738D0A34A%40gmail.com. |

**Attachment:
TradTwoPhase.tla**

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/2C070E7E-A900-4476-B102-808738D0A34A%40gmail.com. |

**Follow-Ups**:**Re: [tlaplus] Question about "Temporal formula is a tautology" in fairness***From:*Markus Kuppe

**References**:

- Prev by Date:
**[tlaplus] Re: Question about "Temporal formula is a tautology" in fairness** - Next by Date:
**Re: [tlaplus] Question about "Temporal formula is a tautology" in fairness** - Previous by thread:
**[tlaplus] Re: Question about "Temporal formula is a tautology" in fairness** - Next by thread:
**Re: [tlaplus] Question about "Temporal formula is a tautology" in fairness** - Index(es):