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

Re: [tlaplus] Running TLC on Graph module from Specifying Systems

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.


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/5d5fb5b4-53d9-ab5d-7822-1d9a59c872c6%40lemmster.de.