NetworkVerification / nv

A Framework for Modeling and Analyzing Network Configurations
MIT License
31 stars 2 forks source link

Allow arbitrary numbers as nodes #79

Closed alberdingk-thijm closed 2 years ago

alberdingk-thijm commented 2 years ago

This PR removes the requirement that nodes be defined strictly as a sequence of non-negative integers, starting from 0 and ascending to nodes. Instead, users may now also define nodes as follows:

let nodes = (1, 2, 4, 6) (* without the "n" suffix *)
let nodes = (0n, 1n, 3n, 5n) (* with the "n" suffix *)

Additionally, edges may reference nodes not listed by let nodes = ..., and these nodes will be silently added to the network:

let nodes = ()
let edges = {
  1=2;
  2=3;
}

(It may be argued that this is a slightly dangerous addition to the language: we can discuss if an error should be thrown if an edge is defined here but not used.)

This change is particularly useful for partitioning, as it frees us from having to reindex nodes in TransformDecls. The downside is that it means some data structures for iterating over the nodes of the file become slightly more complicated: a fair bit of code has been changed to use nodes in the order returned by AdjGraph.fold_vertex and then store the nodes in a Vertex.t list, rather than just using a bare int.

Another potential benefit of this PR is that it opens up the possibility of defining nodes as having some other type than an int: for instance, nodes could be identifiers. This would be a step towards fully addressing #48 and allowing node aliases.