doyeka/final_project

Logical Model of Graphing Algorithms

We used the MIT logical modeling software alloy to model Prim's, Kruskal's, and Bellman-Ford algorithms.

Modeling a Graph Algorithm

We attempted several different graph models, the variation between them coming from how they represented edges. At first, our desire to show weighted edges seemed to necessitate that we make an edge sig with a weight attribute. However, after some trial we settled on Node -> Int -> Node which allows us to model connectedness and visualizes well.

Prim and Kruskal

Prim's forced us to model adjacency, connectedness, and how to create a Source node. Kruskal's forced us to further consider connectedness. We needed a way to test if a graph was cyclic, which initially seemed impossible for weighted edges. The solution turned out to be a function getUnweightedEdges, which taught us of the strange implicit return values in alloy (see the function declaration for more details). With this tool, along with the function getWeight allowed us to properly reason about cycles.

We compare the two in the file prim-kruskal-test.als. This comparison led us to create a shared Node definition between the two MST algorithms. However, we wanted them to have different State sigs so that we could see how each generated an MST starting from the same input. nonUniqueMST shows the conditions under which Prim's and Kruskal's algorithms might find different results. The crucial step is in finding some potential edge that can be added to an MST to make a cycle and swapped for another edge in the cycle. See the nonUniqueMST definition for more information.

We chose to implement Prim's and Kruskal's algorithms on connected graphs. Though they could have been implemented to make minimum spanning forests instead of trees, we were more focused on MSTs and this abstraction made reasoning about MSTs simpler.

Dijkstra and Bellman-Ford

To view these shortest path algorithms, we recommend that in addition to projecting over State and Event to also show distance and infinite sigs as attributes rather than arcs.

We decided to model Dijkstra's model with an infinity relation to shows which nodes have an infinite distance variable. Though this required our model to be slightly more complicated, it results in a more scalable model since the our representation of "inifinity" need not change with a greater integer bit-width.

In addition to the sigs and relations from Dijkstra, Bellman-Ford made us create anotherStepPossible predicate. After run for |N|^2 States, anotherStepPossible implies a negative cycle. When Dijkstra's is run on the same input it simply generates an incorrect tree instead of noting this. Unfortunately, the numerous steps required for Bellman-Ford means that it is extremely slow, and is best run on two nodes, but these are enough to see its functionality. Since this was our reach goal, we are proud of what we were able to accomplish with Bellman-Ford.

final_project's Issues

Can't update distance attribute

Problem:

Right now there's no way to change the distance variable of a node. It is defined as a static sig i.e. Node maps to a single int sig.

Proposed solution

Add distance to the State sig. This means that I'll be able to say something like:

all n : Node | post.distance.n = pre.distance.current + incidentEdge[current, n]

Bellman-ford can be fooled

Problem

There could be a cycle that doesn't get chosen as current in the penultimate state and thus wouldn't change weights, so our algorithm wouldn't detect the negative cycle.

Proposed solution

Assert that there's no possible way to change the edge weights

All the edges have the same weight

Problem

I'm not sure if it's just because of some strange alloy default, but right now all of the edges have the same edge weight. When I change the constraints under positiveEdgeWeight so that all weights must be greater than some number, e.g. 5, all the edge weights will switch to a different number, e.g. 6, but they will still all be the same weight.

Proposed solution

Delete predicates until the graph once again has random edge weights and modify the code accordingly so that the graph is always like this.

Neighbor distances aren't updated properly

Problem

I added this section of code to the Event sig fact in order to update neighbors:

-- update distance variables of neighbors
all v : Node | isAdjacent[pre, current, v] implies {
	-- if infinite or greater distance than current + incident edge
	let new_dist = pre.distance[current] + pre.graph[current].v | {

	 	pre.infinite[v] = 1 or pre.distance[v] > new_dist  implies {
			post.infinite[v] = 0
			post.distance[v] = new_dist
		}
		
		pre.infinite[v] = 0 and pre.distance[v] < new_dist implies {
			post.infinite[v] = 0
			post.distance[v] = pre.distance[v]
		}
	}
}

all v : Node | not isAdjacent[pre, current, v] implies {
	post.infinite[v] = pre.infinite[v]
	post.distance[v] = pre.distance[v]
}

However, for some reason in the post State the neighbors are getting sets of random values as their distance values.

Proposed solution

Figure out where we are underconstrained and add a constraint so that there is a well defined value for the distance value of every node for both pre and post.