Assignment 5: Modeling 3

Modeling 3: Introduction to Temporal Alloy ------ # Learning outcomes :::info In this assignment, you will: - Practice using linear temporal logic operators to model a system. - Get experience using the new trace view to see how traces evolve over time. - Practice both modeling a system and specifying the expected behavior of that system as predicates. - Remind yourself how you can implement a stack with a linked-list! ::: 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](https://alloytools.org/alloy6.html), as installed in the previous assignments. :::success :star: This assignment is based on a stencil file, which you can [download here](https://drive.google.com/file/d/1wK77Xd9LxwBXcp_aY4grjF0Iaa49FMB2/view?usp=share_link). ::: ## Additional Alloy Resources For additional resources on temporal logic syntax/meaning in Alloy, check out: [AlloyDocs: Time](https://alloy.readthedocs.io/en/latest/language/time.html) ["Meaning of temporal connectives" in Alloy 6 Documentation](https://alloytools.org/alloy6.html) [Verifying Expected Properties: Formal Software Design with Alloy 6](https://haslab.github.io/formal-software-design/overview/index.html#verifying-expected-properties) [It's About Time: Alloy 6 blog post](https://www.hillelwayne.com/post/alloy6/) ## Task 0: LTL tutor For task 0, you (and your partner) should first complete a series of exercises using **LTL tutor**, a tool that adapts exercises based on your demonstrated understanding of linear temporal logic. Access LTL tutor here: https://www.ltl-tutor.xyz Select "Have a course code?", enter your Wellesley alias (e.g., `av111`), and the course code `CS340 sp25`. :::warning If you are completing this part of the assignment as a pair, include both of your aliases with a dash, e.g., `av111-xy123`. However, **only do this** if you are actively sitting together, in person, discussing and working through each exercise together. Otherwise, you may complete this part separately. I will just check for the total number of exercises completed with your alias (so for academic integrity, make sure you only include your/your partner's alias if you are actively working together). ::: :::success Review the LTL syntax used by the tool [here](https://www.ltl-tutor.xyz/ltl). I suggest using the "Electrum" syntax, which is almost identical to Alloy's syntax. Complete **30 or more** individual LTL tutor exercises. I will grade on completeness, not correction (but I reserve the right to check timestamps of exercises, to see that you are not just guessing on every one). There is a dropdown along the top "tutor dashboard" row where you can select "Electrum syntax". Exercises are grouped as e.g. `Question 1 of 4`; I suggest noting down the number in the group (e.g., `4`) as you complete them, so you don't have to go back through your profile's logs to see how many you have completed. ::: # Main assignment description In the remainder of this assignment, you will use Alloy's temporal logic to model the behavior of a [last-in, first out (LIFO) stack](https://en.wikipedia.org/wiki/Stack_(abstract_data_type)). More specifically, we will model a stack that is implemented with a backing linked-list. Using the [stencil file](https://drive.google.com/file/d/1wK77Xd9LxwBXcp_aY4grjF0Iaa49FMB2/view?usp=share_link) is required for this assignment. :::info In the stencil file, you will see that `Stack` itself contains a reference to its `top`. `Value`s 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 `Node`s, each of which has a `Value` and optionally a `nextNode`, which points to the next node in the linked-list. Some `Node`s may not be in the stack at a particular state--if this is the case, those `Node`s 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. :::success 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. :::info :star: **Tip**: in the visualizer, I suggest editing your Theme to hide `Value`s 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. :::warning Note: unlike the trash model from class, you should **not** add a `doNothing` predicate here: something should happen at every step. ::: :::success 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. :::success 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? - 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 :::success 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: :::info 10 points: **LTL tutor** exercise completion 25 points: State change predicates - 5: `init` - 10: `push` - 10: `pop` 5 points: Valid traces fact - 5: `validTraces` 40 points: Predicates to verify expected outcomes - 12: `validStack` - 8: `beforePop` - 8: `pushToEmpty` - 12: `popThenPush` 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](https://docs.google.com/document/d/e/2PACX-1vSjEbk4oJTvNxgxKWxcSgSKLnmNDsM6fZkkN10n_UD4JOlraUMzMDoFH_lWcm377smn_hmkjdVI4OZP/pub) assignment from [Tim Nelson's][tim] [Logic for Systems][lfs] at Brown University. [tim]: https://cs.brown.edu/~tbn/ [lfs]: https://csci1710.github.io/2023/