2.8.1 Data Refinement

We will continue the example from Section 2.4, where we built a simplified model of a traffic light controller. The model was simplified because we abstracted the traffic lights to TRUE and FALSE and a number of features were still missing.

We will introduce data refinement in this section. The objective is to create a mapping between the abstract traffic light values and actual colours. Figure 2.13 depicts our mapping for the traffic light.

Figure 2.13: Mapping between Abstract and Concrete Events

For simplicity, the traffic light for pedestrians consists of only two lights: red and green.

We break this problem into two steps:

1. Create a context with the data structures for the colours.

2. Create a refinement of the existing model that sees the new context and refines the boolean states into colours.