| 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+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/2907DC3E-DB0C-434F-9293-334CDA201D31%40gmail.com. |