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:
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