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

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

Thank you, this is exactly what I was looking for.

> On Feb 4, 2019, at 11:27 PM, Stephan Merz <stepha...@xxxxxxxxx> wrote:
> 
> 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
> 
> 
>> 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.
>> 
>> — 
>> 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.
> 
> 
> -- 
> 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.