Hi,
Section 11.1.2 from the Specifying Systems book describes a Graph module. To try it out I use the following code:
---- 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}
====
Trying it out using Evaluate Constant _expression_:
Path([
node |-> {0,1,2},
edge |-> {<<0,0>>, <<0, 2>>}
])
Results in the following error:
Attempted to enumerate { x \in S : p(x) } when S:
Seq({0, 1, 2})
is not enumerable
Is it to be expected that the Graph module from the book is not runnable in TLC? Reading the thread in https://groups.google.com/d/msg/tlaplus/wmkxVexaFK4/zFOm4eOoCgAJ it is indeed not possible. I now implemented something similar using a recursive operator that does not depend on Seq. Is that the way to go or is there a way to get the Graph code to work (which looks more elegant and idiomatic to me).
Thanks,
-Leroy