Is it possible to generate tuple sequence?

[Dmytro Ivanov]

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!

[Stephan Merz]

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 : TRUE

       IN  << x >> \o SeqFromSet(S \ {x})

It so happens that TLC evaluates SeqFromSet(1 .. 5) to the sequence <<1,2,3,4,5>>.

Best,

Stephan

--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/07e1f71b-14d3-4d36-abdc-e5c7be42cdc1%40googlegroups.com.

[dmy...@unity3d.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 : TRUE

       IN  << x >> \o SeqFromSet(S \ {x})

It so happens that TLC evaluates SeqFromSet(1 .. 5) to the sequence <<1,2,3,4,5>>.

Best,

Stephan

On 19 Dec 2019, at 11:33, Dmytro Ivanov <dmy...@beardsvibe.com> 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.