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.)
LTL Template: [](!P)
Predicates:
P = e1szEQ2 && (beforeregistera1e1 || beforeregistera2e1)LTL Formula:
[]!(e1szEQ2 && (beforeregistera1e1 || beforeregistera2e1))
Embedded predicates:
Defined predicates:
beforeregistera1e1 beforeregistera2e1 e1szEQ2
See the INCA-generated SPIN input for this property.
See the Never clause generated by SPIN from this LTL formula
Up to Property 8: Size of registration list does not exceed 2
Forward to Property 9: INCA-SPIN
Back to Property 7: INCA-SPIN