# [tlaplus] Running TLC on Graph module from Specifying Systems

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 NaturalsLOCAL INSTANCE SequencesPath(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

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.