Modeling 1: Introduction to Alloy

Learning outcomes

In this assignment, you will:

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:

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

Your task: extend the short model from above to also model the existence of footers. Each free block should have its own footer and allocated blocks should not have footers.

Write your answer in a new Alloy file, block_footers.als.

Begin a README.{md, txt} file. Answer the following:

Written Q1: Explain how you updated the model in 1-2 sentences. If you used a pred or a fact, explain why you chose to use that construct and not the other construct.

Written Q2: Explain whether you used a run or check command to view your model, and why you chose that command.

You do not need to define any fields on footers. You do not need to worry about the overall heap footer/epilogue.

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.

Your task: determine which individual properties, if eliminated (individually), allow the remaining properties to be satisfied? For each such property eliminated, give an example (as a comment) of a relation that satisfies the rest of the properties.

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

Write your answers either as in-line comments next to each property or as a new block comment at the bottom of the file (denoted with /* ... /*) in a file called binary_relation.als.

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.

For full credit, you should use minimal examples. Use the fewest number of atoms and the simplest names to describe any counterexamples you include. You may not need to change the scope for this: if r has only only element, then it is already is the smallest relation that satisfies some r.

An example of simplifying names would be r = {u1->u2} instead of r = {Univ$1->Univ$2}.

Problem 3: Predicate Calculus

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

Your task for this problem: rewrite each property from Problem 2:

    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

in a predicate calculus style instead. 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.

Write your answers in the format shown above (that is, 8 named assert statements) in a file named predicate_calculus.als.

Written Q3: Do you prefer the predicate calculus style or the relational style? Answer in your README. There is no right or wrong answer! You need only provide a short sentence.

Problem 4: Distributivity [INDEPENDENT]

Note: this is an [INDEPENDENT] problem that you should discuss only with your partner and the instructor.

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

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

Your task for this problem: for each of the above three algebraic identities, say whether it appear to hold, 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 but 0 Int

For full credit, you should:

  1. Minimize your counterexample. Use the smallest scope and the simplest names to describe any counterexamples found.
  2. As part of your counterexample, describe the two different sets found to be not equal for that specific counterexample (with the concrete names from your minimized description).

Write your three named assertions, whether or not the property holds, and any minimized counterexamples in a file named distributivity.als.

Written Q4: For the properties that appear to hold, have you proven anything? For the properties that do not appear to hold, have you proven anything? Answer with justification in your README.

Grading

In your README, also report:
Written Q5: Collaborators other than your partner?
Written Q6: Roughly how long did this assignment take you (in hours)?

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.