Modeling 3: Introduction to Temporal 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. This assignment uses Alloy 6, as installed in the previous assignments.

:star: This assignment is based on a stencil file, which you can download here.

Additional Alloy Resources

For additional resources on temporal logic syntax/meaning in Alloy, check out:

AlloyDocs: Time
"Meaning of temporal connectives" in Alloy 6 Documentation
Verifying Expected Properties: Formal Software Design with Alloy 6
It's About Time: Alloy 6 blog post

Assignment description

In this assignment, you will use Alloy's temporal logic to model the behavior of a last-in, first out (LIFO) stack. More specifically, we will model a stack that is implemented with a backing linked-list.

Using the stencil file is required for this assignment.

In the stencil file, you will see that Stack itself contains a reference to its top. Values are pushed to the top and popped from the top. If the stack is empty, the top is none (the empty set).

The stack is implemented as follows: top is the head of a linked-list of Nodes, each of which has a Value and optionally a nextNode, which points to the next node in the linked-list. Some Nodes may not be in the stack at a particular state–if this is the case, those Nodes should not have a nextNode or be the nextNode of another Node.

Task 1: Modeling changes over time

Like the trash model we saw in class (and used in the Alloy 6 textbook), we'll need to place some constraints on the initial state as well as constraints on the predicates to describe valid transitions between states.

Your task: Flesh out the predicates for init, pop, and push.

You should constrain the Stack to begin empty.

Your models for push and pop should specify what preconditions should hold for these operations to take place and how the Stack changes when they do (for example, one precondition is that you should not be able to pop from an empty stack).

Start a README and answer the following written questions there:

Written Q1: Why should your transition predicates constrain the value of every var sig or field in the next state?

Written Q2: Do your transition predicates also need to constrain the value of every non-var sig or field?

The stencil has a few predicates and run statements to check for small example traces with push and pop. See the comments for more advice.

:star: Tip: in the visualizer, I suggest editing your Theme to hide Values and show the val relation as an attribute, rather than an arc, to simplify the view.

Task 2: Modeling valid traces

Now, we want to constraint all traces to describe some sequences of pushes and/or pops to our stack.

Note: unlike the trash model from class, you should not add a doNothing predicate here: something should happen at every step.

Your task: Flesh out the fact for validTraces.

validTraces should invoke your 3 previous predicates: init, push, and pop.

Written Q3: How does the Analyzer find valid "lasso" traces without a doNothing predicate?

Task 3: Verifying expected behavior of the model

Finally, the most interesting part of this assignment (and where temporal modeling is the most useful) is in specifying and verifying/checking that our model has expected behavior in different scenarios.

Your task: fill in the 4 predicates for properties to check in the stencil:

  1. validStack. The stack is always valid. (Note that you should not call this within push and pop, it should instead be an separate predicate that should hold because of how you designed push and pop.
  2. beforePop. Everything that was popped must have been pushed previously.
  3. pushToEmpty. Whenever the stack is empty, only available transition must be a push (since you cannot pop from an empty stack).
  4. [Independent] popThenPush. What does the stack look like after a pop followed by a push of the same value? (:star: fixed typo in predicate name 2024-02-21.)
    • Note: you can get most of the credit for this part by just constraining the top part of the stack.
    • For the final 5 points of credit, you should also constrain the nextNode relation in the Stack. This is more difficult, since popping then pushing the same Value does not actually require the same Node be used (similar to how an in-memory representation of a linked-list would actually work).

Written Q4: Why doesn't the uses of nextNode within each of these predicates only refer to the nextNode relation in the first state when run by the check statements at the end of the file?

The stencil ends with 4 check commands. These should all succeed once you have completed all of the predicates and facts in the stencil. The various run commands should also successfully show instances: you can add more of your own run/check commands to debug or sanity check your model.

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:

30 points: State change predicates

10 points: Valid traces fact

40 points: Predicates to verify expected outcomes

20 points: README/Written Qs 1-6

Submission

Submit the following 2 files on Gradescope: stack.als and README.{txt, md}.

Attribution

This exercise is adapted from on a previous version of a Forge Model Checking assignment from Tim Nelson's Logic for Systems at Brown University.