VRRP: Increasing Reliability and Failover with the Virtual Router Redundance Protocol

E.5. Protocol Assertions

Ownership and Priority

For the discussions related to ownership, we introduce a unary predicate:

x is the owner of the virtual router v

and we symbolize this predicate as

O(x).

With our definitions and symbolisms for priority, primary IP address, and ownership at hand, we start our study of assertions related to the ownership within VRRP virtual routers.

A-(1)	If a VRRP router x is the owner of the virtual router v, then the priority of x in v has the value 255.
∀x (O(x) → prio(x) = 255)
A-(2)	If the priority of a VRRP router x has the priority 255 in the virtual router v, then x is the owner of v.
∀x ( prio(x) = 255 → O(x))

From A-(1) and A-(2) using the equivalence (4), we can obtain the following assertion:

A-(3) ...