DESCRIPTION
Requirement: Dispatcher never gives an event to an artist that is not registered for it.
We will concern ourselves with the verification of this requirement
for a particular artist (a1
) and a particular event
(e1
):
Refinement: Dispatcher never gives event
e1
to artist a1
if a1
is not
registered for e1
.
SPECIFICATION
Up to Chiron Original Dispatcher (2 artists, 2 events)
Forward to Property 7
Back to Property 5