Place/transition nets modeling (1)
Consider the following diagram showing a crossroads with traffic lights.
In terms of behavior four traffic lights can be distinguished: the pedestrian traffic lights F1 and F2 as well as the traffic lights KFZ1 and KFZ2 for vehicles.
The following place/transition net is given for describing the behavior of traffic lights KFZ1 and KFZ2:
The net represents the behavior of two Dutch traffic lights. Places safe1 and safe2 ensure that the traffic lights behave safe and fair. Safe means that at least one traffic lights shows a red light at any time. Fair means that the traffic lights alternate in showing green light.
a) Expand the given place/transition net by incorporating the two pedestrian traffic lights F1 and F2. Each of these traffic lights should be represented by two places (one for the red light and one for the green light). The traffic light F1 (F2) should show the green light only as long as KFZ1 (KFZ2) shows the green light. Otherwise it should show the red light.
b) Expand the given place/transition net by incorporating one pedestrian traffic light the signal of which applies to both directions of the corssroads. The net should be safe and fair. I.e. the pedestrian traffic light is only allowed to show the green light as long as the other two traffic lights show the red light. Furthermore, the three traffic lights should alternate in showing the green light.
c) Consider a German traffic light. It is different to a Dutch traffic light as it has a fourth phase: After the red light is shown, the red and the yellow light are shown at the same time.
- Create a place/transition net that could behave like a German traffic light. The net should contain three places, one for each color. All state transitions should be supported.
- Create a place/transition net that exactly behaves like a German traffic light. Make sure that all state transitions are correct.
- Create the reachabiligy graph for the last net. Are there dead states?
More information on place/transition nets can be found in the book in chapter 4.2.