module Family // Name signature sig Name{} // Person signature (abstract) abstract sig Person { name: Name, // Exactly one father: lone Man, // Zero or one mother: lone Woman // Zero or one } // Man and Woman extends Person sig Man extends Person { wife: lone Woman } sig Woman extends Person { husband: lone Man } // Two different persons do not share the same name fact NoSharedName { all p1,p2: Person | (p1 != p2) implies (p1.name != p2.name) } // The husband relation is the transpose of the wife relation fact HusbandIsTransposedOfWife { husband = ~wife } // Prevents incestuous relations fact { no (wife & *(mother+father).mother) no (husband & *(father+mother).father) } // Checks incestuous relations assert ParentsCannotBeHusbandOrWife { no (wife & *(mother+father).mother) no (husband & *(father+mother).father) } // No one who can be in the list of his/her parents fact NoSelfParent { no p: Person | p in p.^(mother+father) } // Returns the set of grandparents for a person fun grandparents[p: Person] : set Person { let parents = (father+mother) | p.parents.parents } // Returns the set of grandfathers fun grandfathers[p: Person] : set Man { grandparents[p] & Man } // Returns the set of grandmothers fun grandmothers[p : Person] : set Woman { grandparents[p] & Woman } // Check whether a person p has grandparents. Returns true or false pred hasGrandparents[p : Person] { some grandparents[p] } // TODO: write a fact (invariant) to prevent that a parent of a person // can also be a grandparent (i.e. a parent of his/her parent) of that person. // Hints: // - You can use the (reflexive) transitive closure operators (* or ^) // - You can use operations on sets: +, -, &, in, = // - To simplify the code, you can also create a parent variable fact { // ... } // Find satisfying instances containing at least one person with some grand parents pred Show { some p: Person | some grandmothers[p] and some grandfathers[p] } run Show for 6 check ParentsCannotBeHusbandOrWife for 3