Property 5: Dispatcher does not block if no one is registered

DESCRIPTION

Requirement: Dispatcher does not block ADT if no one is registered.

Refinement: If no artists are registered for event e1, dispatcher does not notify any artist of e1.

SPECIFICATION

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

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

Forward to Property 6

Back to Property 4