Requirement: The size of the linked list used to store IDs of artists registered for an event never exceeds 2.
Refinement: No artist attempts to register for
e1 when the size of the array used to store artists
e1 is equal to 2.
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: Native SPIN
Back to Property 7: Native SPIN