在模塊化項目中使用添加功能

我已經使用合金模擬了我的項目，並且我想將運行部分與我的項目的建模部分分開。在一些事實和謂詞中，我使用add函數進行基數比較。下面是一個例子：在模塊化項目中使用添加功能

#relation1 = add[ #(relation2), 1]

當運行部分和模型部分是在同一個文件中的所有成功運行。

但是，當我在2個文件將它們分開，我有以下的語法錯誤：

The name "add" cannot be found.

我認爲這需要打開整數模塊那裏有一個附加功能，所以我打開它，它的模型部分的標題。但是然後運行時問我指定這個/ 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」this/Univ「」錯誤。

我應該怎麼做，要使其工作？

來源

2014-01-08 user2858691

如果我沒有記錯+是工會運營商，因此不能被用來進行補充。

您正在使用哪種版本的合金？

我想添加[INT，INT]最近加入的功能，之前它曾經是加[INT，INT]。

你可能想嘗試加[INT，INT]，看看它是否解決您的問題。否則，很高興能夠訪問您的模型。也許錯誤來自其他地方。

來源

2014-01-08 16:52:54

我使用合金4.2。你是對的+是工會運營商。我錯了。我嘗試了plus操作符，並且當命令和模型與add操作符在同一個文件中工作時。但是，當我嘗試在單獨的文件中使用該命令時，似乎使用關鍵字open打開的文件既無法訪問添加，也無法訪問正運算符。 – user2858691

我認爲，如果您分享有問題的模型，那麼診斷哪些問題會更容易。我實際上很難通過將運行部分與模型部分分開來表示您的意思。 –

顯式打開util/integer應該可以工作。「大學」的缺失範圍是一個奇怪的錯誤，我也想看到造成它的模型。 –

在模塊化項目中使用添加功能

回答

相關問題