/* * Exercise A.1.1 on page 240 of * Software Abstractions, by Daniel Jackson * * This following Alloy model constrains a binary relation to have a collection * of standard properties. * * A finite binary relation cannot have all of these properties at once. Which * individual properties, if eliminated would allow the remaining properties to * be satisfied? For each such property eliminated, give an example of a * relation that satisfies the rest. * * You can use the Alloy Analyzer to help you. The run command instructs the * analyzer to search for an instance satisfying the constraints in a universe * of 4 atoms. To eliminate a property, just comment it out. To get you * started, we have commented out the non-empty property to permit the empty * relation as a solution. */ pred show { some r: univ -> univ { // some r // non empty r.r in r // transitive no iden & r // irreflexive ~r in r // symmetric ~r.r in iden // functional r.~r in iden // injective univ in r.univ // total univ in univ.r // onto } } run show for 4