迭代合金关系

Question

我有以下签名：

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.

当一个人迭代关系时，有什么事情不能做吗？ 我也尝试将量词全部更改为一些，但每次我引用一个元组时，求解器都会返回这个错误。 有没有办法手动对其进行sklemize？ 有什么原因我不能在表达式中操纵关系吗？

提前致谢。

Answer 1

您说：“路径是源节点与一个或多个汇节点之间的连接”。你的意思是“连接是一条路径......”？无论哪种方式，也许您的 Connexion 签名都可以重写

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

这将大大降低复杂性。它可能无法消除 skolemization 问题。为了解决这个问题，您应该通过 Connexion 进行量化：

all c: Connexion | ...