我面前有一个由不同模块（文件）组成的Alloy模型 . 主模块（包含命令的模块）不包含任何签名声明，只包含命令和一些事实 .
该模型强制只有一个实例可能是可满足的，但在分析之后，找到了几个可满足的实例 . 我调查了生成的实例之间的差异，发现Univ签名神奇地出现（除了内置的univ签名） . 生成的每个实例之间的差异来自属于该神秘添加的原子数 .
将签名添加到主模块后，Univ签名消失 . 当包含执行的命令的模块中没有找到签名声明时，Alloy分析器似乎自己添加了此签名 . Is this behavior generally desired ? If so, why ?
重现此行为的最简单方法是使模块仅包含：run {}
1 回答
我相信这个特例是一个错误 . 最初的动机是，当你没有定义sigs（根本没有），并且只想检查内置关系中的某些属性（例如，
unit，iden，none），除非存在sig，否则分析器赢了't be able to produce instances with more than 0 atoms. That' s为什么在这些情况下会自动生成Univsig . 当前的实现无法检查导入的模块是否定义了任何sigs，因此在这些情况下，正如您已经意识到的那样，您最终得到了神秘的Univsig . 您还正确地指出，一个简单的解决方法是将虚拟空sig添加到定义命令的模块，例如，您还应该检查最新的实验版本，因为这个bug可以在那里修复（但不确定） .