Property 1: LTL for INCA-generated SPIN Input

Part (a)

Refinement, part (a): Artist a1 never registers for event e1 if she is already registered for e1.

Pattern: Absence

Scope: Global (P is false globally.)

LTL Template: []!P

Predicates:

   P = isregistereda1e1 && beforeregistera1e1

[]!(isregistereda1e1 && beforeregistera1e1)

Embedded predicates:

Defined predicates: isregistereda1e1 beforeregistera1e1

See the INCA-generated SPIN input for this property.

See the Never clause generated by SPIN from this LTL formula

Part (b)

Refinement, part (b): Artist a1 never unregisters for event e1 unless she is already registered for e1.

Pattern: Absence

Scope: Global (P is false globally.)

LTL Template: []!P

Predicates:

   P = !isregistereda1e1 && beforeunregistera1e1

[]!(!isregistereda1e1 && beforeunregistera1e1)

Embedded predicates:

Defined predicates: isregistereda1e1 beforeunregistera1e1

See the INCA-generated SPIN input for this property.

See the Never clause generated by SPIN from this LTL formula

Up to Property 1: Artists register and unregister properly

Forward to Property 2: INCA-SPIN

Back to Property 0: INCA-SPIN