[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] How to choose a record field when a record is an element of a set?
Thank you Jaak and Stephan. I was also thinking about functional representation, but purposely chosen sets to closely model SQL, because access by index is not the only access I need to verify. I probably can create wrapper functions/operators to make it look functional, or re-think my approach again.
P.S. Jaak, regarding your comment about using id \in DOMAIN theSet. It is also possible to use a slightly different approach: theSet[id] = NoVal if id \in SomeSet and you initialize theSet = [p \in SomeSet |-> NoVal] as described in Specifying Systems on p 52.