Symbolic Route Analysis: Handling of intermediate BGP attributes

[millstein]

The Batfish simulation of BGP routing uses a set of "intermediate" BGP attributes to control the handling of route updates that implicitly involve both a "read" and a "write". For example, Batfish models an additive community set of 40:40 as a write of (InputCommunities U 40:40). For some config formats InputCommunities should refer to the communities of the original
route, but for others it should refer to the current community set that reflects prior updates. To account for the latter semantics, Batfish inserts directives to read from and write to the intermediate attributes.

The symbolic route analysis in TransferBDD does not handle arbitrary uses of these directives. Rather, it only correctly models platforms where the directives to read from and write to intermediate attributes are used in such a way as to ensure that the current set of route attributes, reflecting all updates made so far, are always read. For example, if a particular platform's semantics requires that only some of the updates to an attribute be seen when later reading the attribute, then that situation will not be modeled properly in the symbolic route analysis.