---
tags: Projects-Summer2021
---
# Mini-Project: Model Checking
### Due Date: Friday, August 6, 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

### Background
In the mid 1980's, the [Therac-25](https://en.wikipedia.org/wiki/Therac-25) computer-controlled radiation machine malfunctioned and administered lethal doses to several patients. An independent investigation found that the root cause of the incident was "poor software design and development practices." In more recent years, we've heard concerns about critical errors in software-controlled cars, planes, 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!

In this project you will implement two different graph representations, as well as build a simple **model checker**: a program that can be used to check the safety of a system to help avoid potentially disastrous errors like those described above.

### Learning Objectives
- build and compare different implementations of graph structures
- apply graphs and graph algorithms to a specific problem (model checking)
- develop and use comprehensive testing for your program

## Setup

### Stencil Code
You can clone your individual project repository with stencil code [**here**](https://classroom.github.com/a/F9EMPFe1).
::: info
As this is an individual assignment, the standard 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.
:::
### Dependencies (CSV Parsing and Testing)
1. In Intellij, go to **File** -> **Project Structure**
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 `lib` directory of your repository and select `commons-csv-1.8.jar` and `tester.jar`.
5. Click **Okay** to save the setting

## Programs as Graphs

We can think of a program as describing a (very) large graph. Each node of the graph represents the **state** of the program at a given moment, where the state is defined as the *mapping between the programs variables and their values*.

As a program runs, it ***transitions*** between states as the values of its variables change. An edge from node `A` to node `B` in the graph means that the variables in the program changed their values from those at state `A` to those at state `B`. Consider the following example...

### Single Traffic Light Example
Imagine that you wrote the following program to manage a single traffic light. The program uses a `Timer` library, with a countdown timer that "expires" when time runs out and can be restarted using `restart()`.

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 continue to cycle its colors forever as long as the timer continues to expire (the timer restarts are not in the picture).


### Intersection Traffic Light Example

In a real traffic intersection, there are *two* color variables, one for each of the intersecting streets. There are also usually multiple timers (a short one for the *yellow-to-red* transition and a longer one for the *green-to-yellow* transition). Given this information, we get a more complicated graph such as the following example. Consider the traffic lights at the intersection of two streets on campus, **Hope** and **Waterman**. There is a `String` variable for each street `hope` and `waterman`, where each variable stores the current color of that street's lights as either `"red"`, `"yellow"`, or `"green"`.


### 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 state does exist in the graph, but the real question is *whether or not that node can be reached in practice*. If the traffic lights start up in the configuration `{hope: red, waterman: green}` (the top-left node), for example, there is no way to follow the edges to get to the double-green node. However, if the lights start up in the configuration `{hope: yellow, waterman: yellow}`, we could reach the double-green configuration, and an accident could occur!

### Model Checking
There are two key parts of traversing a graph to check system safety:
- Write a predicate (function that returns boolean) that captures the **bad** condition. This will be a function that takes in a state and outputs a `Boolean` for whether or not the given state satisfies the bad condition.
- Traverse the graph to check whether any state that is reachable from the initial system of the 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 traversal step from above:

- Check whether there is a cycle reachable from the start state in which the good condition is never satisfied (such a cycle means 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 both safety and liveness.

## Implementation Architecture

Your implementation of a model checker will consist of two main parts:
- Classes and interfaces for generic graph representation
- Classes and interfaces for a State Machine with model checking functionality

Here is a diagram that outlines the architecture. The classes in green are what you will be implementing in this assignment.

### Graph Representations

For this assignment, you will implement both of the following two graph representations, an adjacency list and an adjacency matrix, in their respectively classes `AdjacencyList.scala` and `AdjacencyMatrix.scala`. Both classes implement the same `IGraph` trait, meaning they share the same behaviors and can be used to do the same things, however behind the scenes they work differently.

#### 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 the collection all of the nodes to which it is connected by outgoing edges. This is how we have used graphs in lecture.
:::info
You also most likely dealt with this representation in **Search**, when you stored the page link structure of a corpus (yes, that was a graph!).
:::

#### Adjacency Matrix

Another way to represent a graph is to use a 2D array (matrix) of booleans that stores information about edges between nodes, 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 to figure out a way to map each node to its index (the same index in each matrix dimension).

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. See the below example of a simple graph represented by an adjacency matrix...


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 an `IllegalStateException` with an informative message if users attempt to add more nodes than the number allowed by `maxSize`.

### Graph Implementation

You will find the traits that you need to implement in the files located in the `src` package of the project. These traits encapsulate how you will be representing and building graphs. Each of these traits, `IGraph` and `INode`, have several methods that you will need to implement.

#### Implementing `IGraph`

Classes that extend the `IGraph` trait (i.e. the `AdjacencyList` and `AdjacencyMatrix` classes in the `sol` folder) will need to implement the methods `addNode`, `addEdge`, and `show`.
* `addNode` should add a new `INode` to the graph with specified contents and return that new `INode`. It should *not* build any edges.
* `addEdge` should take in as input two `INode` objects and build an edge between them.
* `show` should take no inputs and return nothing, but should print the representation of the graph legibly.

#### Implementing `INode`

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

* `getContents` should return the contents of the caller `Node`.
* `getNexts` should return a `List[Node]` that contains every `Node` to which the caller `Node` connects.
* `addEdge` takes in a `Node` and builds a connection to it from the caller `Node`. It should not return anything.

<!-- ### General Archiecture
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

- Two different implementations of the `IGraph` trait: `AdjacencyList` and `AdjacencyMatrix`
- A `StateMachine` class that uses the `Graph` interface to build a specific state graph and provides methods for checking both safety and liveness of the state 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. -->

### Model Checking Classes

A *State Machine* (like the second traffic light example above) consists of a finite collection of discrete *states* and *transitions* between different states. This can be captured in a graph structure of nodes and edges.

#### State

In the `src` package you will find `State.scala`, a class that stores the data of a state in a program graph. A `State` has two fields:
- `id: String` : a unique identifier for the state. No two states in the same state machine graph should have the same `id`
- `data: Map[String, String]` : the state of the program's variables, where the keys in the map are regular, alphanumeric string variable names and the values are regular, alphanumeric string variable values.

#### State Machine
Your state machine implementation, `sol/StateMachine.scala`, implements the `IStateMachine` trait in the `src` package. You should read the Scaladocs in the trait for more details about the methods and their expected behavior. Your `StateMachine` class will implement methods for populating the state machine's state graph:
- `addState`, `addTransition`, and `initFromCSV`

Therefore, there are two ways to populate the state graph of a state machine: manually adding states and transitions in code via `addState` and `addTransition`, or by calling `initFromCSV` to add all the states and transitions from CSV files. Your implementation must support both of these.
:::warning
For these methods it is important that you ensure that the caller does not add a new state with the same `id` as a state already in the state graph or try to add a transition between states that are not in the state graph. If either of these situations occurs, you should throw an `IllegalStateException`.
:::

You also must implement model checking methods to test the *safety* and *liveness* of a program graph:
- `checkAlways`, `checkNever`, and `checkEventually`

These methods are described more in detail in the following section.

### Model Checking Methods

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:

val traffic: StateMachine = setupTrafficStateMachine()

def areBothLightsGreen(state: State): Boolean = {
    state.data("hope") == "green" && state.data("waterman") == "green"
}

traffic.checkNever(initialState, areBothLightsGreen)

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 three methods:

#### `checkAlways`

- `checkAlways(startState: State, checkState: State => Boolean): Option[State]` checks whether the `checkState` function returns `true` on every state that is reachable from the `startState`. The function returns `None` if the function returns `true` on all states, otherwise it returns `Some` with a *counterexample*, a `State` on which the function returns `false`.

#### `checkNever`
- `checkNever(startState: State, checkState: State => Boolean): Option[State]` checks whether the `checkState` 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 state on which the function returns true.

#### `checkEventually`
- `checkEventually(startState: State, checkState: State => Boolean): Boolean` which checks whether the `checkState` predicate is ***guaranteed*** to return `true` at some point, starting from the `initialState` (meaning, there are no cycles in the graph on which the predicate is `false` for all states, or paths that terminate without reaching a positive state).

#### Requirements
- All methods should always return, without going into an infinite loop.
- `checkAlways`, `checkNever`, and `checkEventually` will have a lot of similar code, so you should try to abstract as much as you can.
- You can assume that the predicates passed in to the model checking methods will only look at the fields of the `State` object and will not perform additional costly computations.

:::info
Note that the `checkAlways` and `checkNever` methods take in and return `State` objects, while `chekEventually` returns a boolean. Your `StateMachine` class should handle the interaction between these inputs and outputs and the underlying `INode[State]` graph structure.
:::

## CSV Parsing

To make it easier for a user to populate state graphs, your `StateMachine` class will provide the option to initialize from CSV files through the method:

  def initFromCSV(statesCSV: String, transitionsCSV: String): Unit

This method takes in paths to a CSV file defining the **states** of the state graph, `statesCSV`, and a CSV file defining the **transitions** between states, `transitionsCSV`. It will parse these files and build up the state graph nodes and edges (states and transitions).

### File Format

#### statesCSV

A valid `statesCSV` file has a header labeling the columns `id` and `data`, and one row per state in the state graph

Below is an example CSV file for states that contain the variables `color`, `count`, and `isActive`

id,data
s1,color=green;count=0;isActive=false
s2,color=orange;count=10;isAcitve=true
s3,color=red;count=20;isActive=false
...

#### transitionsCSV
A valid `transitionsCSV` file has a header labeling the columns `from` and `to`, one row per transition, where a transition is a directed edge between two states in the state graph. `from` and `to` represent the IDs of the origin and destination states of the edge respectively.

Below is an example CSV file for transitions between states.

from,to
s1,n2
s2,s3
s3,s1
...

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

### Helper Code
To help you implement the CSV parsing part of this assignment, we have provided a `Parser` object in the `src` package, which contains a method `parseCSV` for you to call in `initFromCSV` to handle most of the interaction with the `commons-csv` library:

def parseCSV(csvFile: String, parseRecord: CSVRecord => Unit): Unit = {
    ...
}

Notice that in addition to a filepath, the method takes in a **function** as a parameter. You will write your own `parseRecord` function that will handle parsing an individual row in the csv file and pass them into `parseCSV`. Think about what your `StateMachine` will want to do with each row in the `statesCSV` file and the `transitionsCSV` file and write your functions accordingly. To learn more about what is contained in a `CSVRecord` object, refer to the library documentation [**here**](https://commons.apache.org/proper/commons-csv/apidocs/org/apache/commons/csv/CSVRecord.html).

:::warning
Your parsing methods should throw an informative exception if a `statesCSV` file contains duplicate state ids or if a `transitionsCSV` entry references a state that was not present in `statesCSV`. This may be handled by other parts of your code.
:::

## 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. We provide two files in which to write your tests: `GraphTestSuite.scala` and `StateMachineTestSuite.scala`.

In `GraphTestSuite.scala`, you should write lightweight tests for the simple methods:
- `addNode` and `addEdge` from your Graph classes,
- `getContents`, `getNexts`, `addEdge` from your Node class.

:::info
**Note:** It's tricky to test `addNode` since you don't have access to the nested Node classes. You should use `getContents` to test `addNode`.
:::

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`. **Make sure that you test both of your graph implementations.**

In `StateMachineTestSuite.scala`, you should have extensive testing for the following methods from `StateMachine`:
- `checkAlways`, `checkNever`, and `checkEventually`.

For the more complicated graph-traversal methods, make sure you think about and test potential edge cases!

We will not grade testing on your helper methods, but we strongly recommend that you do at least some testing on them to help isolate problems in your code when debugging.

### Expectations

In grading your testing, some things we will look for are (but aren't limited to):
- 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)

:::info
**Tip:** you can get more mileage out of a single graph by varying (a) the initial state of the traversal or (b) the predicate/condition being checked
:::

Your examples do **not** need to be realistic (as the traffic light was): it is fine for you to create state graphs with non-sensical state data, as long as the tests are still covering valid cases.

### 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 with the (example) filepath `data/sampleCSV.csv`. You don't need to worry about these filepaths for submission.

## Written Questions
For this assignment, we also ask that you complete a number of written reflections. In your `README`, please provide answers to the following in a clear, well formatted (enumerated) manner. 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 represents (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 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[State]` (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 two Graph representations (Adjacency List and Adjacency Matrix).
- 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

**Task:** Review the information that 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)) collect about you.

**Task:** Discuss the implications of this data using the [social threat-modeling table](https://docs.google.com/document/d/1PDYOcwgQmfSLS7YAAzoUlwoytvRr7_gDwM-BRkPa548/edit). Specifically, pick two cells of the table to discuss. Your writeup should separate your analysis of the two cells from one another, and clearly label your answers with the corresponding cells. (~4 sentences per cell)

**How to Hand In/Grading:**
Submit your work as a single PDF file on Gradescope to the **Model Checking: SRC** submission portal. Do not include your name or other identifying fields anywhere in your response. This, like all assignments, is subject to the course collaboration policy.

## Design Check (Optional)

Design checks for this project are optional (it will not count towards your final grade). Design checks will be held from **Tuesday July 27th through Fri. July 30th**. If you would like to have a design check, fill out the form [**here**](https://forms.gle/S6oA28z5cqcQHTyTA) by **Sunday July 25th at 11:59PM EST.**

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`, `checkAlways`, and `checkEventually`

## Final Submission

The final submission is due on Gradescope by **August 6th at Anywhere-on-Earth time**.

### Code

Please submit on Gradescope:
1. All `scala` files in your `sol` folder. **Do not submit any files from the `src` package**
- At a minimum: `AdjacencyList.scala`, `AdjacencyMatrix.scala`, `StateMachine.scala`, `GraphTestSuite.scala`, and `StateMachineTest.scala`
3. All files from your `data` folder.
4. The drawings of your graphs used in testing.
5. A `README` (txt or pdf) file that includes:
- An outline of your code and how it works together
- A description of any bugs in your program
- Documentation of each test file that you created (if any).
- Your well-formatted answers to the **Written Questions**

:::info
If you are are aiming for an A or S with Distinction in the course, you should complete the entire assignment as described (this will be required to receive those grades). However, if you are not, you may opt not to complete the `AdjacencyList` implementation as well the `checkEventually` method in `StateMachine`. You must still complete all of the other methods and classes, as well as the SRC.

**Important:** you must still submit all of the required files, and do not comment out the `AdjacencyList` class or any of its methods or `StateMachine.checkEventually` (even though you did not implement them). This is to ensure that your code still compiles with the autograder.
:::

### SRC
Follow the instructions in the **SRC** section of the handout to submit it!

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