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

[tlaplus] In the Composition Rule from section 10.2 of Specifying Systems, what is F_ij?

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!


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.