NV Syntax

This page is meant to provide a comprehensive guide to the statements and expressions that can be written in NV. It is (obviously) not a formal grammar; its goal is to provide brief explanation about NV's syntax and capabilities. It omits definitions of the topology and the trans/merge/init functions, which can be found here. It also omits preprocessing, which can be found here.

Statements

Variable and Function declarations

Variables and functions may be declared using OCaml syntax:

   let x = e (* Assign variable x the value of the expression e *)
   let f arg1 ... argn = e (* Assign f a function value with arguments arg1 ... argn *)

Type declarations

Users may declare custom types using the keyword type, e.g.

    type bool_opt = option[bool]

All record types must be declared before being used, but otherwise type declarations are purely a convenience for the programmer.

Symbolic variables

A symbolic variable is one whose value is not specified by the user; it is free to take any value of its type (although it can only have one value in a given run of the program). Symbolic variables may be declared using the symbolic keyword, followed by a type, e.g.

symbolic foo : int

Symbolic variables may also be declared by giving a default value, whose type is inferred. The only difference is that the simulator will use the given value instead of the type's default value. For example,

symbolic bar = 12

Require clauses

To restrict the domain of symbolic variables, the user may use a require clause. These clauses are arbitrary expressions which must evaluate to true at the beginning of the program. For example,

symbolic foo
require 0 < foo && foo < 32

Expressions

NV supports OCaml-like let, if, and match statements. Note that if statements must always include an else branch, since NV does not have side effects.

Base Types

Booleans

The boolean type is bool. The two boolean values are true and false. NV supports the following operations involving booleans:

• And: b1 && b2
• Or: b1 || b2
• Not: !b1
• If: if b1 then e1 else e2. Here, e1 and e2 are arbitrary expressions with the same type.

Integers

NV has separate types for different sizes of integer (measured in bits). For example, 5-bit integers and 16-bit integers have types int5 and int16, respectively.

To support type inference, integer values must also be labeled with their size. This is done by appending 'u' to the value, followed by its size. For example, the 5-bit representation of the value 10 is written 10u5, and the 16-bit representation is 10u16. If the size annotation is left off, it is assumed to be 32 -- that is, the values 10 and 10u32 are identical.

NV supports the following integer operations. Each operator must be annotated with a size in the same way as values; also like values, omitted annotations are assumed to be size 32. Both operands must match the size of the operator.

• Addition: 10u5 +u5 11u5
• Subtraction: (Not currently implemented)
• Comparison: x <=u5 17u5, etc. Supported comparisons are <, <=, >, >=.
• Equality : 10u5 = 5u5. Note that the equality operator does NOT need a size annotation, as it works for most values (not just ints).

Nodes

NV has a separate type tnode for values which represent nodes in the network. Node values are written as integers with suffix 'n', for example, 0n or 10n.

Node values may be compared using comparison operators with the 'n' suffix: e.g. node <=n 17n. The comparison simply compares the integers that represent the nodes. However, unlike integers, nodes cannot be added together (or subtracted). As a result, the only way to create a node value is to write it as a literal. It is an error to write a literal which does not correspond to an actual node, for example, writing 10n in a network with 5 nodes.

Edges

NV has a type tedge which represents edges in the network. Edge values are written as <node>~<node>; for example, 0n~1n. The 'n' suffix may be omitted in this context, since it is unambiguous; hence it is also acceptable to simply write 0~1.

As with nodes, it is an error to write an edge literal which does not correspond to an actual edge in the network.

There is a built-in function toEdge : tnode -> tnode -> option[tedge] which, given two nodes, returns the edge corresponding to those nodes if it exists, or None otherwise.

Compound types

Options

NV supports option types, written as option[<type>], where <type> is arbitrary. As in OCaml, the possible values are Some v and None, where v is a value of type <type>.

Tuples

Tuple types in NV are written as (<type>, <type>, ..., <type>). Values are written the same way, as (v1, v2, dots, vn). The only way to extract the values of a tuple is via a match statement.

Records

Records are like tuples, except they use strings to index their values. A record type is written {lab1 : <type>, ..., labn : <type>}, and values are written the same way. Given a record expression r, the value associated with label lab can be retrieved using record projection, written r.lab. For detailed information about records, see Records.

Note that all record types must be declared before use, and that no label may be used more than once (within a type or across types).

Maps

Map is the NV term for a dictionary data structure, which associate keys with values. All maps in NV are total.

Map types

Map types are written dict[<type>, <type>]. The first type is the type of the keys, and the second is the type of the values. The syntax set[<type>] is syntactic sugar for dict[<type>, bool].

The key type of a map may not contain another map type; however, the value type can.

Due to the way we encode maps into SMT, NV does not allow arbitrary expressions to be used as keys into a map. An expression is allowable as a map key if and only if one of the following is true:

• It is a constant
• It has type tnode or tedge
• It is a symbolic variable

Hence, arbitrary expressions are only allowed to be used as keys into maps whose key type is tnode or tedge.

Map expressions

• createDict v creates a map with default value v.
• m[k] returns the value associated with key k in map m.
• m[k := e] returns a map with the key k associated with the value of e.
• {k1 |-> e1; k2 |-> e2; ...; kn |-> en; _ |-> v} is syntactic sugar for (createDict v)[k1 := e1][k2 := e2]...[kn := en], i.e. creating a map with n key-value pairs. The _ |-> v element is required, but the number of additional keys that can be given is arbitrary.
• map f m returns a map m' such that m'[k] = f m[k].
• mapIf pred f m returns a map m' such that m'[k] = if pred k then f m[k] else m[k]; that is, it applies f to only those values in the map whose key satisfies pred. Note that pred must be an actual function expression -- it cannot be, e.g., a variable.
• combine f m1 m2 returns a map m' such that m'[k] = f m1[k] m2[k].
• foldNodes f m acc may only be used on maps whose key type is tnode. It computes f n1 m[n1] (f n2 m[n2] (... (f nn m[nn] acc)))), where n1 through nn are the nodes in the network. The order of computation is arbitrary.
• foldEdges f m acc is as foldNodes, but the key type must be tedge, and the fold is over all edge values in the network.

Set expressions

These expressions are all syntactic sugar for dealing with dictionaries whose value type is bool.

• {e1, e2, ..., en} creates a set with entries e1 through en.
• s1 union s2 computes the union of sets s1 and s2.
• s1 inter s2 computes the intersection of sets s1 and s2.
• filter pred s computes the subset of s whose elements satisfy pred (i.e. the set of e in s such that pred e returns true).