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

*From*: Jam <wawrzynchonewicz@xxxxxxxxx>*Date*: Wed, 24 Apr 2019 03:38:31 -0700 (PDT)

Hello. I'm struggling with a seemingly simple conversion of a set of N elements into a tuple with those same elements. One way I think this could be done (I haven't tried this, because i don't want this) is:

-- `VARIABLES i, tuple, set, temp`

Convert ==

/\ i < Cardinality(set)

/\ temp = CHOOSE x \in set : TRUE \* I don't even know how to pull them in order

/\ set' = set \ temp

/\ tuple' = Append(tuple, temp)

/\ i' = i + 1

I don't like this solution because it requires multiple steps, destroys the original, and quite frankly, is ridiculous.

Is there a way of doing it in just one step? And preferably without variables (if i remember correctly there are variables for preserving state between steps, and values for computing state within a step)? The reason I need this is because i have a queue (which internally is a tuple), and i need to enqueue 2 things in one step. I figured maybe I can do this by

`queue' = queue \o multiple_elements`

but for this i need multiple_elements to be a tuple, and currently its a set.

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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.

Visit this group at https://groups.google.com/group/tlaplus.

For more options, visit https://groups.google.com/d/optout.

**Follow-Ups**:**[tlaplus] Re: Converting a set into a tuple in one step***From:*William Schultz

**[tlaplus] Re: Converting a set into a tuple in one step***From:*Jam

- Prev by Date:
**[tlaplus] Re: When TLC error trace send with stuttering - what does this mean?** - Next by Date:
**Re: [tlaplus] Re: When TLC error trace send with stuttering - what does this mean?** - Previous by thread:
**[tlaplus] Re: Removing "equivalents" from a set** - Next by thread:
**[tlaplus] Re: Converting a set into a tuple in one step** - Index(es):