Converting a set into a tuple in one step

[Jam]

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.

[Jam]

Well, I have figured it out. With the help of https://learntla.com/tla/ , i learned that tuples are functions and found a useful operator:

Range(T) == { T[x] : x \in DOMAIN T }
Seq2(S, n) == UNION {[1..m -> S] : m \in 1..n}

which I then use as follows to get what I need:

SetToTuple(set) ==
    CHOOSE x \in Seq2(set, Cardinality(set)) : Range(x) = set

It's no joke that TLA+ has a steep learning curve!

[oci.thr...@gmail.com]

Here is another, more conventional way:

RECURSIVE S2T(_)
S2T(S) == IF Cardinality(S) = 0 THEN <<>>
          ELSE
          LET
            x == CHOOSE x \in S : TRUE
          IN

            <<x>> \o S2T(S \ {x})

[William Schultz]

There is a SetToSeq operator defined in the SequencesExt.tla module in the TLA+ CommunityModules repo that provides the functionality you want. There are instructions in that repo's README on how to easily utilize those modules in your own spec.