Mapping items from one constant to another?

[Philip White <phi...@xxxxxxxxxxxxx>]

Hello, TLA+ enthusiasts,

I’m developing a TLA+ model where I’d like to have two constants: ORGANIZATIONS and PEOPLE. I want to model that every organization has an owner, who is a person. I’m thinking of doing this by having a function from an organization to a person. I’d like TLA to create this function for me in the initial condition. Is that possible?

I understand this may not /always/ be possible, such as if I define my constants to have fewer people than organizations. But if I make sure that the constants are well-defined, can TLA+ do this mapping for me?

Alternately, is there a different / more idiomatic way to represent a relationship between constants?

Thank you.

— 
Philip