E.3. About Our Formal Perspective

The assertions we are going to make about VRRP virtual routers are organized around certain predicates to be applied to VRRP routers.

F(r, v, t)

In this formula “F” is a predicate with three arguments: r, representing an operational VRRP router; v, referring to a virtual router; and t, indicating a time point. For example, we can symbolize the statement

r is the master of the virtual router v at time t

as

(23) M(r, v, t).

We propose the following simplification in interpreting this type of assertion: let t mean “between now and the convergence moment of the election.” Under this simplification

x is master

should be interpreted to mean

x is either master right now or will become master at the end of the next election. ...

Get VRRP: Increasing Reliability and Failover with the Virtual Router Redundance Protocol now with the O’Reilly learning platform.

O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.