用合金写断言答案

【问题标题】：Writing assertions in alloy用合金写断言
【发布时间】：2015-09-15 11:33:16
【问题描述】：

我在 Alloy 中对基于基数的特征模型进行建模，允许创建多个特征实例。

所以我的合金模型具有特征模型本身、特征和实例的签名。 Feature-Model 有一组Features和一组Instances（配置，包含所有Features的所有Instances）。一个特征有一组实例和一个包含特征允许多重性的间隔（使用下限和上限）。现在我试图在特征的间隔中找到整数，任何配置都不会满足。

我尝试了许多不同的解决方案，但目前都没有。例如这个断言：

assert featureInstanceCardinality{
    all f: Feature, d: Int - 0 | some c: FM.config | IsPossibleCardinality[f, d] => (#(f.instances & c) = d)
}

在我看来应该导致正确的解决方案（对于每个 Feature f 和每个 Integer d，如果 d 是 f 的可能多重性，则至少存在一个配置 c，其中 f 有 d 个实例）。不幸的是，这会为每个功能的每个可能数量的实例返回反例。

任何人都可以解释为什么会发生这种情况，或者是否有可能我正在尝试做什么？在这种情况下，我非常感谢您的帮助。

【问题讨论】：

这个问题恕我直言，因为您没有提供足够的模型让我们知道发生了什么，所以这个问题仍未得到解答。如果您仍在寻求帮助，请编辑您的问题 :-)

标签： alloy

【解决方案1】：

一个明显的问题是签名 Int 包含负数，所以你的断言

assert featureInstanceCardinality{
  all f: Feature, d: Int - 0 | 
    some c: FM.config | 
      IsPossibleCardinality[f, d] 
      => (#(f.instances & c) = d)
}

似乎声称(f.instances & c) 中的原子数可能是-2，如果IsPossibleCardinality[f,-2] 为真。所以如果IsPossibleCardinality错误地持有一些负数，那将导致断言失败。

只有在您给出所遇到问题的完整工作示例时，才有可能获得更完整的答案。

【讨论】：