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