# Assignment 1

#### 1. Spanning Tree

- Implement a predicate that takes a binary relation as input (on
**univ** set) and tests whether or not the relation is a *tree*.
- Implement a predicate that takes two binary relations as input and constrains one to be a spanning tree of the other. Use this predicate to give an example of a graph with two distinct spanning trees. Note that the versions of the predicate may be different for directed or undirected graphs. Specify both the versions.
- Consider a weighted undirected graph. Implement a predicate to check whether a given relation forms an MST.

### 2. Report

- Create a report in latex clear.y explaining how you iteratively refined your model and how did Alloy help you to indentify counter-examples in your modeling process.

Last updated on Dec 29, 2019