[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Mapping items from one constant to another?

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.


On 5 Feb 2019, at 02:16, Philip White <phi...@xxxxxxxxxxxxx> wrote:

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.


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.