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