Since the atomic propositions of [P.sub.i] (those in A[P.sub.i]) can be read by other processes, and since the value of the atomic propositions of [P.sub.i] gives some information about the possible current local state of [P.sub.i], we shall refer to [L.sub.i] as the externally visible location counter of [P.sub.i].
Since these atomic propositions are combined into the externally visible location counter [L.sub.i], this requires only a single write operation.
In an atomic read/write model, a simple term can be used as the guard of an arc, since checking that a simple term evaluates to true (and therefore that the arc can be executed) can be done using a single atomic read operation (which reads the single shared variable or externally visible location counter that the simple term refers to, depending on its form).
In our framework, there are two types of variables: (1) shared variables, which every process can read/write, and (2) the externally visible location counter, which the owning process can write and which every other process can read.
Since the externally visible location counter does not distinguish [s.sub.i] and [t.sub.i], we introduce a function num, from the set of i-states to the natural numbers, that assigns a natural number to each i-state.
we can take the pair (L[[s.sub.i]], num[s.sub.i])) as uniquely defining [s.sub.i], i.e., as giving the location counter (which, in effect, points to the "current" local state).
(13) Note also that the externally visible location counter (which encodes the atomic propositions) is not introduced until Phase 2; Phase 1 deals directly with the atomic propositions.
4.2.1 Step 2.1: Introduce the Externally Visible Location Counters. We now introduce the externally visible location counter [L.sub.i], and replace all references to the atomic propositions in [AP.sub.i] by references to [L.sub.i]:
We note that whenever the atomic propositions in A[P.sub.i] are mutually exclusive and exhaustive (in other words, every atomic proposition is true in exactly one i-state, with no two atomic propositions being true in the same i-state), then we can encode the externally visible location counter [L.sub.i] efficiently by setting its value to the name of the proposition that is currently true, rather than the singleton set containing that proposition.
Thus, we could optimize the synthesis method by "grouping" only the atomic propositions of each process [P.sub.i] that are referenced by some [P.sub.j], j [not equal to] i, into the externally visible location counter [L.sub.i].
[L.sub.i] is the externally visible location counter, and [num.sub.i] is an integer variable that contains the number of the current i-state.