kbanks
Member
If I have a set like a = {1,2,3} and I create a Sequence b = Sequence(a), I get a sequence of length 1, with the sole element being the set. In other words, b = <<{1,2,3}>>.
What is the right way to somehow enumerate over the set, so I can define a set of things in my config (.cfg) file, and make a sequence from them in my .tla file? (My intent was to wind up with b = <<1,2,3>>)
First answer: don't use config files, rather use the toolbox, which accepts more TLA+ values than the parser of config files. In particular, you can directly instantiate a constant parameter to a sequence such as <<1,2,3>>.
Second answer: while computing the set of elements contained in a sequence is straightforward, there are many sequences containing the elements of a set, even excluding repeated elements. So it depends on whether some arbitrary such sequence is enough for you or whether you'd like to try out all such sequences. If the former is enough, in TLA+ you can simply write
sequenceOf(S) == CHOOSE seq \in Seq(S) : Len(seq) = Cardinality(S) /\ \A s \in S : \E i \in 1 .. Len(seq) : seq[i] = s
(in a module EXTENDing Sequences and FiniteSets) to denote any such sequence. However, TLC cannot evaluate this operator because Seq(S) is infinite even if S is a finite set. Instead, you can give a recursive definition, such as
sequenceOf(S) ==
LET soAux[s \in SUBSET S] == IF s = {} THEN <<>>
ELSE LET elt == CHOOSE e \in s : TRUE
seq == soAux[s \ {elt}]
IN Append(seq, elt)
IN soAux[S]
Hope this helps,
Stephan
Laven writes that his definition of ToSeq produces a sequence in the reverse order than that produced by Merz's definition. What he should have written is that this was what he discovered when running the two definitions on a particular example on a particular version of TLC. The semantics of TLA+ do not imply this, and what those definitions produce could depend on the particular version of the particular tool one is using. If you want the elements in a certain order, you should define an operator that ensures that they are in that order--for example, one that sorts the sequence produced by either Laven's or Merz's definitiion.
You must log in to post.
