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

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

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.

On Wednesday, April 24, 2019 at 6:38:32 AM UTC-4, Jam wrote:
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 view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/e06d1583-1d04-473d-bd76-b0242f33a1c1%40googlegroups.com.