Property 6: LTL for INCA-generated SPIN Input

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)

Embedded predicates: notifyclienteventa1e1

Defined predicates: isregistereda1e1

See the INCA-generated SPIN input for this property.

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

Back to Property 5: INCA-SPIN