| The definition
Init == owner \in [ORGANIZATIONS -> PEOPLE]
describes all possible states in which each organization is assigned to a person. From the remainder of your message it sounds like you'd like this function to be injective, i.e., no person owns two organizations. This can be written as
Init == owner \in { f \in [ORGANIZATIONS -> PEOPLE] : \A o1,o2 \in ORGANIZATIONS : f[o1] = f[o2] => o1 = o2 }
Now, if there are fewer people than organizations, TLC will find that there is no initial state.
Regards, Stephan
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 -- 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+u...@xxxxxxxxxxxxxxxx. To post to this group, send email to tla...@xxxxxxxxxxxxxxxx. Visit this group at https://groups.google.com/group/tlaplus. For more options, visit https://groups.google.com/d/optout.
|