- MACHINE
Celebrity_2
- REFINES
Celebrity_1
- SEES
Celebrity_c0
- VARIABLES
- INVARIANTS
- EVENTS
- Initialisation
- begin
- end
- Event
celebrity
- refines
celebrity
- when
- with
- then
- end
- Event
remove_1
- refines
remove_1
- any
- where
- with
- then
- end
- Event
remove_2
- refines
remove_2
- any
- where
- with
- then
- end
- END