Property 2: Dispatcher notifies before receiving again

DESCRIPTION

Requirement: If an artist is registered for an event and the dispatcher receives this event, it will not receive another event before passing this one to the artist.

We will concern ourselves with the verification of this requirement for a particular artist (a1) and a particular event (e1):

Refinement: If a1 is registered for e1 and the dispatcher receives e1 from the adt_wrapper then it will not accept another event from the adt_wrapper before passing e1 to a1.

SPECIFICATION

• Native SPIN
• INCA-SPIN
• INCA-SMV
• INCA
• FLAVERS

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

Forward to Property 3

Back to Property 1