当模块为空时，Univ 签名神奇地出现

Question

我面前有一个由不同模块（文件）组成的合金模型。 主模块（包含命令的模块）不包含任何签名声明，只有一个命令和一些事实。

该模型强制只有一个实例可能是可满足的，但经过分析，会找到几个可满足的实例。 我调查了生成的实例之间的差异，发现 Univ 签名神奇地出现了（除了内置的 univ 签名）。 生成的每个实例之间的差异来自于属于那个神秘添加物的原子数量。

在主模块添加签名后，Univ签名消失了。 当在包含执行命令的模块中找不到签名声明时，Alloy 分析器似乎会自行添加此签名。 这种行为是普遍需要的吗？如果是，为什么？

重现此行为的最简单方法是让模块仅包含：run {}

Answer 1

我相信这种特殊情况是一个错误。最初的动机是，当您（根本）没有定义 sig，并且只想检查内置关系上的某些属性（例如，unit、iden、none）时，除非存在 sig，分析器将无法生成原子数超过 0 的实例。这就是在这些情况下自动生成Univ sig 的原因。当前实现无法检查导入的模块是否定义了任何 sig，因此在这些情况下，正如您已经意识到的那样，您最终会得到神秘的 Univ sig。您还正确地指出，一个简单的解决方法是在定义您的命令的模块中添加一个虚拟的空 sig，例如

sig Dummy {}
fact { no Dummy }

您还应该检查最新的实验版本，因为该错误可能已修复（虽然不确定）。