small fix

Author: nickgian

_posts/2020-06-18-models-of-distributed-protocols.md

@@ -42,7 +42,7 @@ The routing process for SIMPLE, and other protocols we model, operates by transm
 
 Informally, SIMPLE operates as follows.  Each router with a valid route can choose to export the route to one or more of its neighbors.  When a message traverses an edge in the graph, it is transformed. The length of the route will increase by one, the next hop field will change, and the importer will change the preference field, making the route more or less desirable.   We call the function that executes those transformations the *trans* function.  Since the transformation may vary from one edge of the graph to the next, when we care to be specific, we write $\mathbf{\mathtt{trans}}_{\mathtt{e}}$ for the transformation function to be applied across the edge e.
 
-When a router receives one or more routes from its neighbors, it compares those routes with its initial route and chooses the most desirable route available.  More specifically, it prefers the route with the highest preference value.  If there is a tie, it will prefer the route with the shortest path length.  If there is still a tie, it prefers the route through the lowest numbered neighbor (e.g., all other things being equal, router $\mathtt{R_3}$ prefers routes it receives from $\mathtt{R_1}$ over those it receives from $\mathtt{R_2}$).  In general, when multiple routes are available at a router, the router will use information from those routes to compute its most desired route.  We call the function that executes that computation the _**merge**_ function, and often write $\mathtt{R_1~+~R_2}$ to denote the merge of two routes, r1 and r2.  In principle, the merge function can differ at every router.  If we care to distinguish between the merge functions of particular routers, we will write _**merge$_R$**_, or $\mathtt{R_1}~\mathtt{+_R}~\mathtt{R_2}$, for the merge at router R, but to keep the notation light, we will often assume the merge functions are the same across all nodes and elide the subscript.
+When a router receives one or more routes from its neighbors, it compares those routes with its initial route and chooses the most desirable route available.  More specifically, it prefers the route with the highest preference value.  If there is a tie, it will prefer the route with the shortest path length.  If there is still a tie, it prefers the route through the lowest numbered neighbor (e.g., all other things being equal, router $\mathtt{R_3}$ prefers routes it receives from $\mathtt{R_1}$ over those it receives from $\mathtt{R_2}$).  In general, when multiple routes are available at a router, the router will use information from those routes to compute its most desired route.  We call the function that executes that computation the _**merge**_ function, and often write $\mathtt{R_1~+~R_2}$ to denote the merge of two routes, $\mathtt{r_1}$ and $\mathtt{r_2}$.  In principle, the merge function can differ at every router.  If we care to distinguish between the merge functions of particular routers, we will write _**merge$_R$**_, or $\mathtt{R_1}~\mathtt{+_R}~\mathtt{R_2}$, for the merge at router R, but to keep the notation light, we will often assume the merge functions are the same across all nodes and elide the subscript.
 
 Choices such as which router forwards routes to which other routers, and how to change a field like the preference value are typically part of the configuration of a protocol.  In contrast, the notion of "most desirable route" (i.e., the _**merge**_ function) is usually a fixed part of the protocol.  The configurations are typically defined by network operators---they are what allows a protocol to be customized to the needs of a particular network.  Router vendors like Cisco and Juniper have complex, proprietary languages for configuring their devices, and in large networks, such configurations can be hundreds or thousands of lines of code per router, and hundreds of thousands or millions of lines in total for a large data center network.  However, when it comes to network verification, it does not really matter whether a route processing function is defined by a configuration or is an inherent, unchangeable part of the protocol.  Hence, our models incorporate both and do not distinguish between fixed and configurable parts.