我用合金建模了我的项目，我想将运行部分与项目的建模部分分开 . 在某些事实和谓词中，我在基数比较中使用了add函数 . 这是一个例子：
#relation1 = add[ #(relation2), 1]
当运行部件和模型部件在同一文件中时，所有工作都成功 .
但是当我将它们分成2个文件时，我有以下语法错误：
The name "add" cannot be found.
我认为需要打开整数模块，其中有一个add函数，所以我把它打开了模型部分的 Headers . 但后来运行时要求我指定此/ Univ的范围 .
You must specify a scope for sig "this/Univ"
这是一个例子：首先是一个模块中的模型
module solo
open util/ordering [A] as chain
//open util/integer
sig A{ b : set B}
fact { all a : A - chain/last | #(a.next.b) = add[ #(a.b), 2]}
sig B{}
然后在另一个模块中运行部分：
module due
open solo
run {#(solo/chain/first.b) = 2 }for 10 B, 5 A
当我这样称它为“无法找到名称添加”错误 . 当我取消注释整数模块打开时，我有“你必须为sig指定一个范围”这个/ Univ“”错误 .
我应该怎么做才能使它有效？
1 回答
如果我没有弄错的是union运算符，因此不能用于执行添加 .
你使用的是哪种合金？
我认为add [Int，Int]函数最近被添加，之前它是加号[int，int] .
您可能想尝试加上[Int，Int]并查看它是否解决了您的问题 . 否则，访问您的模型会很高兴 . 也许错误来自其他地方 .