Modeling 2: Trees and Graphs

Modeling 2: Trees and graphs ------ # Learning outcomes :::info In this assignment, you will: - Practice converting a English language problem description into a specification, and work on an algorithmic solution. - Model directed and undirected graphs and trees. - Use nested quantifiers to express more complex properties, such a acyclicity on an undirected graph. - Model a specific network topology. - _Optionally practice more Rust programming_. ::: 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 assignment. ## Additional Alloy Resources For additional resources on Alloy syntax or operators, check out: * [The official Alloy documentation](http://alloy.mit.edu/alloy/documentation.html) * [A quick reference guide to most Alloy operators](http://www.ics.uci.edu/~alspaugh/cls/shr/alloy.html) # Assignment description You should not use any external Alloy modules for these problems. Your solutions should each terminate within 30 seconds. :::success For each problem, please add additional constraints as needed to make the instances nontrivial. That is, the empty instance should not be a possible instance of each of your solution models. ::: ## Problem 0 (ungraded, participation credit) You are a network engineer tasked with configuring a network of individual servers. You are provided with a list of possible connections between the servers (not all pairs of servers are able to be connected, based on physical layout) and an estimate of the latency (time delay) for each connection. Your task is to determine the lowest-cost way of enabling communication between all of the servers. (:dark_sunglasses: This is a problem encountered by all sorts of real-world routing problems, including the design of roads in a city or country). :::warning Note: you may not have seen this type of problem before if you've taken CS230 but not CS231, which is why this is an ungraded exercise. During Workshop, we will work in groups to solve this problem in pseudocode, but you do not need to actually code a solution for this assignment. ::: <details> <summary>Click after we have completed the pseudocode in Workshop. </summary> <br> :::info This problem resolves to finding a ["minimum spanning tree"](https://en.wikipedia.org/wiki/Minimum_spanning_tree) on an undirected, weighted graph. *Weighted* graphs are graphs where every edge has some numeric weight. It Two solution sketches: - [Prim's algorithm](https://en.wikipedia.org/wiki/Prim%27s_algorithm) is similar to Dijkstra's algorithm for finding the shortest path in a graph (Dijkstra co-invented Prim's). It works by starting from an arbitrary vertex, then builds the tree by choosing an outgoing vertex that is not currently in the tree but is reachable via one edge. - [Kruskal's algorithm](https://en.wikipedia.org/wiki/Kruskal%27s_algorithm) works by selecting the lowest-weight edge overall that does not form a cycle. It uses the union-find algorithm to track disconnected components in order to prevent cycles. In problems 2 and 3 on this assignment, you will precisely define *undirected trees* and *spanning trees* in Alloy. We do not yet have all the right Alloy building blocks to model one of the algorithmic solutions for *finding* a minimum spanning tree in Alloy, but we will cover those in the coming weeks! ::: </details> <br>  ## Problem 1: Directed Tree Properties A tree has several canonical definitions within computer science that you may be familiar with. In the most common definition, [a tree is a data structure](https://en.wikipedia.org/wiki/Tree_(data_structure)) consisting of nodes and **child pointers** to other nodes. Each child has only one parent (except the root node, which has zero parents), and each node may have one or more children (note: we are not restricting to binary trees.) The child pointers cannot form a cycle. This may also be referred to as a directed tree. Directed trees have many applications across computer systems and networks. My personal favorite example is [dominator trees](https://en.wikipedia.org/wiki/Dominator_(graph_theory)) for control-flow graphs, used within optimizing compilers! The above description and Wikipedia page describe directed trees informally and formally in English and mathematical notation. A directed tree can also be described as a relation that satisfies some properties. :::success Your task: write a model that specifies a non-trivial directed tree using a minimal set of properties. Express your properties in relational logic as much as possible (though you may choose to use quantifiers and the predicate calculus style). Note you should express the properties for a **tree**, not a [forest](https://en.wikipedia.org/wiki/Tree_(graph_theory)#Forest). Write your answer in a new Alloy file, `directed_trees.als`. Begin a `README.{md, txt}` file. Answer the following: **Written Q1:** Which of your properties constraints the model to be a tree, rather than a forest? Briefly describe how this property works. ::: Here is a template to help you: ```java pred isDirectedTree (r: univ -> univ) { ... } run isDirectedTree for 5 but 0 Int ``` Replace the ellipsis with some constraints on the relation `r`, and execute the command to visualize some sample instances.  ## Problem 2: Undirected Tree Properties Another common definition of a tree is an [undirected tree](https://en.wikipedia.org/wiki/Tree_(graph_theory)). In an undirected *graph*, rather than pointers from one node to another, there are edges between nodes that have no orientation. That is, an edge from a node `a` to a node `b` is also an edge from `b` to `a`. As we saw in class, an undirected graph can be represented as a binary relation, constrained to be symmetric. An undirected *tree* is an undirected graph in which there is exactly one path between any two distinct vertices. This is equivalent to stating that undirected trees are acyclic (lacking [cycles](https://en.wikipedia.org/wiki/Cycle_(graph_theory))) and [connected](https://en.wikipedia.org/wiki/Connectivity_(graph_theory)#Connected_graph). In class, we went over several equivalent definitions of undirected trees. :::success Your task: complete the following template to specify a model for non-trivial, undirected trees. ```java pred isUndirectedTree (r: univ -> univ) { ... } run isUndirectedTree for 5 but 0 Int ``` Write your answer in a new Alloy file, `undirected_trees.als`. **Written Q2:** Does your definition of an undirected tree allow self-loops (that is, edges from a node to itself)? Why or why not? ::: :::danger Note: you should not use the Int type or the `#` operator in Alloy for this problem, since counting does not scale and is not necessary for this model. ::: :::warning Warning: if you see an error about skolemization, you are probably trying to quantify over a relation directly. Instead, see the class notes for how to reformulate this as a quantifier and implication over elements of the set the relation is on. :::  ## Problem 3: Spanning Trees A spanning tree of an undirected graph is a [subgraph](https://en.wikipedia.org/wiki/Glossary_of_graph_theory#Subgraphs) that is an undirected tree and that covers all the nodes in the original graph. Spanning trees have many applications in computer systems. In networks and distributed systems, spanning trees are used to find optimal communication topologies. :::success Your tasks: 1. Transform this informal definition into a precise specification with an Alloy Model. 2. Give an example of a graph with two distinct spanning trees as a comment. Your example should be written with simplified names, as in Modeling 1, but need not otherwise be minimal. Include all relevant sets and relations needed to describe the example. Here is a template to help you: ```java // You can reuse your existing solution from the previous problem. pred isUndirectedTree (r: univ -> univ) { ... } // True iff graph1 spans graph2 (`graph1` is a subgraph of // `graph2` and covers all the nodes in `graph2`). pred spans (graph1, graph2: univ -> univ) { ... } // True iff tree1 and tree2 are distinct spanning trees of // graph. pred showTwoSpanningTrees (graph, tree1, tree2: univ -> univ) { ... } run showTwoSpanningTrees for 5 but 0 Int ``` Add your answer to your existing Alloy file, `undirected_trees.als`. Recall that you can use the Execute menu in the Alloy Analyzer to select which command to run. **Written Q3:** Is it possible for a graph to not be a tree, but have exactly one spanning tree? Why or why not? ::: Note that this problem does not tell us anything about *how* to find a spanning tree, given a graph. In the next few weeks, we'll see how to model events and traces in Alloy in order to show how we can model algorithms that actually produce output, for example, modeling an algorithm that produces a spanning tree given a graph.  ## Problem 4: Rings [Independent] :::warning Note: this is an **[INDEPENDENT]** problem that you should discuss only with your partner and the instructor. ::: [Some communication protocols](https://en.wikipedia.org/wiki/Ring_network) organize nodes in a network into a ring, with directed links from node to node forming a circle. Characterize, as simply and concisely as you can, the constraints on `next`, the relation from node to node, that ensures that it forms a ring. :::success Your task: complete the following template to specify a non-trivial, directed ring. Be as concise as possible. Be sure to check instances in the Analyzer the command to see if the instances you obtain are indeed rings: ```java sig Node { succ: set Node } pred isRing { ... } run isRing for 5 but 0 Int ``` Write your answer in a new Alloy file, `ring.als`. ::: ## Problem 5: Extra credit: Implement MST While we don't yet have the tools to model an MST-finding algorithm in Alloy, this is another chance to practice algorithmic and Rust programming skills! Implement an MST-finding algorithm of your choice in Rust. You may reference existing pseudocode, but avoid looking at other full implementations (and list any reference pseudocode in your README). Your implementation should consume graphs in a form similar to PBT (one edge per row), but (1) edges should be undirected/assumed to be bidirectional, and (2) there should be an additional value per line for the edge weight. Similar to PBT, your implementation should expect to read one graph from `stdin`. Your implementation should produce the output MST in the same format to `stdout`. For example: Input weighted undirected graph: ``` 1 2 100 2 3 90 3 1 80 ``` Output MST: ``` 2 3 90 3 1 80 ``` You can assume all edge weights are positive and that the input graph is connected. For full extra credit points, include either 10+ hand-written unit tests and/or property-based testing. Implement your algorithm in a file named `main.rs` and include a `Cargo.toml` file. # Grading :::success In your README, also report: **Written Q4:** Collaborators other than your partner? **Written Q5:** Roughly how long did this assignment take you (in hours)? **Written Q6:** _Optionally, if you implemented Problem 5, describe your implementation and testing choices here_. ::: This assignment is worth 100 points, broken down by: :::info - 15: Problem 1 - 30: Problem 2 - 20: Problem 3 - 20: Problem 4 - 15: `README`/**Written Qs** 1-5 - _(optional) up to +20 Rust implementation of MST_ ::: # Submission Submit the following 4 files on Gradescope: `directed_trees.als`, `undirected_trees.als`, `ring.als`, and `README.{txt, md}`. Optionally, submit `main.rs` and `Cargo.toml`. # Attribution Exercises adapted from Appendix A of Daniel Jackson's [Software Abstractions](http://mitpress.mit.edu/books/software-abstractions).