In the R&W framework, specifications are also described using state
machines. In order to obtain the model 
we must do the
following:
is constructed over
a set of events, 
. It is assumed that each is
nonblocking. is ``self-looped'' with respect to
. In terms
of the state machine , this simply means adding a
self-looping edge at each state, and labeling it with the events
that are possible in P but not constrained
by . Let 
denote the self-looped
specifications corresponding to . Notice that each includes events that may not be controllable. In Figure
7, we give the state machines for requirements (i)
and (ii) of Specifications I.
. These are
the global specifications we want to enforce on the behavior of P.
In order to obtain the intersection of two state machines, we start with
the composed initial state 
, and, from here, we
determine the events that are possible in both graphs. If event
is possible from both initial states, then in the
intersection graph, there is an edge from 
to the corresponding composed state 
. (See Section 6.1.)
The model can now be used to obtain a generator for the ``legal
language,'' 
, or the largest behavior of the plant that
satisfies all the requirements given by . This is given by
.
Remark
It is not necessary to intersect all the 's before
computing the legal language. For instance, since
, we have
chosen to construct first in our Two-Pusher Example the recognizer
, which gives the ``legal states'' of
the system. Finally, we construct the legal language by
intersecting 
with 
. (See Section 6.1.)
With this formalism, both ``state-avoidance'' problems (``safety specifications'') and ``string-avoidance'' problems (``sequential specifications'') can be considered. However, we should point out that describing specifications by means of state machines is often a nontrivial task.