合金-#和Int

Question

我是一个在合金的新手，并想了解#如何与国际贸易的限制有关的工作。考虑没有自循环的无向图的以下简单模型：

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)，一些解决方案违反了#n.nearBy =2在ringTopology中的限制。

对于同一个例子，在计算器中我得到#Node4.附近= -4 (- 4!)。在(2)中，我得到了一个唯一且正确的解(具有环拓扑的10节点图)，这是不可能的。

谢谢，爱德华多

Answer 1

你用的是哪一种合金？看起来，由于整数溢出，您得到了该解决方案。最新版本的合金(2015-02-22)有“防止溢出”选项(选项->防止溢出)，应防止这种情况发生。