Property 2: LTL for INCA-generated SPIN Input

Refinement: If a1 is registered for e1 and the dispatcher receives e1 from the adt_wrapper then it will not accept another event from the adt_wrapper before passing e1 to a1.

Pattern: Existence

Scope: Between (P becomes true between Q and R.)

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

Predicates:

   P = notifyclienteventa1e1
   Q = afternotifyartistse1 && isregistereda1e1
   R = notifyartistse1 || notifyartistse2

[](((afternotifyartistse1 && isregistereda1e1) && <>(notifyartistse1 || notifyartistse2)) -> (!(notifyartistse1 || notifyartistse2) U notifyclienteventa1e1))

Embedded predicates: afternotifyartistse1 notifyclienteventa1e1 notifyartistse1 notifyartistse2

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 2: Dispatcher notifies before receiving again

Forward to Property 3: INCA-SPIN

Back to Property 1: INCA-SPIN