---
tags: Projects
---
Mini-Project: Model Checking
================
**Due April 16th at Anywhere-on-Earth time.**

## The Hunt Continues... (optional)

:::spoiler Look here for the next clue!

At long last, the CS18 Team of Theme is ready to reveal the final clue to Blueno’s treasure. Many sweat, tears, and hardwork have gone to this moment (very many). Blueno’s treasure has been sitting, gathering dust and bugs for so long that we need to check if all of the clues still work.

*You’ve come far, dear student, on you I depend*
*But there’s yet a clue to be found, my friend*
*I’ll give it to you*
*And the [qr compiler](https://qr-combiner.vercel.app/), too*
*Put the pieces together, this is almost the end*

Put together the qr code pieces that you've been *compiling* to find Blueno's treasure! There are 9 in total! 6 are from the homeworks and 3 are from the projects.


:::

Overview
-------

In the mid 1980's, the [Therac-25](https://en.wikipedia.org/wiki/Therac-25) computer-controlled radiation machine malfunctioned and administered (near) lethal doses to several patients. In more recent years, we've heard concerns about critical errors in software-controlled cars, railway signaling, and more.

Software flaws contributed to each of these accidents. These flaws weren't uncovered during testing, instead emerging after the corresponding system was in use. Admittedly, thorough testing is difficult (if not impossible): a realistic system has too many possible inputs for us to check them all. Yet we don't want to leave errors in safety-critical systems. What's to be done?

Graph algorithms to the rescue!

We can think of a program as describing a (very) large graph. Each node of the graph holds values of the key variables in the program. As a program runs, it updates the values of its variables. An edge from node `A` to node `B` in the graph means that the program changed its values from those at node `A` to those at `B` while the program was running.

### Programs as Graphs

Here's a simple example: imagine that you wrote the following program to manage a traffic light. The program uses a `Timer` library, with a countdown timer that "expires" when time runs out and can be restarted with a full allotment of time.

class TrafficLight(timer: Timer) {
   val String color = "red";
   
   while (true) {
     if (color.equals("red") && (timer.expired)) {
      color = "green";
      timer.restart();
    } else if (color.equals("green") && (timer.expired)) {
      color = "yellow";
      timer.restart();
    } else if (color.equals("yellow") && (timer.expired)) {
      color = "red";
      timer.restart();
    }
  }
}

This program could be represented by the following graph. The nodes are in grey. Each node contains the current value of the `color` variable. The `timer` status labels the edges. The values in the node and the label on the edges get and-ed together to summarize the conditions for moving around the graph. In this graph, the light will keep cycling its colors forever as long as the timer continues to expire (the timer restarts are not in the picture).


***WARNING:** the arrows are reversed in the above picture. Each should go in the opposite direction from what is shown.*

In a real traffic intersection, there are *two* color variables, one for each direction (north/south and east/west). There are usually multiple timers (a short one for the yellow->red transition and a longer one for the green->yellow transition). If we put all of those together, we get a more complicated graph such as the following (we've collapsed the `var=value` notation from the previous graph to single words and left off the edge labels for readability):


### Traffic Safety

Now, let's think about the safety of this traffic light system. An accident could occur if both lights were green at the same time. We see that such a node is indeed in the graph. But the real question is *whether that node can be reached in practice*. If the traffic light starts up in the configuration with `bigAveRed` and `smallStGreen` (the top-left node), for example, there is no way to follow the edges to get to the double-green node. But if both lights started off red, we could reach the double-green configuration.

Thus, there are three key steps to traversing a graph to check system safety:
1. identify the state (node) that your system will be in when you start it up
2. write a predicate (function that returns boolean) over the state labels capturing the bad condition (here, `(bigAveGreen and smallStGreen)`)
3. check whether any state that is reachable from the start-up state satisfies the bad condition. If so, the system is unsafe.

These steps help make sure that **bad things can't happen** (where the expression defines what is bad).

One way to make a safe traffic light would be to permanently set both lights to red. This wouldn't be very useful, however. Therefore, sometimes we want to check program graphs to make sure that **good things will happen**. In the context of our traffic light, we might want to check that the light in each direction does eventually turn green. This can be done with a modified version of the third step from above:

4. check whether there is a cycle reachable from the start state in which the good condition never happens (such a cycle says that our program could get stuck)

These two kinds of checks: *safety* (nothing bad happens) and *liveness* (something good happens) are at the foundation of using programs to search for software errors. In CS, these tools are called **model checkers**. They are increasingly used in many companies (including some parts of Microsoft) to help detect errors in programs. CS1710 at Brown ("Logic for Systems") goes into this in more depth.

In this project, you will apply what you have learned about graph data structures and computing reachability (using depth-first search) to build a simple program checker for safety. For those who are interested, we are also giving you the starter code for checking simple liveness (but only safety, up through step 3 above, is required for this project).

Project Requirements
========

The following diagram shows the general architecture of a model checker. Roughly speaking, there is a program graph (called a State Graph in the figure), and a condition that we want to check. These feed into a model-checking algorithm, that reports on whether the condition holds. The State Graph could be built on a variety of concrete data structures for graphs.


For this project, you will implement

- A `Graph` class with basic functionality for nodes and edges, choosing from one of two data structures.
- A `StateMachine` class that uses the `Graph` class to build a specific state graph and provides two methods for checking conditions against the graph.

You will create a collection of specific graphs with node labels and conditions on which to test your model checker. You'll also write about the design decisions and performance of your solution. This is a culminating assignment, where you get to show us what you have learned about OO programming, data structure choices, and testing.

Graph and Node Traits
----------

You will find the traits that you need to implement in the files located in the `src` folder of your repository. These traits encapsulate how you will be representing and building graphs. Each of these traits, `Graph` and `Node`, have three methods that you will need to implement.

Classes that extend the `Graph` trait (i.e. the `AdjacencyListGraph` and `MatrixGraph` classes in the `sol` folder) will need to implement `createNode`, `addEdge`, and `show`.

* `createNode` should return a new `Node` that has the contents of the input to the function. It should *not* build any edges.
* `addEdge` takes in as input two `Node` objects and builds an edge between them.
* `show` is a utility function to help you visualize the graph. It takes no inputs and returns nothing, but should print the representation of the graph legibly.

Classes that extend the `Node` trait (i.e. the `ALNode` subclass of the `AdjacencyListGraph` class and the `MNode` subclass of the `MatrixGraph` class) will need to implement `getContents`, `getNexts`, and `addEdge`.

* `getContents` returns the contents contained at the `Node` the method gets called on.
* `getNexts` returns a `List[Node]` that contains every `Node` that the `Node` the method is called on can get to (i.e. the connections out of the `Node`).
* `addEdge` takes in a `Node` that an edge will get built to and builds that connection. It should not return anything.

The Graphs
--

:::info
You will choose **ONE** of the following two graph data structures to implement. (We originally intended for you to implement both, but are reducing the workload by requiring only one.) [Note: If you're comfortable with the way we've done graphs in lecture so far, you might learn more from the Matrix version.]
:::

**Option 1: Adjacency List**

One way to represent the relationship between a node and the rest of the graph is to have a field in each node that stores all of the nodes that it points to. This is how we have used graphs in lecture.

**Option 2: Adjacency Matrix**

Another way to represent a graph is to use a 2D array (matrix) of booleans that stores information about edges, given certain coordinates in the matrix. If `matrix[i][j]` is `true`, then there is a connection from the nodes represented by `i` and `j`. The matrix has the same number of rows as it does columns (the number of nodes in the graph).

To use the matrix approach, you'll need a way to map each node to its index (the same index in each matrix dimension). You'll have to figure out how to do this.

So, if we had Node A stored in index 3 of the node array, and Node B stored in index 5, and `matrix[3][5] == true`, then Node A has an edge to Node B.

Your implementation should also handle the following edge cases:
1. Throw an `IllegalArgumentException` with an informative message for negative `maxSize` of your matrix.
2. Throw a `RuntimeException` with an informative message if users attempt to add more nodes than the number allowed by `maxSize`.

State Machine
--

A *State Machine* (like the second traffic light example above) consists of a graph in which the contents of each node is a subset of a collection of labels (like `bigAveRed`, `bigAveGreen`, ...); these labels stand for different values of variables in the program. The `StateData` class in the stencil captures a collection of labels (this will be the type of the contents in your underlying graph). The state machine also marks a single node as its start state (like the 'bigAveRed/smallStGreen' node in the above example).

*Note: with these data structures, you can capture programs that have a finite set of variable-value labels. This means we can't represent programs with arbitrary arithmetic: that's beyond the scope of this assignment.*

### Reading State Machines from CSV

To make it easier for you to define state machine graphs, the stencil code for `StateMachine` includes a method (`initFromCSV`) that populates a `StateMachine` from CSV files. This method takes a CSV file describing the nodes, another describing the edges, and the name of the node from which the program would start running.

def initFromCSV(nodeCSV: String, 
                edgesCSV: String, 
                startState: String)` 
    ...

The `nodeCSV` has one row per node in the graph. Its header row is `id,contents` where `id` is a string that serves as a name for the node, and `contents` is a semi-colon-separated list of labels. The `edgesCSV` has one row per edge. Its header row is`fromNode,toNode` where each is a node id from the corresponding nodes-csv.

Sample nodeCSV

id,contents
n1,blue;3;on
n2,red;0;off
n3,green;10;off

Sample edgesCSV

fromNode,toNode
n1,n1
n1,n3
n2,n3
n3,n2
n3,n3

We have provided sample CSV files of the traffic lights example in the `data` folder.

Modify `initFromCSV` so that it raises some exception (could be any exception) if the `edgesCSV` tries to use a state that was not listed in the `nodeCSV`.

:::spoiler Click here if you're having trouble setting up the apache common-csv-1.8.jar.

1. In Intellij, pen the `Project Structure` by clicking on the file icon with three blue squares in the top right corner.
2. Click on `Modules` under the Project Setting heading in the sidebar on the left window.
3. Click on the ‘+’ icon at the bottom and then click on `JARs and directories`
4. Navigate to the file that contains the common-csv-1.8.jar file (in the ‘lib’ folder of your modelchecking project) and select it.
5. Click the checkbox next to newly added common-csv module, then click Apply at the bottom of the window. then click Okay.

The CSVParser should work now!

:::

### Checking for Unsafe Behaviors

Recall our traffic light example, where we wanted to check that both lights could not be green at the same time. Assume that you had a `StateMachine` object named `Traffic` with the contents from the figure. We want to write this check as:

Traffic.checkNever(state => state.hasLabel("bigAveGreen") && state.hasLabel("smallStGreen"))

Here, `checkNever` is a method that runs the provided function on every reachable state (node). Sometimes, we prefer to express checks positively, in which case we'll use a corresponding method called `checkAlways`.

Your `StateMachine` class must provide these two methods. Specifically:

`checkAlways(checkNode: (StateData => Boolean)): Option[Node[StateData]]` checks whether the `checkNode` function returns `true` on every state that is reachable from the `startState`. The function returns `None` if the function is true on all states, otherwise it returns `Some` with a Node on which the function fails.

`checkNever(checkNode: (StateData => Boolean)): Option[Node[StateData]]` checks whether the `checkNode` function returns `false` on every state that is reachable from the `startState`. The function returns `None` if the function is false on all states, otherwise it returns `Some` with a Node on which the function returns true.

**Requirements**
- You can assume that the predicates will only involve boolean expressions over uses of `hasLabel`.
- Both methods should always return, without going into an infinite loop.
- These two methods will have a lot of similar code. Your final solution will share the common code between these two methods (this will be checked in grading)

:::spoiler An Optional, More Advanced Check (Liveness)

*This part is not required, but is here in case you find this interesting and want to try at some point*

Also implement the following function:

`checkEventually(checkNode: (StateData => Boolean)): Boolean` which checks whether the `checkNode` predicate is guaranteed to return true at some point (meaning, there are no cycles in the graph on which the predicate is false in all states).
:::

Written Questions
==

In your `README`, please provide answers to the following. (Each question is tagged with the learning objective that it supports.)

1. What is the worst-case running time of your `checkNever` method? State your answer and briefly justify it. Your answer should explicitly state what the variable is (as in "quadratic in n where n is the number of turtles in the marina". Either terms like "quadratic" or formulas like $n^2$ are fine.) [*Objective: time/space*]
2. ~~Assume that you knew that your program had an error (it previously crashed, but you didn't know why).~~ *[Updated 4/12 for clarity]* Assume that you knew some state would violate `checkNever`, but you don't know which one (so you still want to run the `checkNever` algorithm to figure out where it is). Would that change the worst-case running time? Why or why not? [*Objective: time/space*]
3. Assume that we had asked you to modify `checkNever` and `checkAlways` to return not just an `Option[Node[StateData]]` (indicating whether there is a state that passes/fails the check), but also the path from the start state showing how to get to the error state (if one exists). How would this change the running time? Explain your answer. [*Objective: time/space*]
4. Continue with the previous question's setup about returning the path to a violating state. What would you use as the return type of `checkNever` and `checkAlways` in this situation? [*Objective: OOdesign*]
5. You implemented one of the two Graph representations (Adjacency List or Adjacency Matrix).
- Why did you implement the one that you did (honesty here is just fine)? [*Objective: choosingDataStructures*]
- State one performance-related advantage to each representation as a contrast the other [*Objective: time/space*].
- Briefly explain any programmer/coding-facing tradeoffs between them [*Objective: choosingDataStructures*]

Socially-Responsible Computing (Optional)
==

**The SRC component on this assignment is entirely optional**. *If you don't do it, your SRC objective grade will be finalized based on what you've already turned in (from Hwk6 and earlier). If you submit it, we will use it to make up for SRC points lost on earlier assignments. Note that SRC is only half of the analysis score, so if you already have the grade-range you want on SRC, this likely won't be worth submitting from a grade perspective.*

Review the information Facebook (instructions can be found [here](https://www.facebook.com/help/1701730696756992/?helpref=hc_fnav)) or Google (instructions can be found [here](https://support.google.com/accounts/answer/162744?hl=en)) have on you, then discuss the implications of this data using the [social threat-modeling table](https://docs.google.com/document/d/1PDYOcwgQmfSLS7YAAzoUlwoytvRr7_gDwM-BRkPa548/edit). Specifically, pick three cells of the table to discuss. Your writeup should separate your analysis of the three cells from one another, and clearly label your answers with the corresponding cells.

Testing
=======
Testing for this project will not be graded by wheats and chaffs. As such, you *will not be able to tell if you have covered certain test cases*. However, we still expect you to test your methods exhaustively.

You should have lightweight tests for the simple methods:
1. `createNode` and `addEdge` from your Graph class (the one you chose to implement),
2. `getContents`, `getNexts`, `addEdge` from your Node class.

Your objective here is to show us (one last time) that you know how to set up a test that a data-structure operation has the expected impact on the data. You do *not* need to test `show`.

For your `StateMachine` class:
1. Do substantial testing on `checkAlways` and `checkNever`. All of these listed methods should made `public` so that we may run our own tests against them as well.

Since there are no wheat or chaffs for this assignment, you will not run into autograder issues for testing helper methods. We will not grade testing on your helper methods, but we strongly recommend that you do at least some testing on them and that you use tests as an aid if you need to debug your programs.

You get to determine the access permissions on all other methods (your choices will count towards [*Objective: access modifiers*])

### Expectations

In grading your testing ([*Objective: writing tests*]), we will look for:
- whether you come up with an varied collection of graph shapes to test (for example, having all of your graphs look like traffic light, with only one edge leaving each state, has little variation)
- whether the predicates that you test exercise depth-first-search in varied ways (for example, having every formula that you test fail on a node in a two-node cycle has little variation)

**Note:** Bear in mind that you can get mileage out of a single graph shape by varying (a) which state you designate as the start state or (b) the labels on the states.

Your examples do **not** need to be realistic (as the traffic light was): it is fine for you to just create a state machine with meaningless labels against which you look for errors in different path and cycle configurations.

### Describing and Creating Tests

Upload a picture/image (as png, jpg, or pdf) of the graphs that you are using for testing. These should show the nodes and edges (as in the 9-state traffic light diagram above), and state labels from one of your tests. You can draw these by hand or with a tool. If you plan to use the same structure more than once, but with different labels for different tests, you only have to submit the drawing once. Just annotate the drawn diagram with a name and the IDs for the states, then use comments on your tests to explain which diagram and configuration you are using.

You may actually create your graph test cases either using the CSV interface or by writing manual setup nodes. Remember good testing style as well!

If you produce CSV files, please put them in the `data` folder. When you submit your project, submit the `data` folder. When you test your CSVs, you can refer to them wit the (example) filepath `data/sampleCSV.csv`. You don't need to worry about these filepaths for submission.

Project Tasks
=============
::: info
This is a solo assignment: the homework collaboration policy applies. We refer to this as a "mini project" because it has some of the open-endedness of a project, but you will not work with a partner (the amount of work will be on par with a homework).
:::

Design Check (Optional)
--
Design checks for this project are optional (it will not count towards your final grade). Design checks will be held from **Wed. April 7th through Fri. April 9th**. Sign up for a design check [here](https://docs.google.com/spreadsheets/d/18T5Bhyl0DYmRkSkG1jN5Z5aoJVTpFtCydfb0eTXXlYw/edit?usp=sharing).

Think of the design check here as a pre-scheduled office hour slot with a TA where you can talk through your understanding of the assignment. Things you might want to discuss are:

- Your plan for working on the project: what sequence of smaller steps will you take to build up to your solution?
- Your ideas for interesting graphs and label patterns to test
- How you envision using depth-first search to implement `checkNever` and `checkAlways`
- Which methods you want to include in each class

Source Code
-----------
Get the stencil code here: https://classroom.github.com/a/r3edEki4

Final Submission
----------------
The final submission is due on Gradescope by **April 16th at Anywhere-on-Earth time**.

You must submit to the correct Gradescope assignment (for autograding purposes):
- If you implemented the Adjacency List Graph, submit to `Model Checking: Adjacency List Graph Implementation`.
- If you implemented the Matrix Graph, submit to `Model Checking: Matrix Graph Implementation`.

Please submit on Gradescope:
1. All `.scala` files in your `sol` folder. Please *exclude* the files from your `src` folder.
2. The `data` folder.
3. The drawings of your graphs used in testing.
4. A `README` (txt or pdf) file that includes:
- An outline of your code and how it works together
- Documentation of each test file that you created (if any).
- Your answers to the "Written Questions".
5. (Optional) Your answers to the Socially-Responsible Computing questions in a (txt or pdf) file called `SRC`.

Revisiting the Big Picture
-----------

This project has only scratched the surface of model checking. If you found this interesting, consider taking CS1710: Logic for Systems, which is all about this idea of using logic for exploring system behavior. Model checkers are a maturing technology; they belong to a broader class of tools called *formal methods* that are seeing various use in industrial software development. In fact, the researchers who first proposed algorithms for model checking won the Turing Award (the CS analog of a Nobel Prize) for this work.

Of course, when we analyze systems in practice, the graphs get pretty big. How big? REALLY big (as in more-nodes-than-pages-on-the-internet big). Which means we need special data structures that are tailored to computing reachability on very large graphs. We've only scratched the surface. But in one of our final CS18 lectures ...