Property 3: LTL for Native SPIN

Refinement: Dispatcher does not notify any artists of e1 until it receives e1 from the ADT.

Pattern: Precedence

Scope: Global (S precedes P globally.)

LTL Template: <>P -> (!P U (S & !P))

Predicates:

   P = notifyclienteventa1e1 || notifyclienteventa2e1
   S = notifyartistse1

<>(notifyclienteventa1e1 || notifyclienteventa2e1)-> (!(notifyclienteventa1e1 || notifyclienteventa2e1) U (notifyartistse1 && !(notifyclienteventa1e1 || notifyclienteventa2e1)))

See the Never clause generated by SPIN from this LTL formula

Up to Property 3: Dispatcher notifies only after receiving

Forward to Property 4: Native SPIN

Back to Property 2: Native SPIN