Property 1: Artists register and unregister properly

DESCRIPTION

Requirement: An artist never registers for an event if she is already registered for that event, and an artist never unregisters for an event unless she is already registered for that event.

We will concern ourselves with the verification of this requirement for a particular artist (a1) and a particular event (e1). We will also split the requirement into two parts.

Refinement, part (a): Artist a1 never registers for event e1 if she is already registered for e1.

Refinement, part (b): Artist a1 never unregisters for event e1 unless she is already registered for e1.

SPECIFICATION

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

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

Forward to Property 2

Back to Property 0