我有以下签名：
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？有什么理由我不能在表达中操纵关系吗？
提前致谢。