Property 7: LTL for INCA-generated SPIN Input

Requirement: If artist a1 registers for event e1 before artist a2 does, then once dispatcher receives e1 from the ADT, it will not notify a2 before notifying a1.

We separate this claim into two parts, each of which must be verified in order to fully verify the claim. Part (a) is essentially a restatment of the claim, but it makes reference to a predicate registereda1a2e1. The purpose of Part (b) is to show that registereda1a2e1 will hold whenever we have had a1 and then a2 register for e1, without either unregistering. Note the slight difference between the predicates in Part (b) and the corresponding ones used for Native SPIN.

Part (a)

Pattern: Existence

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

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

Predicates:

   P = notifyclienteventa1e1
   Q = registereda1a2e1 && notifyartistse1
   R = notifyclienteventa2e1

[](((registereda1a2e1 && notifyartistse1) && <> notifyclienteventa2e1) -> (!notifyclienteventa2e1 U notifyclienteventa1e1))

Embedded predicates: notifyartistse1 notifyclienteventa2e1 notifyclienteventa1e1

Defined predicates: registereda1a2e1

See the INCA-generated SPIN input for this property.

See the Never clause generated by SPIN from this LTL formula

Part (b)

Pattern: Universality

Scope: After-Until (P is true after Q until R.)

LTL Template: [](Q -> P U (R | [](P)))

Predicates:

   P = registereda1a2e1
   Q = registera2e1 && isregistereda1e1
   R = beforeunregistera1e1 || beforeunregistera2e1

[]((registera2e1 && isregistereda1e1) -> (registereda1a2e1 U ((beforeunregistera1e1 || beforeunregistera2e1) || []registereda1a2e1)))

Embedded predicates: registera2e1

Defined predicates: registereda1a2e1 isregistereda1e1 beforeunregistera1e1 beforeunregistera2e1

See the INCA-generated SPIN input for this property.

See the Never clause generated by SPIN from this LTL formula

Up to Property 7: Dispatcher notifies artists in order

Forward to Property 8: INCA-SPIN

Back to Property 6: INCA-SPIN