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

*From*: oci.throwaway.1@xxxxxxxxx*Date*: Sat, 29 Feb 2020 16:35:53 -0800 (PST)*References*: <b9fae7aa-2b2f-4baa-b02d-3dc0bc8b907e@googlegroups.com> <d9b1e0d1-c244-4ccf-9dc5-f66ab68525da@googlegroups.com>

Here is another, more conventional way:

S2T(S) == IF Cardinality(S) = 0 THEN <<>>

ELSE

LET

x == CHOOSE x \in S : TRUE

IN

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

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) = setIt's no joke that TLA+ has a steep learning curve!

On Wednesday, April 24, 2019 at 12:38:32 PM UTC+2, 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 + 1I 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_elementsbut 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/bde2f6f9-eee4-46a6-aa4d-6c7560175b2b%40googlegroups.com.

**References**:

- Prev by Date:
**[tlaplus] Question about prophecy variables** - Next by Date:
**[tlaplus] Re: Question about prophecy variables** - Previous by thread:
**[tlaplus] Re: Converting a set into a tuple in one step** - Next by thread:
**[tlaplus] Re: Converting a set into a tuple in one step** - Index(es):