You should not use any external Alloy modules for these problems. Your solutions for this assignment should terminate within 10 seconds. For each problem, please add additional constraints as needed to make the instances nontrivial.

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.

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. What exactly are these properties? Express them in relational logic as much as possible (though we do not prohibit you from using quantifiers), and illustrate with a few examples. Note you should express the properties for a tree, not a forest.

Here is a template to help you:

pred isDirectedTree (r: univ -> univ) { ... }
run isDirectedTree for 4

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 used in the domain of graph theory 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. 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 (can you see why?).

Complete the following template:

pred isUndirectedTree (r: univ -> univ) { ... }
run isUndirectedTree for 4

Note: you should not use the Int type in Alloy for this problem, because counting does not scale well in Alloy.

Hint: a graph must contain a cycle if for any edge e = (u,v), there is a path from u to v that does not use e.

Problem 3: Spanning Trees

A spanning tree of a graph is a subgraph that is an undirected tree and that covers all the nodes in the original graph. Based on this definition, create a model in Alloy that will produce instances of a graph with two distinct spanning trees.

Here is a template to help you:

pred isUndirectedTree (graph: univ -> univ) { ... }
pred spans (graph1, graph2: univ -> univ) { ... }
pred showTwoSpanningTrees (graph, tree1, tree2: univ -> univ) { ... }
run showTwoSpanningTrees for 3

where pred spans (graph1, graph2: univ -> univ) { ... } means graph1 spans graph2 (graph1 is a subgraph of graph2 and also covers all the nodes in graph2) and pred showTwoSpanningTrees (graph, tree1, tree2: univ -> univ) { ... } means both tree1 and tree2 spans graph.

Spanning trees have many uses. In networks, they’re often used to set up connections. In the Firewire protocol, for example, a spanning tree is automatically discovered, and the root of the tree becomes a leader that coordinates communication.

Problem 4: Rings

Some communication protocols organize nodes in a network into a ring, with 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. You should model the edges on this graph as directed.

Here is a sample Alloy model in which you can implement your constraints, and then execute the command to see if the instances you obtain are indeed rings:

sig Node {succ: set Node}
pred isRing () {
	...
}
run isRing for exactly 4 Node

Handing In

Run cs1950y_handin alloy2 from a directory holding your 4 Alloy files (directed_tree.als, undirected_tree.als, spanning_tree.als, ring.als). You should receive an email confirming that your handin has worked.

Credit

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