CSSE 373 -- Formal Methods in Specification and Design

                           Quiz 20 Handout


You need to specify the behavior of a traffic light and a set of
crosswalk signals. To simplify this problem, assume that you only need
to specify the color of the traffic light in one direction, and you
only need to specify one crosswalk signal (the one affected by the
light you specify).

Here is the expected behavior of the traffic light:
 --  The light should be yellow for 5 seconds before changing to red.
 --  The light should only be red for 60 seconds.
 --  The light should be green for the rest of the 2 minute period.
You may use "G", "Y", and "R" as shorthand for the colors.

Here is the expected behavior of the crosswalk:
 --  The signal should show "Don't Walk" when the traffic light is
     either yellow or red.
 --  The signal should flash "Don't Walk" for 10 seconds before
     changing to Don't Walk.
 --  The signal should show "Walk" for the rest of the 2 minute
     period.
You may use "W", "F", and "D" as shorthand for these signals.

Use the notation "Sx" to denote the event that starts timer x, and
"Ex" to denote the event that occurs when timer x expires. The label
of each transition in a state diagram has 2 parts separated by a
slash: the input event that caused the transition, and an optional
output event created by the transition. For example, a transition
labeled "E20/S30" was caused by the expiration of timer 20, and this
transition causes the start of timer 30.