How to add restrictions to fields of a signature when there are two instances in the model

Question

I have the following Alloy model which describes a group of people. to simplify the problem. Here is a sample code snip.

sig groupofpeople {
member: set person,
country: Country
}{
 #person=2
} 

sig people {
teamleader: Bool,
position: String
}

So now we have two peoples in a group. Next I want to add some restrictions to the people in the group. For example, I want the two people in a group to always have one team leader and one team member. I use the following fact to do this:

fact {
all n: people , m: people - n {
        n.teamleader not in m.teamleader
    }
}

Now I encounter a problem which keep me from moving forward. The desired model I'm looking for is that if a group's country is "US", then the position of the teamleader is "US_TL" and position of the team member is "US_TM". If the country is "UK" then the position of teamleader is "UK_TL" and position of the team member is "UK_TM", and so on.

I tried to add something like:

all n: groupofpeople {
        (n.country in US => (
        n.member.position="US_TL" or 
        n.member.position= "US_TM"))  or
        (n.country in UK => (
        n.member.position ="UK_TL" or 
        n.member.position = "UK_TM"))
    }

But there are obviously something wrong with the prediction and the model can't generate correct solutions for me. Could you help me to identify the problem in my model?

Answer 1

The model you posted here doesn't compile, so I can't really pinpoint the problem (since there are many, so of which might be just typos). What seems to be incorrect for sure is the or between the two implications in the last all quantifiers: based on your description of the task, it should be and instead.

If I understood the desired properties of your model, here's how I would rewrite it (and if that's not what you intended to achieve, please clarify your question and post a model that is syntactically correct):

open util/boolean

abstract sig Country {}
one sig US extends Country {}
one sig UK extends Country {}

sig GroupOfPeople {
  member: set Person,
  country: one Country
}{
  #member=2
} 

sig Person {
  teamleader: Bool,
  position: String
}

fact {
  all g: GroupOfPeople {
    all n: g.member, m: g.member - n {
      n.teamleader not in m.teamleader
    }
  }
}

run {
  all n: GroupOfPeople {
    (n.country in US => (
        n.member.position="US_TL" or 
        n.member.position= "US_TM"))
    (n.country in UK => (
        n.member.position ="UK_TL" or 
        n.member.position = "UK_TM"))
    }
} for 5

Answer 2

Would it not be nicer to replace the defn of sig Person above by

abstract sig Person{position : String}
sig Leader, Follower extends Person

fact one_leader {
  all g : GroupOfPeople | one (g.member & Leader)
}

and even better to put this fact in the invariant of GroupOfPeople:

one (member & Leader)