Property 8: CTL for INCA-generated SMV Input

Refinement: No artist attempts to register for event e1 when the size of the array used to store artists registered for e1 is equal to 2.

Pattern: Absence

Scope: Global (P is false globally.)

CTL Template: AG!P


   P = e1szEQ2 & (beforeregistera1e1 | beforeregistera2e1)

CTL Formula:

AG(!(e1szEQ2 & (beforeregistera1e1 | beforeregistera2e1)))

Embedded predicates:

Defined predicates: beforeregistera1e1 beforeregistera2e1 e1szEQ2

See the INCA-generated SMV input for this property.

Up to Property 8: Size of registration list does not exceed 2

Forward to Property 9: INCA-SMV

Back to Property 7: INCA-SMV