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
Predicates:
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