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

[tlaplus] Assign incremental IDs to sets of functions



I have a very simple initialization for a function as follows:

sampleTableINIT ==
        sampleTable = [person \in group |-> 
            [
                status |-> "Active",
                divisions |-> {[assignedDivision |-> division] : division \in getDivisions(person)} 
            ]]


Here is a sample result from the definition:

[Sam :> [status |-> "Active", divisions |-> { [assignedDivision |-> "Sales"]]  
[Mary :> [status |-> "Active", divisions |-> { [assignedDivision |-> "Sales"], [assignedDivision |-> "CS" }]

What I'd like to accomplish is simple: Per person entry, I'd like to assign an ID per division. The result below is what I want:

[Sam :> [status |-> "Active", divisions |-> { [id |-> 1, assignedDivision |-> "Sales"]]    
[Mary :> [status |-> "Active", divisions |-> { [id |-> 1, assignedDivision |-> "Sales"], [id |-> 2, assignedDivision |-> "CS" }]  

Order on ID assignment does not matter. Is there an easy way to do this rather than mutating the function in a future state?

--
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/5c1eb8c4-80d2-472f-a3cd-fe6147adabean%40googlegroups.com.