\* TLA+ Configuration file for RegistrationKey specification

CONSTANTS
    MAX_STRING_LENGTH = 50
    ASCII_MIN = 32
    ASCII_MAX = 122

SPECIFICATION Spec

INVARIANTS
    TypeInvariant
    ValidInputs
    PhaseOrder
    FinalKeyLength
    NoEmptyKey

PROPERTIES
    Termination

\* Constraint to limit state space for model checking
CONSTRAINT
    /\ Len(firstName) <= 10
    /\ Len(lastName) <= 10
    /\ Len(productName) <= 15
    /\ Len(email) <= 20