Structure of an NV Program

NV Programs

Programs in NV describe network configurations. A program consists of two parts: a specification of the network's topology, and a specification of the network's behavior. The files in the examples/ directory are a good reference -- beginners should first look at examples/simple.nv.

Network topology

NV Models networks as directed graphs. To specify such a graph, you must specify the number of nodes, and which edges exist. For example, the line

let nodes = 5

specifies a network with exactly 5 nodes, numbered 0 through 4. Nodes are always referred to by number.

Edges are declared with the syntax "node-node" or "node~node". Bidirectional edges may be specified using the syntax "node=node". Bidirectional edges declarations are syntactic sugar for two single edge declarations. For example, the line

let edges = { 0~1; 1=2; 2-3; }

specifies a graph with four unidirectional edges: node 0 to node 1, 1 to 2, 2 to 1, and 2 to 3.

Network behavior

The behavior of an NV network is described by three functions: init, trans, and merge. These functions manipulate values called attributes which are stored at each node.

Attributes

Each node in an NV network contains a piece of local information called an attribute. It sends this attribute to its neighbors, and updates its own attribute upon receiving a neighbor's message.

A typical example of an attribute is a routing table. Each node has one, and it sends information about its own table to each of its neighbors so that they can update their routes.

In NV, attributes may have arbitrary type, which must be specified near the beginning of the program with the line

type attribute = <type>

Init, trans, and merge

The network's behavior is specified by these three functions. They have the following types:

init : node -> attribute
trans : node -> attribute -> attribute
merge : node -> attribute -> attribute -> attribute

• The init function determines the initial state of the network. Given a node, it returns that node's starting attribute.
• The trans function describes how messages are sent to neighbors. If node n has attribute a, then each of the node's neighbors will receive a message with contents (trans n a)
• The merge function describes how nodes combine their attribute with attributes they receive from neighbors. If node n has attribute a1, and a receives a message with attribute a2, then it will update its attribute to (merge n a1 a2). If this causes its attribute to change, it will then send a message to each of its neighbors using the updated attribute.

Assertions

NB: The syntax of assertions is likely to change in the near future.

NV programs may optionally provide an assertion. An assertion is a predicate about the final state of the network -- for example, are all nodes reachable. To specify an assertion, write a function

assert : node -> attribute -> bool

For each node, assert will be called on that node and its final attribute, and any false return values will be reported.