Requirement: Dispatcher does not notify any artist of an event until it receives this event from the ADT.
We will concern ourselves with the verification of this requirement
for a particular artist (
a1) and a particular event
Refinement: Dispatcher does not notify any artists
e1 until it receives
e1 from the ADT.
Up to Chiron Decomposed Dispatcher (2 artists, 2 events)
Forward to Property 4
Back to Property 2