Property 8: LTL for Native SPIN

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 event e1 when the size of the array used to store artists registered for e1 is equal to 2.

Instead of formulating this property, we use SPIN's built-in ability to check that no arrays go out of bounds. This is done by default, unless the analyzer pan.c is compiled with the option -DNOBOUNDCHECK.

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