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

*From*: Leroy van Engelen <leroy.vanengelen@xxxxxxxxx>*Date*: Tue, 26 May 2020 00:31:30 -0700 (PDT)

Hi,

Results in the following error:

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

-- 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

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.

**Follow-Ups**:**Re: [tlaplus] Running TLC on Graph module from Specifying Systems***From:*Markus Kuppe

- Prev by Date:
**Re: [tlaplus] How to remove an iterm from a Sequence?** - Next by Date:
**Re: [tlaplus] How to remove an iterm from a Sequence?** - Previous by thread:
**Re: [tlaplus] How to remove an iterm from a Sequence?** - Next by thread:
**Re: [tlaplus] Running TLC on Graph module from Specifying Systems** - Index(es):