Property 7: LTL for Native SPIN

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.

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

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 = afterregistera2e1 && isregistereda1e1
   R = unregistera1e1 || unregistera2e1

[]((afterregistera2e1 && isregistereda1e1) -> (registereda1a2e1 U ((unregistera1e1 || unregistera2e1) || []registereda1a2e1)))

See the Never clause generated by SPIN from this LTL formula

Up to Property 7: Dispatcher notifies artists in order

Forward to Property 8: Native SPIN

Back to Property 6: Native SPIN