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

*From*: Andrew Wilcox <andrew.wilcox@xxxxxxxxx>*Date*: Thu, 2 Jan 2020 11:21:06 -0800 (PST)

In Specifying Systems section 10.1, Lamport derives a composition rule for composing two systems (equation 10.1 on page 138). The first disjunct in the next-state action of the right hand side reads:

-- N_1 /\ N_2

In section 10.2 (also on page 139) Lamport generalizes for multiple components and describes the Composition Rule. The corresponding disjunction in the general rule appears as:

\E i, j \in C : (i # j) /\ N_i /\ N_j /\ F_ij

and the rule concludes with "for some actions F_ij".

For the two component case with C = {1, 2}, this disjunction is equivalent to:

\/ N_1 /\ N_2 /\ F_12

\/ N_1 /\ N_2 /\ F_21

or, if F_12 is the same as F_21, I guess just N_1 /\ N_2 /\ F_12. In any case, it appears to be the same as the two component case, except for the addition of F.

I was following along up to this point, but here I got lost. What is F? Why is it needed?

Thank you!

Andrew

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/110fade9-36f7-4407-aedd-f4c0264fe50b%40googlegroups.com.

- Prev by Date:
**Re: [tlaplus] Re: Why strong fairness implies weak fairness?** - Next by Date:
**Re: [tlaplus] TLA+, Event B comparison** - Previous by thread:
**Re: [tlaplus] Re: Why strong fairness implies weak fairness?** - Next by thread:
**[tlaplus] Question regarding Two Phase Commit spec and the enabling condition of one of its definitions** - Index(es):