什么影响 Alloy 的范围？

Question

下面这个模型就可以了，Alloy找实例

abstract sig A{}

sig B extends A{}
sig C extends A{}

run {} for 1 but exactly 1 B, exactly 1 C

这让我明白了范围不受顶级签名 A 的限制，而是受其扩展 B 和 C 的限制。

但是，我有一个很大的模型（在这里张贴它没有意义）只能满足 14 的范围。对于 13 的范围，分析器找不到实例。

当我分析找到的实例时，使用求值器请求 'univ'，我得到一个解决方案，每个签名大约有 5 个原子。只有顶层抽象签名有14个原子

我是否遗漏了有关范围的信息？它会影响签名以外的其他东西吗（例如谓词）？它的行为是否与我假设的玩具示例不同？

为什么我的模型不能模拟 5 的范围？

编辑：如果有人有兴趣看一看，这是我的模型。这是模型转换的结果，这就是为什么易读性是一个问题http://pastebin.com/17Z00wV4

编辑2：下面的谓词有效。如果我运行 5 的谓词但没有明确指定其他范围，则它找不到实例。

run story3 for 5 but exactly 4 World, exactly 4 kPerson, 
   exactly 0 kSoftwareTool, exactly 1 kSourceCode, 
   exactly 1 kDocument, exactly 1 kDiagram, exactly 3 kChange, 
   exactly 1 kProject, exactly 2 coBranch, exactly 1 coRepository, 
   exactly 3 modeConfiguration, exactly 2 modeAtomicVersion, 
   exactly 2 relatorChangeRequest, exactly 0 relatorVerification, 
   exactly 1 relatorCheckIn, exactly 1 relatorCheckOut, 
   exactly 2 relatorConfigurationSelection, 
   exactly 1 relatorModification, 
   exactly 0 relatorRequestEvaluation, exactly 2 relatorMarkup

这个不是（它是相同的谓词，但没有 "exactly" 关键字

run story3 for 5 but exactly 4 World, 4 kPerson, 1 kSourceCode, 
   1 kDocument, 1 kDiagram, 3 kChange, 1 kProject, 2 coBranch, 
   1 coRepository, 3 modeConfiguration, 2 modeAtomicVersion, 
   2 relatorChangeRequest, 1 relatorCheckIn, 1 relatorCheckOut, 
   2 relatorConfigurationSelection, 1 relatorModification, 
   2 relatorMarkup

有人告诉我 Alloy 会在定义的范围内找到任何可能的实例，所以

run story3 for 5

应该也可以！

Answer 1

如果扩展另一个签名的每个签名都有明确定义的范围，（您给出的小示例就是这种情况，那么分析器是 "smart enough" 以了解顶层的范围signature 至少等于分割它的签名的一些范围。

在这种情况下，现在您没有为特定签名提供任何范围，我假设分析器将无法处理顶级签名的范围，如下所述，因此顶级签名将具有作为范围你给的全局的。

什么影响 Alloy 的范围？

What affects Alloy's scope?

alloy