Enumerating a set - converting a set into a sequence

[mrynd...@gmail.com]

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.

[Stephan Merz]

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.

Stephan

[1] https://groups.google.com/forum/#!topic/tlaplus/d1UnxjNaYYc

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

[mrynd...@gmail.com]

I've managed to do what I wanted on sets only. Thank you for the advice!

W dniu wtorek, 31 grudnia 2019 17:36:37 UTC+1 użytkownik Stephan Merz napisał:

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.

Stephan

[1] https://groups.google.com/forum/#!topic/tlaplus/d1UnxjNaYYc

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.