![]()
- MACHINE
mac1
- REFINES
mac
- SEES
ctx1
- VARIABLES
- INVARIANTS
![]()
![]()
- EVENTS
- Initialisation
- begin
![]()
![]()
- end
- Event
set_peds_green
![]()
- refines
set_peds_go
- when
![]()
- then
![]()
- end
- Event
set_peds_red
![]()
- refines
set_peds_stop
- begin
![]()
- end
- Event
set_cars
![]()
- refines
set_cars
- any
- where
![]()
![]()
- then
![]()
- end
- END