Property 1: CTL for INCA-generated SMV Input

Part (a)

Refinement, part (a): Artist a1 never registers for event e1 if she is already registered for e1.

Pattern: Absence

Scope: Global (P is false globally.)

CTL Template: AG !P

Predicates:

   P = isregistereda1e1 & beforeregistera1e1

[]!(isregistereda1e1 & beforeregistera1e1)

Embedded predicates:

Defined predicates: isregistereda1e1 beforeregistera1e1

See the INCA-generated SMV input for this property.

Part (b)

Refinement, part (b): Artist a1 never unregisters for event e1 unless she is already registered for e1.

Pattern: Absence

Scope: Global (P is false globally.)

CTL Template: AG !P

Predicates:

   P = !isregistereda1e1 & beforeunregistera1e1

AG !(!isregistereda1e1 & beforeunregistera1e1)

Embedded predicates:

Defined predicates: isregistereda1e1 beforeunregistera1e1

See the INCA-generated SMV input for this property.

Up to Property 1: Artists register and unregister properly

Forward to Property 2: INCA-SMV

Back to Property 0: INCA-SMV