关于亚型属性的推理

Question

我发现自己经常遇到以下情况：

sig Property {}

abstract sig Unit {
  property: some Property
}


sig Hardware, Software, Services extends Unit {}

fact  {
  no Hardware.property & Software.property
  no Hardware.property & Services.property
  no Software.property & Services.property
}

也就是说，我有一个抽象的签名，它声明了一个属性，以及一些扩展该签名的子类型。我想确保子类型之间的属性property没有重叠。

Hardware的两个实例将被允许共享property值，但Hardware和Software实例永远不应该被允许具有共同属性。

我真的宁愿不必写那样的fact。如果我添加第四种Unit，我很容易搞砸事实。

这感觉我需要能够反省类型，但我不知道有任何设施可以做到这一点。

有什么建议？

Answer 1

它可能不是最优雅的解决方案，但您可以为每个单元子类型定义属性子类型。

这样，您就不需要手动编写交叉产品，从而减少错误:-)。

abstract sig Property {}

abstract sig Unit {
  property: some Property
}

sig Hardware, Software, Services extends Unit {}
sig PropHard , PropSoft, PropServ extends Property{}

fact {
    Hardware.property in PropHard
    Software.property in PropSoft
    Services.property in PropServ
}