DESCRIPTION
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.
SPECIFICATION
Up to Chiron Decomposed Dispatcher (2 artists, 2 events)
Forward to Property 4
Back to Property 2