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

*From*: dmytro@xxxxxxxxxxx*Date*: Thu, 19 Dec 2019 05:27:22 -0800 (PST)*References*: <07e1f71b-14d3-4d36-abdc-e5c7be42cdc1@googlegroups.com> <2907DC3E-DB0C-434F-9293-334CDA201D31@gmail.com>

> first of all, note that {x : x \in 1..5} is just an obfuscated way of writing 1 .. 5. :-)

Ah yes! I just had something like {x * 8 : x \in 1..5 } to generate set of valid pointers for 64 bit platform, forgot that if * 8 is removed then it's just 1..5 :)

> SeqFromSet(S \ {x})

Oh, nice! Coming from mostly imperative programming haven't thought about removing elements like that.

That solves my problem, thank you :)

Best,

Dmytro

On Thursday, December 19, 2019 at 11:55:36 AM UTC+1, Stephan Merz wrote:

Hello,first of all, note that {x : x \in 1..5} is just an obfuscated way of writing 1 .. 5. :-)There is not a unique sequence corresponding to a set, and that probably explains why TLA+ doesn't have syntax for sequence comprehension analogous to set comprehension. In particular,CHOOSE x \in Seq(1 .. 5) : TRUE(which TLC refuses to evaluate anyway) could denote any sequence containing the numbers 1 to 5, including << >>, <<1, 1, 4, 1>> etc.You can write a recursive operator that constructs a sequence containing exactly one copy of a finite set, as follows:RECURSIVE SeqFromSet(_)SeqFromSet(S) ==IF S = {} THEN << >>ELSE LET x == CHOOSE x \in S : TRUEIN << x >> \o SeqFromSet(S \ {x})It so happens that TLC evaluates SeqFromSet(1 .. 5) to the sequence <<1,2,3,4,5>>.Best,StephanOn 19 Dec 2019, at 11:33, Dmytro Ivanov <dmy...@xxxxxxxxxxxxxx> wrote:Hi everyone :) Learning TLA+ and have a question about sequences:If I have a set of valid values, for example foo == {x : x \in 1..5}How can I generate some sequence of this values in PlusCal?Currently I just hardcoded bar = << 1, 2, 3, 4, 5 >> and that works.I've also tried bar = << x \in foo : TRUE >> but that's not supported. Tried bar = CHOOSE x \in Seq(foo) : TRUE but that doesn't for because Seq(foo) is not itereable ..Thanks!--

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 tla...@googlegroups.com .

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/07e1f71b-14d3- .4d36-abdc-e5c7be42cdc1% 40googlegroups.com

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/69869125-52b8-4e8e-b6cd-2e6cd2f6386b%40googlegroups.com.

**References**:**[tlaplus] Is it possible to generate tuple sequence?***From:*Dmytro Ivanov

**Re: [tlaplus] Is it possible to generate tuple sequence?***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Is it possible to generate tuple sequence?** - Next by Date:
**[tlaplus] Is there a generic hash function in TLA+?** - Previous by thread:
**Re: [tlaplus] Is it possible to generate tuple sequence?** - Next by thread:
**[tlaplus] Is there a generic hash function in TLA+?** - Index(es):