--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/e6ba59a2-16c6-4547-be8d-f0f21da08e91%40googlegroups.com.
There was a recent thread with a similar question [1], perhaps it solves your issue.However, it may be preferable to avoid constructing a sequence from a set and to stay at the abstraction level of sets if you can.
On 31 Dec 2019, at 14:45, mrynd...@gmail.com wrote:
I have the following problem. I need to convert a set into a sequence:nbrs == {x \in {-1, 0, 1} \X{-1, 0, 1} : x /= <<0, 0>>}I've found 'OrderSet' from 'Practical TLA+', but using OrderSet(nbrs) causes this error in TLC:TLC threw an unexpected exception.This was probably caused by an error in the spec or model.See the User Output or TLC Console for clues to what happened.The exception was a util.WrongInvocationException: Attempted to construct a set with too many elements (>1000000).TLC was unable to fingerprint.Could someone shed some light onto this, or propose alternative solution?Help is greatly appreciated.--
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 tla...@googlegroups.com.