Property 4: LTL for Native SPIN

Requirement: Having received event e1, dispatcher never notifies artists of e2.

Pattern: Absence

Scope: After-Until (P is false after Q until R.)

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

Predicates:

   P = notifyclienteventa1e2 || notifyclienteventa2e2
   Q = notifyartistse1
   R = notifyartistse2

[](notifyartistse1 -> (!(notifyclienteventa1e2 || notifyclienteventa2e2) U (notifyartistse2 || []!(notifyclienteventa1e2 || notifyclienteventa2e2))))

See the Never clause generated by SPIN from this LTL formula

Up to Property 4: Dispatcher notifies of what was received

Forward to Property 5: Native SPIN

Back to Property 3: Native SPIN