Expressing availability in NV

[alberdingk-thijm]

Suppose I want to verify that a given network has multiple redundant paths to a destination, i.e. it has a certain degree of availability. I don't care how long the paths are, and I want to be able to verify availability of an arbitrary number of paths. Checking the property would involve asking if every node has X paths in its solution. Is this expressible in NV?

My initial attempt at doing this would be to express a path as a type path = set[edge], and then store the paths in another set, i.e., type attribute = set[path]. But a set is not a valid key in NV, so this doesn't work.

In that case, I need to hold onto multiple paths at once, but I don't know how many I might get! I know that if I fixed the number of paths I was interested in, then I could write an attribute like (option[path], option[path]) and just store the best two, but I would prefer not to bound this number. However, my suspicion is that the total number of unique paths must be bounded by the topology, so perhaps there is a way to use a map of nodes or edges to store all of the paths?

[alberdingk-thijm]

I've realized there's a conceptual problem here: if we don't care about whether or not an edge is repeated in the paths, this may never converge, since we could just add arbitrarily many cycles to the solution and grow forever. So let's suppose instead that we have some bound on the lengths of the paths we can consider, or that if one path is a subset of another, then we discard the superset path.

[alberdingk-thijm]

Okay, on further reflection, I think this is subsumed by fault tolerance. Suppose I want to verify that there are X paths to d for every node. In other words, I want to verify that there are X-1 paths to d for every node if I make an arbitrary path to d unavailable. Making it unavailable would involve deleting an edge from the path so that we can't choose it again. Then I can continue until I have a subgraph where I want to verify that there is a single path to d.