Home Articles

在模块化项目中使用add函数

Asked
Viewed 1660 times
0

我用合金建模了我的项目,我想将运行部分与项目的建模部分分开 . 在某些事实和谓词中,我在基数比较中使用了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 Answer

  • 3

    如果我没有弄错的是union运算符,因此不能用于执行添加 .

    你使用的是哪种合金?

    我认为add [Int,Int]函数最近被添加,之前它是加号[int,int] .

    您可能想尝试加上[Int,Int]并查看它是否解决了您的问题 . 否则,访问您的模型会很高兴 . 也许错误来自其他地方 .

Related