合金 - ＃和诠释

alloy

2016-05-23 74 views 0 likes

我是合金的新手，并想了解＃如何与诠释的限制工作。考虑以下的简单模型的无向图，没有自循环：合金 - ＃和诠释

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试过）。 –

合金 - ＃和诠释

回答

相关问题