Property 8: LTL for INCA-generated SPIN 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.)

LTL Template: [](!P)


   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