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.