Shortest path in weighted graph

I’d like to define the shortest path in a graph with weighted edges, so that I can later model an algorithm for finding the shortest path and check it’s correctness by comparing to the “true” result.

What would be a good way to achieve this?

Currently I have defined the graph as

sig Node {
  edges: set Edge

sig Edge {
  nodes: set Node,
  weight: Int
} {
  #nodes = 2
  weight = 0

pred edges_ok {
  all e: Edge, n: Node | n in e.nodes iff e in n.edges

pred at_most_one_edge_for_pair_of_nodes {
  // Any two edges can't have the same nodes
  all disj e1, e2: Edge | e1.nodes != e2.nodes

fact constraints {

I thought I could define the shortest path with something like:

fun getPaths(start: Node, end: Node): seq Edge {
    p: seq Edge
      // define start and end of path
      | start.edges in s.first
      and end.edges in s.last
      // edges have to be reachable from the start
      and p.elems in startNode.edges.^(nodes.edges)
      // next edge is reachable from the current edge
      and all i,j: Int | j = i + 1 implies path[j] in path[i].nodes.edges

fun shortestPath(start: Node, end: Node): seq Edge {
    shortest: getPaths[start, end]
      | all other: getPaths[start, end]
      | sum shortest.elements.weight <= sum other.elements.weight

But the analyzer is giving me:

A type error has occurred:
This must be a unary set. Instead, its type is

The type error comes from the fact that, under the hood, a seq Edge is a relation of type Int -> Edge (where the Int is the index of the element in the sequence). However, a comprehension can only range over sets, not relations.

A couple of hints for your model:

First, you may get rid of egdes and specify the corresponding relation in the Node signature:

sig Node {
	succ: Int -> Node

fact "at most one edge between two nodes" { 
	all n1, n2: Node | lone n1.succ.n2 

Then, as quantification on a sequence is problematic (as it’s a relation), you may reify the sequence into a signature:

sig NodeSeq { 
	nodes: seq Node

and then define a path as a well-formed NodeSeq:

fun Path : set NodeSeq {
	{ p: NodeSeq | 
		all i: Int | let n1 = p.nodes[i], n2 = p.nodes[add[i,1]] |
			(some n1 and some n2) implies some n1.succ.n2 }

AFAICT, an issue will be that you will need all possible paths to exist (to retrieve the shortest one) and, in general, you don’t know how many such paths there will be. So you’ll need all possible NodeSeqs to exist, which must be enforced by a specific fact (a so-called “generator axiom”, cf. the Alloy book) and by an adequate (and unfortunately large) bound on NodeSeq.

Thanks a lot, that’s great feedback! Your model is cleaner and also visualizes better. I feel like I might try to do this in an unidiomatic way, is there a better way to check correctness of graph algorithms in Alloy which I’m missing?

Notice that the formalization I gave for Path will probably need to be refined, it’s an example.

I think your approach is OK to model what a shortest path is (which is not really an algorithm, BTW, rather the specification thereof).

Got it, this was intended as first step to have something to check the result of some algorithm against, good to hear that it’s not completely off. Your pointers did help me understand what’s going on, thanks again!