Home Articles

当模块为空时,Univ签名会显得神奇

Asked
Viewed 349 times
4

我面前有一个由不同模块(文件)组成的Alloy模型 . 主模块(包含命令的模块)不包含任何签名声明,只包含命令和一些事实 .

该模型强制只有一个实例可能是可满足的,但在分析之后,找到了几个可满足的实例 . 我调查了生成的实例之间的差异,发现Univ签名神奇地出现(除了内置的univ签名) . 生成的每个实例之间的差异来自属于该神秘添加的原子数 .

将签名添加到主模块后,Univ签名消失 . 当包含执行的命令的模块中没有找到签名声明时,Alloy分析器似乎自己添加了此签名 . Is this behavior generally desired ? If so, why ?

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

1 Answer

  • 3

    我相信这个特例是一个错误 . 最初的动机是,当你没有定义sigs(根本没有),并且只想检查内置关系中的某些属性(例如, unitidennone ),除非存在sig,否则分析器赢了't be able to produce instances with more than 0 atoms. That' s为什么在这些情况下会自动生成 Univ sig . 当前的实现无法检查导入的模块是否定义了任何sigs,因此在这些情况下,正如您已经意识到的那样,您最终得到了神秘的 Univ sig . 您还正确地指出,一个简单的解决方法是将虚拟空sig添加到定义命令的模块,例如,

    sig Dummy {}
    fact { no Dummy }
    

    您还应该检查最新的实验版本,因为这个bug可以在那里修复(但不确定) .

Related