iterating over Alloy relation

Question

I have the following signatures :

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]}

Where a path is the connexion between a source node and one or multiple sink nodes. There is only one source for a connexion and a source is not in the sinks. These parts belongs to a bigger complicated alloy model.

Here is my problem : When I want to iterate over paths with :

all p : C1.path | one c : C2 | C2.path = this/associatedPath[p]

Where C1 and C2 are 2 distinct sets of connections and associatedPath a function that return the mapping path to the parameter path.

The point is when I just try with just only this part in a separate model, it works. But when I try in the bigger model it returns me :

Analysis cannot be performed since it requires higher-order
quantification that could not be skolemized.

Is there any things not to do when one iterate over relation? I also tried to change the quantifier all to some but each time I refer to a tuple, the solver returns me this error. Is there any way to skolemize it manually? Is there any reason that I cannot manipulate relation in expression?

Thanks in advance.

Answer 1

You say: "a path is the connexion between a source node and one or multiple sink nodes". Do you mean a "connexion is a path..."? Either way, perhaps your Connexion signature can be rewritten

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

That will dramatically reduce the complexity. It may not eliminate the skolemization problem. To address that you should quantify over Connexion:

all c: Connexion | ...