Property 3: Dispatcher notifies only after receiving


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 (e1):

Refinement: Dispatcher does not notify any artists of 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