Property 6: Dispatcher does not notify wrong artists


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.


Up to Chiron Decomposed Dispatcher (2 artists, 2 events)

Forward to Property 7

Back to Property 5