Example 3.15: The FSM in Figure 3.11 can be formally represented as follows: States Inputs Outputs {none, waiting,crossing) ((sig, sigY, sigR) {present, absent)) (pedestrian) present, absent)) {crossing} = = initial States = The update relation is given below: (((none, absent)) ifs = crossing ((none, absent), (waiting, present)) f(crossing, absent)) (s, absent otherwise Ni(sig@ = present if 8 = none if s = waiting possibleUpdates(8,1) = (3.3) Ni(sigh) = present for all s e States and i E Inputs. Note that an output valuation o E Outputs is a function of the form o: Pedestrian) {present, absent). In (33), the second alternative gives two possible outcomes, reflecting the nondeterminism of the machine