Property 7: CTL for INCA-generated SMV 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.

Part (a)

Pattern: Existence

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

CTL Template: AG(Q -> !E[!P U R])

Predicates:

   P = notifyclienteventa1e1
   Q = registereda1a2e1 & notifyartistse1
   R = notifyclienteventa2e1

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

Embedded predicates: notifyartistse1 notifyclienteventa2e1 notifyclienteventa1e1

Defined predicates: registereda1a2e1

See the INCA-generated SMV input for this property.

Part (b)

Pattern: Universality

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

CTL Template: AG(Q -> !E[!R U (!P & !R)])

Predicates:

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

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

Embedded predicates: registera2e1

Defined predicates: registereda1a2e1 isregistereda1e1 beforeunregistera1e1 beforeunregistera2e1

See the INCA-generated SMV input for this property.

Up to Property 7: Dispatcher notifies artists in order

Forward to Property 8: INCA-SMV

Back to Property 6: INCA-SMV