sig Person {
  spouse: lone Person
}

pred show {}

run show for exactly 3 Person

// 1. run show and show several models, identify the situation from the slides

// 2. check if marriage is symmetric (which will fail)
/*
assert symmetricMarriage {
  spouse = ~spouse
}
check symmetricMarriage for 2
*/

// 3. add the following fact in order to make sure that for each person p it holds that
// p has no spouse OR p is his/here spouses' spouse
// p is now symmetric (check also for scopes larger than 2) but it still has a shortcoming (which?)
/*
fact {
	all p: Person | no p.spouse or p in p.spouse.spouse
}
*/

// 4. add that a person cannot marry herself
/*
fact {
	all p: Person | p.spouse != p
}
*/