以下模型没问题，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
edit2：下面的谓词有效 . 如果我为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
也应该工作！
1 回答
如果扩展另一个签名的每个签名都有一个明确定义的范围，（你给出的小例子就是这种情况，那么分析器“足够聪明”就能理解顶级签名的范围至少等于分区的一些签名范围 .
在现在你不给任何特定签名范围的情况下，我假设分析器将无法处理顶部签名的范围，如下所示，顶级签名因此将具有您给出的全局范围作为范围 .