迭代過合金關係

我有以下特徵：迭代過合金關係

open util/ordering [Graph] as chain 

sig Graph { elements : set Node} 
sig Node {} 
sig Connexion {path : Node -> Node} 
fact { all c : Connexion | #dom[c.path] = 1} 
fact { no c : Connexion | dom[c.path] in ran[c.path]}

凡路徑是一個源節點和一個或多個接收節點之間的聯接。連接只有一個源，源不在連接器中。這些部件屬於較大的複雜合金模型。

這裏是我的問題：當我想遍歷路徑：

all p : C1.path | one c : C2 | C2.path = this/associatedPath[p]

其中C1和C2是2個不同的組返回映射路徑參數路徑連接和associatedPath函數。

重點是當我只是嘗試在一個單獨的模型只是這個部分，它的工作原理。但是當我嘗試在更大的模型，可以返回我：

Analysis cannot be performed since it requires higher-order 
quantification that could not be skolemized.

有什麼事情不該做，當一個疊代的關係？我也嘗試將量詞全部改爲一些，但每次指向一個元組時，解算器都會返回此錯誤。有什麼辦法可以手動調整它嗎？是否有任何理由，我不能操縱表達式中的關係？

在此先感謝。

來源

2013-10-29 user2858691

你說：「一條路徑是源節點和一個或多個宿節點之間的連接」。你的意思是「連接是一條道路......」？無論哪種方式，也許你的Connexion的簽名可以改寫

sig Connexion {from: Node, to: set Node}

這將極大地降低了複雜性。它可能無法消除滑行問題。爲了解決這個你應該在量化聯接：

all c: Connexion | ...

來源

2013-10-30 12:46:34

是的，一個接頭是一個路徑。你說：「這將大大降低複雜性」。將連接表示爲2個部署的簽名，而不是表示爲具有節點之間關係的簽名。通常這兩個簽名應該是相當的，不是嗎？作爲合金使用關係代數，如同路徑關係，或者像你表達它的2個關係1一樣，將關係表示爲與2的arity關係更好？什麼是複雜性影響？對解決性能有沒有影響？在這些情況下是否有任何良好的做法？ – user2858691

迭代過合金關係

回答

相關問題