如何为Alloy模型三元关系设置约束：限制Event.rule_properties的Rule归属

你无法在Event的字段声明中直接使用rulesets.rules来约束值域，因为Alloy不支持在字段类型定义里引用同一sig的其他字段的派生集合。正确的做法是通过fact添加全局约束：

sig Factor {}
sig Rule { rule : some Factor }
sig RuleSet { rules : some Rule }
sig EventRuleProperty {}
 
sig Event {
       rulesets : some RuleSet,
       rule_properties :  RuleSet -> Rule -> EventRuleProperty
}

fact RulePropertyValidity {
  all e : Event, rs : e.rulesets, r : Rule, prop : EventRuleProperty |
    (rs -> r -> prop) in e.rule_properties implies r in rs.rules
}

约束解释 #

• 遍历所有事件e、该事件包含的规则集rs、任意规则r和属性prop
• 只要rs->r->prop属于e的rule_properties关系，就强制要求r必须是rs包含的规则（r in rs.rules）

简化写法（可选） #

如果想让约束更完整，还可以额外确保关联的规则集本身属于当前事件的规则集列表：

fact RulePropertyValidity {
  all e : Event, rs : RuleSet, r : Rule, prop : EventRuleProperty |
    (rs -> r -> prop) in e.rule_properties implies (rs in e.rulesets and r in rs.rules)
}

内容的提问来源于stack exchange，提问作者PeterJ