[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Running TLC on Graph module from Specifying Systems


Section 11.1.2 from the Specifying Systems book describes a Graph module. To try it out I use the following code:

---- MODULE Graph ----

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_:
  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).



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.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/324527b5-1bcd-4291-bdea-6bfcc7c789ea%40googlegroups.com.