alloy - 了解合金中的约束

Question

我正在为我的公司黑客马拉松探索 Alloy。我们有一个复杂的数据模型，我的目标是生成正确示例的图片，以便新员工可以看到它们并了解我们的应用程序。我设法偶然发现并生成了一些图片，但我无法表达以下想法：

角色可以授予对一个或多个字段的访问权限。用户具有一个或多个角色，并且可以访问零个或多个字段。当且仅当用户具有授予对该字段的访问权限的角色时，用户才能访问该字段。

这是语法错误的众多尝试之一；希望它表明我对合金的工作原理有什么误解。

sig Role { grantsAccess: some Field }
sig User { 
    has: some Role,
    canAccess: Field    
}{
    all u: User |
    f: Field in u.canAccess iff some r: Role in u.has | f in r.grantsAccess
}

谢谢！

标签： alloy

Answer 1

-- A role can grant access to one or more fields. 

sig Role { grant : some Field } 
sig Field {}

-- A user has one or more roles, 
-- and can access zero or more fields. 

sig User {
    roles : set Role
}

-- A user can access a field    

pred User.canAccess[ field : Field ] {

    -- if and only if the user has a role 
    -- which grants access to that field.

    some role : this.roles | field in role.grant

    // alternative:
    // some ( this.roles & grant.field )
}

run ex1 { 
    some u : User, f : Field {
        u.canAccess[f]
    }
}