Alloy

Question

我在 Alloy (4.2) 规范中遇到以下类型的错误：

You must specify a scope for sig "this/Univ"

这个问题很容易用玩具示例重现：

open util/ordering[State]
open util/integer

sig State { value : Int }

fact {
  first.value = 0
  all s:State, s': s.next | s'.value = plus[s.value, 1]
}

run { } for 5 State, 3 Int

以上都可以。现在，当我在外部文件中定义 State 并使用 open 语句导入它时，我得到 "Univ scope" 错误：

open util/ordering[State]
open util/integer
open State

fact {
  first.value = 0
  all s:State, s': s.next | s'.value = plus[s.value, 1]
}

run { } for 5 State, 3 Int

我尝试了以上几种变体，但均未成功。为什么会发生这种情况，如何解决？在我的项目中，在不同的文件中定义排序模块的目标 sig 对我很有用。

谢谢，爱德华多

Answer 1

这是一个 Alloy "design bug"。决定在模块中没有定义签名时出现 Univ 签名，以便检查一些属性内置关系（例如，unit、iden、none）。

你有很多方法可以解决这个问题，这里是一个选择：

您可以在运行命令的末尾添加“,0 Univ”
您可以在 Alloy 模块中添加签名
您可以指定全局范围为零 (run { } for 0 but 5 State, 3 Int )

有关其他信息，请参阅 this question

Alloy - this/Univ 的范围，排序，"open" 语句

Alloy - scope for this/Univ, ordering, "open" statement