Problem 1: Binary Relations

The following Alloy model constrains a binary relation to have a collection
of standard properties:

run {
  some r: univ -> univ {
    some r           -- nonempty
    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
  }
} for 4

A finite binary relation cannot have all these properties at once. Which
individual properties, if eliminated (individually), allow the remaining
properties to be satisfied? For each such property eliminated, name the
property and give an example as a comment of a relation that satisfies the
rest.

You can read more about some of the properties defined above here.
Note that what described as "total" above is called "left total" in Wikipedia.

You can use Alloy to help you. The run command instructs the analyzer to
search for an instance satisfying the constraints in a universe of at most 4
atoms. To eliminate a property, just comment it out (with two hyphens in a row
at the start of the line).

Problem 2: Predicate Calculus

The properties in Problem 1 were written in a relational calculus style.
Rewrite each in a predicate calculus style instead, using the code from Problem
1 as a guide. For example, the non-emptiness property can be reformulated as

some x, y: univ | x -> y in r

Each of your reformulations can be cast as an Alloy assertion, so you can use
the analyzer to check it. For example, to check the reformulation of
a property, you would write

assert ReformulatePropertyOK {
  all r: univ -> univ |
         <property in relational calculus> iff <reformulation of property in predicate calculus>
}
check ReformulatePropertyOK

and then execute the check to see if there are counterexamples, i.e. values
of the relation r that satisfy one formulation but not the other. In total,
this file should contain an assertion for each property in the format above.

Problem 3: Distributivity

When writing "navigation expressions," you may notice repeated subexpressions
that can be factored out, making the overall expression more succinct. For
example, the expression p.mother.brother + p.father.brother, denoting p's
uncles, can be written instead as p.(mother + father).brother. Simplifications
like this rely on the assumption that certain algebraic identities hold, such as

• distributivity of join over union: s.(p + q) = s.p + s.q;
• distributivity of join over difference: s.(p - q) = s.p - s.q; and
• distributivity of join over intersection: s.(p & q) = s.p & s.q

for a given set s and binary relations p and q.

For each of the above three identities, say whether it holds, and if not, give a
counterexample. Here is an example of how you might check the first using
Alloy:

assert union {
  all s: set univ, p, q: univ -> univ | s.(p + q) = s.p + s.q
}
check union for 4

The command tells Alloy to find a counterexample within a universe of 4
elements. When you find that a property does not hold, try and obtain the
smallest counterexample you can, by reducing the scope (for example, replacing
for 4 with for 2).

Additional Alloy Resources

If you are struggling with Alloy syntax or operators, some particularly useful resources that the TAs would recommend include:

• the official alloy documentation
• a quick reference guide to most alloy operators
• a helpful powerpoint presentation for syntax and basic examples

Handing In

Run cs1950y_handin alloy1 from a directory holding your 3 Alloy files (binary_relation.als, predicate_calculus.als, distributivity.als). You should receive an email confirming that your handin has worked.

Credit

Exercises borrowed or adapted from Appendix A of Daniel Jackson's Software Abstractions.