## With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

No credit card required

### 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) ...

## With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

No credit card required