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

Re: [tlaplus] Is it possible to generate tuple sequence?



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 <dmytro@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 tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
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/2907DC3E-DB0C-434F-9293-334CDA201D31%40gmail.com.