Re: [tlaplus] Initial state doesn't satisfy type invariant

[Tim Leonard <Tim@xxxxxxxxxxxxx>]

Yes. The second is what I’m now using.

Thank you for the help.

On Dec 8, 2020, at 12:19 AM, Srikumar Subramanian <srikumar.subramanian@xxxxxxxxxxxx> wrote:

I guess you meant this? -

edges_stack \in Seq(UNION {[X -> Nodes] : X \in SUBSET Labels})

or perhaps -

edges_stack \in Seq(UNION {[X -> Nodes] : X \in {1..n : n \in Labels}})

?

--
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/AAF60449-8329-4E99-B186-9053CF1908B0%40TimLeonard.us.