什么影响合金的范围？

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 

这个没有（它是同一个谓词，但没有“确切”关键字

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

如果扩展另一个签名的每个签名都有明确定义的范围，（您给出的小例子就是这种情况，那么分析器“足够聪明”可以理解顶级签名的范围在至少等于划分它的签名的某些范围。

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