使用关系值创建签名字段是最佳做法吗?

商店有顾客。每个客户都使用其用户名和密码登录商店。

我想创建一个合金函数( fun )当传递凭据(用户ID和密码)时,返回拥有这些凭据的客户:

fun customerWithTheseCredentials[userID: UserID, password: Password]: Customer {
    ???
}

我确信,要做到这一点,我必须以这种方式声明客户签名:

sig Customer {
    credentials: UserID lone -> lone Password
}

通过这种方式创建签名,我可以通过以下方式实现该功能:

fun customerWithTheseCredentials[userID: UserID, password: Password]: Customer {
    credentials.password.userID
}

我是否以这种方式创建了客户签名:

sig Customer {
    userID: UserID,
    password: Password
}

那么我就不能实现这个功能了。你同意吗?

我坚信,设计签名字段时最好使用关系值(例如。, credentials: UserID lone -> lone Password )而不是集合(例如。, userID: UserID ). 你也有这样的信念吗?

以下是我的合金模型:

sig UserID {}
sig Password {}
sig Customer {
    credentials: UserID lone -> lone Password
} 

fun customerWithTheseCredentials[userID: UserID, password: Password]: Customer {
    credentials.password.userID
}

run {}

fact Every_customer_has_a_different_password_userID {
    // Every customer has a different userID
    no disj c, c': Customer | 
        c.credentials.Password = c'.credentials.Password
    // Every customer has one userID/password pair
    all c: Customer |
        one id: UserID |
            one p: Password |
                c.credentials = id -> p
}