The NCES plant model will consist of the same PN model shown in the
previous section. Notice that, while there is an unbounded place in
this net, 
, this is of no consequence as it is the only unbounded
place and no specification is related to its input/output transitions
( 
, 
). Below we show the control inputs and outputs which
are relevant only to the em Different Types for M3 Specification.
Figure 24: Input/Output Signals for NCES
For clarity, the specification models are shown separately in Figure 25. The controller function is then:
Figure 25: Specification Model for Different Types for M3.