合金 - ＃和詮釋

我是合金的新手，並想了解＃如何與詮釋的限制工作。考慮以下的簡單模型的無向圖，沒有自循環：合金 - ＃和詮釋

sig Node { 
nearBy : set Node 
} 
fact { 
    no iden & nearBy // irreflexive 
    ~nearBy in nearBy // symmetric 
} 
pred connected[nodes : set Node ] { 
    all n: Node | Node in n.*nearBy 
} 
pred ringTopology[nodes : set Node ] { 
connected[nodes] 
all n: nodes | #n.nearBy = 2 
} 
run { // (1) 
    ringTopology[Node] 
} for exactly 5 Node 
run { // (2) 
    ringTopology[Node] 
} for exactly 5 Node, 5 Int

如果我執行上述（1）的一些解決方案示出違反ringTopology，例如在＃n.nearBy = 2限制對於同一個例子，在評估者中，我得到#Node4.nearby = -4（減4！）。這不會發生（2），我得到一個獨特和正確的解決方案（具有環形拓撲的10節點圖形）。

感謝，愛德華

是否使用的是合金版本

來源

2016-05-23 edrdo

？由於整數溢出，您看起來像獲得該解決方案。最新版本的Alloy（Alloy 4.2_2015-02-22）具有「防止溢出」選項（選項 - >防止溢出），防止這種情況發生。

來源

2016-05-24 00:34:31

謝謝。我使用Alloy 4.2，將選項>禁止溢出設置爲yes，並在Fedora Linux上運行Java 8運行時。如果我將禁止溢出設置爲否，錯誤不會發生，這是你的意思（我期待的反過來）？我也嘗試了MacOS上的例子，同樣的事情發生。 – edrdo

Alloy4.2中有一個關於基數和溢出的已知錯誤;在合金4.2_2015-02-22中修正了錯誤;當「防止溢出」設置爲「是」時，運行（1）命令應該可以正常工作（只用Java 8試過）。 –

合金 - ＃和詮釋

回答

相關問題