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.