Property 3: LTL for INCA-generated SPIN Input

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

Embedded predicates: notifyartistse1 notifyclienteventa1e1 notifyclienteventa2e1

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 3: Dispatcher notifies only after receiving

Forward to Property 4: INCA-SPIN

Back to Property 2: INCA-SPIN