Property 2: LTL for Native SPIN

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.

Pattern: Existence

Scope: Between (P becomes true between Q and R.)

LTL Template: []((Q & <>R) -> (!R U P))

Predicates:

   P = notifyclienteventa1e1
   Q = afternotifyartistse1 && isregistereda1e1
   R = notifyartistse1 || notifyartistse2

[](((afternotifyartistse1 && isregistereda1e1) && <>(notifyartistse1 || notifyartistse2)) -> (!(notifyartistse1 || notifyartistse2) U notifyclienteventa1e1))

See the Never clause generated by SPIN from this LTL formula

Up to Property 2: Dispatcher notifies before receiving again

Forward to Property 3: Native SPIN

Back to Property 1: Native SPIN