Modeling 1: Introduction to Alloy

Learning outcomes

This is a pair assignment—you may choose to either complete the assignment alone or with one other CS340 classmate. On Gradescope, you will be able to form a group with maximum size 2.

Setup

You can run this assignment locally, on your own machine.

Alloy 6

For this assignment, we will use Alloy 6, which you can download here.

For Mac users: download the alloy.dmg file. Open Finder, right-click (not normal click) on the file, and select "Open". You will see a warning that "macOS cannot verify the developer of “org.alloytools.alloy.dist.jar”. Are you sure you want to open it?". Since we trust the friendly MIT developers who make Alloy, click yes.

For Windows or Linux users, download the org.alloytools.alloy.dist.jar file. This is a Java distribution format, so you'll need Java installed to run Alloy (otherwise, clicking the Jar file will unzip it, rather than running it). If you click it and Alloy opens, you are all set. Otherwise, download Java and click it again.

Additional Alloy Resources

For additional resources on Alloy syntax or operators, check out:

• The official Alloy documentation
• A quick reference guide to most Alloy operators

Assignment description

Problem 1: sigs and preds and facts, oh my!

Start with this simplified version of the model we defined for our malloc heap layout in class (see the class notes for the longer version, with many detailed comments).

// Start with this model for this problem
abstract sig Status {} 

one sig Alloc, Free extends Status {}

sig Block {
  status: Status, 
  prede: lone Block, 
  succ: lone Block
}

fact {
  ~prede = succ
}

run {
  some Block
} for 5 but 0 Int

In the malloc heap layout we use in CS240, free blocks have footers, whereas allocated blocks do not have footers. (You do not need to know exactly how the footer is used for this problem, only that footers follow this constraint and are defined per-block).

Problem 2: Binary Relations

The following Alloy model constrains a binary relation to have a collection
of standard properties (note that -- starts a comment in Alloy):

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   -- (left) total
    univ in univ.r   -- onto
  }
} for 4 but 0 Int -- simple, finite scope

A finite binary relation cannot have all these properties at once. When this
model is run in the Alloy Analyzer, the result is: No instance found. Predicate may be inconsistent..

You can read more about some of the properties defined above here.

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, --).

( note: wording here updated to be more clear, 2pm 2024/02/07.)

The command tells Alloy to find an example within a universe of 4 elements. When you find an instance, try and think about whether it's the smallest example possible.

Problem 3: Predicate Calculus

The properties in Problem 2 are written in a relational calculus style.

( Fixed typo: previously said Problem 1. 4:30pm, 2024/02/09. If you already answered this with Problem 1, I'll accept those answers for full credit as long as you have 8 total rewritten properties.)

    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   -- (left) total
    univ in univ.r   -- onto

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.

Problem 4: Distributivity [INDEPENDENT]

When writing expressions with the . syntax, you may notice repeated subexpressions that can be factored out to make the overall expression more succinct.

For example, consider a recursive binary tree definition that has a value and left and right child pointers.

The expression tree.left.value + p.right.value, denoting tree's children's values, can be written in Alloy instead as tree.(left + right).value.

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 (what our tree example depends on);
• 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.

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 but 0 Int

(Note: updated to include but 0 Int in the example, 4:30pm 2024/02/08. This will make the counterexamples much smaller, since in Alloy 6, making the default scope smaller (e.g., for 2) still allows more than 2 Int atoms)).

Grading

This assignment is worth 100 points, broken down by:

Submission

Submit the following 5 files on Gradescope: block_footers.als, binary_relation.als, predicate_calculus.als, distributivity.als, README.{txt, md}.

Attribution

Exercises 2-4 adapted from Appendix A of Daniel Jackson's Software Abstractions.