Running TLC on Graph module from Specifying Systems

[Leroy van Engelen]

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

[Markus Kuppe]

On 26.05.20 00:31, Leroy van Engelen wrote:
>
> 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).

Hi Leroy,

in the other mail thread, Stephan suggests to redefine Seq as
UNION{[1..n -> S]: n \in 0..N} in the TLC model to avoid changing the
original spec.

Markus