余数类型的合金语法？答案

【问题标题】：Alloy syntax for remainder types?余数类型的合金语法？
【发布时间】：2014-02-25 18:29:09
【问题描述】：

有没有一种直接的方法来表示 Alloy 中的余数类型，而不必显式地减去联合的所有子类型？例如，在：

sig Test {}
one sig A, B extends Test {}

我希望能够通过简写方式引用表达式Test-(A+B)，无需在每次Test 被新的sig 扩展时都更改。虽然这只是语法糖，但它可以帮助我在重构模型时避免错误。

【问题讨论】：

标签： alloy

【解决方案1】：

您可以引入一个表示余数的集合，如下所示：

abstract sig Test {}
sig Remainder extends Test {}
one sig A, B extends Test {}

这会将Test 原子集划分为三个子集，Remainder 等同于Test - (A + B)。例如，如果您后来决定通过添加 one sig C 来扩展 Test，Remainder 仍会为您提供余数集。

【讨论】：

【解决方案2】：

我已经有一段时间没有使用 Alloy 了，但我认为它不可能按照您想要的方式使用。但是，您可以将联合重构到模型中的一个位置。示例：

sig Test {}
one sig A, B extends Test {}

fun Remainder : set Test {
    Test - (A+B)
}

run { some Remainder } for 5

您使用一个函数定义一个关系，这里称为Remainder，它是通过从基类型中减去所有子类型的联合来定义的。
每次向模型添加新的子类型时，只需记住将其添加到 Remainder 的定义中即可。

在整个模型中，您只需参考Remainder 即可获得所有纯 Test 原子，就像我在run 命令中的匿名谓词中使用的那样。

【讨论】：

【解决方案3】：

如果您希望定义包含扩展 Test 的任何新 sig，则可以使用 Alloy 鲜为人知的 meta capabilities，它允许您通过特殊集合 sig$ 遍历 sig。

例如，您可以执行以下操作：

fun Remainder [] : set Test {
  {t : Test | all sig : sig$ | sig = Test$ || t not in sig.value}
}

【讨论】：