Looking for a simpler solution

Questions
1

I have this model below, wondering if there is a simpler solution to make sure people are in the company.

sig Company {}
sig Employee {
	company : Company
}
sig Manager {
	company : Company,
	team : set Employee
}
sig Director {
	company : Company,
	team : set Manager
}

-- can this be simplified?
fact SameCompany {
	all e : Employee, m : Manager, d : Director {
		e in m.team and m in d.team implies 
			e.company = m.company and m.company = d.company
	}
}
2

Hi,

First, Iā€™m not sure this fact is what you want, because if a manager has no team but belongs to team then it will not be required to belong to the same company of its director. Likewise, if it does not belong to a team then its own team will not be required to be in the same company. Your fact only applies when managers have a team and belong to a team. I think you should start by splitting the constraint as follows.

fact SameCompany {
	all e : Employee, m : Manager {
		e in m.team implies	e.company = m.company
	}
	all m : Manager, d : Director {
		m in d.team implies m.company = d.company
	}
}

By chaining the dot composition operator you can simplify this as follows.

fact SameCompany {
	all m : Manager {
		m.team.company in m.company
	}
	all d : Director {
		d.team.company in d.company
	}
}

I also recommend you take advantage of signature hierarchy to factor common fields / attributes. For example, you could make managers and directors extend the employee signature and then it would not be necessary to duplicate the declaration of the company field. Likewise for Director and Manager, as the former is specialisation of the latter. With these changes you would be able to further simplify your fact.

Best,
Alcino

1 Like
3

Thank you Alcino for the detailed suggestions, they are very helpful! Happy New Year!