Property 4: LTL for INCA-generated SPIN Input

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))))

Embedded predicates: notifyartistse1 notifyartistse2 notifyclienteventa1e2 notifyclienteventa2e2

Defined predicates:

See the INCA-generated SPIN input for this property.

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: INCA-SPIN

Back to Property 3: INCA-SPIN