SPECIFICATION Spec
CONSTANTS
    Users = {u1, u2}
    Usernames = {n1, n2}
    Passwords = {p1, p2}
    MaxAttempts = 3
    NoAuth = NoAuth
INVARIANTS
    TypeOK
    UsernamesUnique
    AtMostOneCredPerUser
    AuthSound
CHECK_DEADLOCK FALSE