2.8.8 One more Refinement: The Push Button

We will demonstrate another application of refinement: introducing new features into an existing model. A typical traffic light system allows the pedestrians to request a light change by pressing a button. We will introduce this feature in a new refinement.

We could have introduced the push button in the initial machine, but introducing it later allows us to structure the model and makes it easier to understand and navigate.

We will realize this feature by introducing a new boolean variable for the push button. We will introduce an event that notifies the model that a push button has been pressed. Upon allowing the pedestrians to cross, we will reset the push button. This is a simplification of the problem. In practice, a lot would depend on the controller’s capabilities. We would have to consider things like how the push button notification gets to the controller software and how the pressing/depressing sequence is handled. In this example, the event directly sets the controller’s state. This demonstrates the concept of feature refinement without introducing too much complexity for a tutorial example.

As in the previous section, we create a new refinement mac2 by right-clicking on mac1 and selecting Refine. A stub is generated that contains the events from the abstract machine. We simply add a new variable for the push button (including typing and an initialisation clause). We also introduce an event that sets the button. This event doesn’t work while the pedestrians have a green light.

VARIABLES

INVARIANTS

EVENTS

Initialisation

extended

begin

end

Event

push_button

when

then

end

END

Now we need to integrate the push button with the traffic light logic:

• Upon pressing the button, the pedestrians must eventually get a green light.

• At some point, the button variable must be reset.

As we will see in the following discussion, this be more tricky than it first appears. For now, we will introduce a guard preventing the car lights from turning green when the button is true, and we will reset the button when the pedestrian lights turn red:

Event

set_peds_red

extends

set_peds_red

begin

end

Event

set_cars_colours

extends

set_cars_colours

where

end