Graph Analysis

The real power of Transit becomes apparent when we convert the reflected data structure into a general-purpose graph. Using mkStateGraph, we transform the Transit specification into a StateGraph — a specialized Graph type configured with edge and node labels suitable for state machine analysis.

bridgesGraph :: StateGraph
bridgesGraph = mkStateGraph bridgesTransit

^{🗎 test/Examples/BridgesKoenigsberg.purs L97-L98}

Eulerian trail

Once we have this graph data structure, we can perform sophisticated analysis using standard graph algorithms. For the Seven Bridges problem, we want to determine if the graph has an Eulerian trail: A path that visits every edge exactly once but doesn’t necessarily return to the start.

Let’s assume our trail would start and end at the same node. Is there some property that must hold for each node? As we know, a bridge can only be crossed once, so we can conclude that whenever we visit a piece of land via a bridge we must leave it via a different bridge again. That means that the number of bridges connected to each land must be 2, or 4, or 6, or 2000, … in other words, an even number.

However, our trail does not have to start and end at the same piece of land. If this is the case, the start and end nodes can have an odd number of bridges connected to them. This is because we never enter the start node, and we never leave the end node.

This is what Euler formalized in his theorem: An undirected graph has an Eulerian trail if and only if it is connected and has exactly zero or two vertices of odd degree.

Degree of a node

For simplicity we’ll assume that our graphs are always connected. The degree of a node is the number of edges connected to it. Since our graph is undirected, we can obtain the degree of a node by counting the number of outgoing edges:

nodeDegree :: StateGraph -> StateNode -> Int
nodeDegree graph node = Set.size (Graph.getOutgoingEdges node graph)

^{🗎 test/Examples/Common.purs L21-L22}

And we can easily see that all of our nodes have odd degree:

specNodeDegree :: Spec Unit
specNodeDegree = do
  it "should each node have the expected degree" do
    nodeDegree bridgesGraph "A" `shouldEqual` 5
    nodeDegree bridgesGraph "B" `shouldEqual` 3
    nodeDegree bridgesGraph "C" `shouldEqual` 3
    nodeDegree bridgesGraph "D" `shouldEqual` 3

^{🗎 test/Examples/BridgesKoenigsberg.purs L100-L106}

And this already shows that our graph does not have an Eulerian trail.

Checking for Eulerian trail

But we want to create a function that can tell this for any state graph. Let’s do that now, we’ll use this function in the next example again:

hasEulerTrail :: StateGraph -> Boolean
hasEulerTrail graph =
  let
    nodes :: Array StateNode
    nodes = fromFoldable (Graph.getNodes graph)

    countEdgesByNode :: Array Int
    countEdgesByNode = map (nodeDegree graph) nodes

    sumOddEdges :: Int
    sumOddEdges = Array.length (Array.filter Int.odd countEdgesByNode)
  in
    sumOddEdges == 2 || sumOddEdges == 0

^{🗎 test/Examples/Common.purs L24-L36}

The implementation is pretty straightforward. We get all nodes, count the number of edges connected to each node, filter the odd ones and count them. If the count is 2 or 0, we have an Eulerian trail, otherwise we don’t. We can use this function to test our graph:

specEulerTrail :: Spec Unit
specEulerTrail = do
  it "should not have an Eulerian trail" do
    hasEulerTrail bridgesGraph `shouldEqual` false

^{🗎 test/Examples/BridgesKoenigsberg.purs L108-L111}

Graph analysis with the classic state machine approach

If we wanted to perform similar analysis with the classic state machine approach, we would need to generate all possible 5040 walks and empirically check if any of them visit all bridges exactly once. This is due to the fact that the specification of state machine transitions is buried inside the update function.