Property 6: LTL for Native SPIN

Refinement: Dispatcher never gives event e1 to artist a1 if a1 is not registered for e1.

Pattern: Absence

Scope: Global (P is false globally.)

LTL Template: []!P

Predicates:

   P = notifyclienteventa1e1 && !isregistereda1e1

[]!(notifyclienteventa1e1 && !isregistereda1e1)

See the Never clause generated by SPIN from this LTL formula

Up to Property 6: Dispatcher does not notify wrong artists

Forward to Property 7: Native SPIN

Back to Property 5: Native SPIN