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

[钱晨 <allenhandora@xxxxxxxxx>]

Thanks for your nice explanation.

I have another question I want to ask. When I run the case after solving the problem of 'tautology', it happens to be a case that violates the liveness check like below

1. We have [a, b, c] as RM
2. ....

3. TM is in 'aborted' state and all rms are in 'TombstoneNo' (* means forget the result, and 2pc will use Presumed Abort to answer the TM)

4. TM receives one of the abort responses and fills in it in tmConfirmed(* like tmConfirmed = [a] *)

5. Tm occurred tmReboot(* and tmConfirmed will be empty again(* like tmConfirmed = [] *)

Then 4 and 5 will loop forever and cause a liveness problem

I solve the problem by adding the following formulas into the `fairness`(I also add another one that involves "committed" state), and it finally pass the liveness check

```

    /\ SF_vars(

        /\ tmState = "aborted"

        /\ tmConfirmed /= RM

        /\ \A rm \in RM:

            /\ [type |-> "RMABORTED", rm |-> rm] \in msgs

        /\ tmConfirmed' = RM

        /\ UNCHANGED <<rmState, tmState, tmParticipants, tmPrepared, msgs>>          

        ) 

```

It seems we must collect all responses before advancing to the next stage and cannot reboot during the process. In my way, we must write a completely new formula to achieve the goal. Does it exist another better writing style that can achieve the same goal or just use the original formula like `TMRcvAborted`?

Stephan Merz 在 2022年6月28日 星期二晚上11:55:48 [UTC+8] 的信中寫道：

> One more question, you say "When I comment out this useless fairness condition, TLC throws an exception that appears to indicate that some internal tables become too big.". I also encounter the problem, and I want to know what is meant by "some internal tables become too big". Does it mean that some data structures in TLC can not support the size of the action in the `Next`?

It's not the next-state relation that's the problem but the fairness conditions: TLC has to monitor for each fairness condition at which state the underlying action is enabled and which transitions correspond to the action being taken. I do not know how TLC represents this information, but apparently it is not meant to handle a lot of fairness conditions (remember that you have to multiply the RM actions by the number of resource managers in the model).

Stephan

-- 
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/09eb6219-9a8b-4f35-ad5a-e522cf160e05n%40googlegroups.com.