Property 1: LTL for Native SPIN

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 && registera1e1

LTL Formula:

[]!(isregistereda1e1 && registera1e1)

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 && unregistera1e1

LTL Formula:

[]!(!isregistereda1e1 && unregistera1e1)

See the Never clause generated by SPIN from this LTL formula

Up to Property 1: Artists register and unregister properly

Forward to Property 2: Native SPIN

Back to Property 0: Native SPIN