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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Wed, 11 Nov 2020 15:30:07 +0100*References*: <5c1eb8c4-80d2-472f-a3cd-fe6147adabean@googlegroups.com>

Fundamentally, you are trying to convert a set to a sequence that contains each element of the set exactly once. The module SequenceExt from the Community Modules contains an operator that does that: IsInjective(s) == \A i, j \in DOMAIN s: (s[i] = s[j]) => (i = j) SetToSeq(S) == CHOOSE f \in [1..Cardinality(S) -> S] : IsInjective(f) Now you can define your operator as follows: tableInit == [person \in group |-> [ status |-> "Active", divisions |-> LET divs == SetToSeq(getDivisions(person)) IN { [id |-> i, assignedDivision |-> divs[i]] : i \in 1 .. Len(divs) } ]] Instead of representing `divs' as a set of records with id fields, you could represent it as a sequence where the id is implicit in the position of the element in the sequence. However, I wonder if you are at the right level of abstraction for your specification: all the information that you need is contained in the set `group' and the operator `getDivisions'. Is it important to construct an explicit data structure that materializes that information, in particular since you don't care about the order of IDs? 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/31E8E255-2AE2-4152-ACB9-9128F40E1704%40gmail.com. |

**References**:**[tlaplus] Assign incremental IDs to sets of functions***From:*tlalearner

- Prev by Date:
**Re: [tlaplus] How to generate a sequence from another sequence ?** - Next by Date:
**Re: [tlaplus] Finding Inductive Invariants using TLC and Proving it using TLAPS** - Previous by thread:
**[tlaplus] Assign incremental IDs to sets of functions** - Next by thread:
**[tlaplus] tla+ source code for the example in "How to Write a 21st Century Proof"** - Index(es):