Modeling 2: Trees and graphs

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

Additional Alloy Resources

For additional resources on Alloy syntax or operators, check out:

Assignment description

You should not use any external Alloy modules for these problems. Your solutions should each terminate within 10 seconds.

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

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.

Click after we have completed the pseudocode in Workshop.

This problem resolves to finding a "minimum spanning tree" on an undirected, weighted graph. Weighted graphs are graphs where every edge has some numeric weight.

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!


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

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.

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:

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. 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) and connected. In class, we went over several equivalent definitions of undirected trees.

Your task: complete the following template to specify a model for non-trivial, undirected trees.

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?

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

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:

// 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]

Note: this is an [INDEPENDENT] problem that you should discuss only with your partner and the instructor.

Some communication protocols 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.

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:

sig Node {
  succ: set Node
}
pred isRing {
  ...
}
run isRing for 5 but 0 Int

Write your answer in a new Alloy file, ring.als.

Grading

In your README, also report:
Written Q4: Collaborators other than your partner?
Written Q5: Roughly how long did this assignment take you (in hours)?

This assignment is worth 100 points, broken down by:

Submission

Submit the following 4 files on Gradescope: directed_trees.als, undirected_trees.als, ring.als, and README.{txt, md}.

Attribution

Exercises adapted from Appendix A of Daniel Jackson's Software Abstractions.