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

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

Thanks, Stephan; that was a help. The _expression_ you suggested didn’t quite work because it needed square brackets around “X -> Nodes”, and TLC couldn’t enumerate the values, but once you showed me what the problem was, I was able to define and use this constant:

SetsOfLabeledEdges ==
          UNION { [ 1..n -> Nodes ] : n \in 0..Cardinality(Nodes) }

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/3A716915-90B6-461C-AD59-585B5A5AD6B6%40TimLeonard.us.