合金 - this/Univ 的范围，订购，“开放”声明答案

【问题标题】：Alloy - scope for this/Univ, ordering, "open" statement合金 - this/Univ 的范围，订购，“开放”声明
【发布时间】：2016-05-27 09:09:17
【问题描述】：

我在以下类型的合金 (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 对我很有用。

谢谢，爱德华多

【问题讨论】：

标签： alloy

【解决方案1】：

这是一个合金“设计错误”。决定在模块中未定义签名时出现 Univ 签名，以检查内置关系（例如，unit、iden、none）上的某些属性。

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

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

更多信息请见this question

【讨论】：