---- MODULE Graph ----
LOCAL INSTANCE Naturals
LOCAL INSTANCE Sequences
Path(G) == {p \in Seq(G.node) : /\ p /= <<>>
/\ \A i \in 1..(Len(p) - 1): <<p[i], p[i+1]>> \in G.edge}
====
Path([ node |-> {0,1,2}, edge |-> {<<0,0>>, <<0, 2>>}])
Attempted to enumerate { x \in S : p(x) } when S:Seq({0, 1, 2})is not enumerable