[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.