SPECIFICATION Spec
CONSTANTS
    Users = {u1, u2, u3}
    Passwords = {p1, p2, p3}
    MaxAttempts = 3
    NoAuth = NoAuth
INVARIANTS
    TypeOK
    PasswordsUnique
    AtMostOneCredPerUser
    AuthSound
CHECK_DEADLOCK FALSE