Correctness Properties

This section contains the correctness properties that hold in stable states and express the specification or goal of net update: correct spanning trees. The manual proof of partial correctness is based on these properties as well as some invariants and behavioural properties which are mostly weakened versions, expressing something about the consistency of states during net update. Termination has not yet been shown, although care has been taken to avoid some obvious sources of non-terminating activity. Once net panic and net update have completed and the topology is stable, the following holds. The properties are presented at the detailed level of bridge portals, if possible preceded by an abstract description at the abstract graph level (which is slanted).
For each bus within the net:

-

All adjacent bridges have the consistent net identity and distance information.
All portals have the same prime, hops to prime and bus id value.

-

There is one outgoing bridge iff there is no prime portal on the bus.
For exactly one portal, alpha is true.

-

For the local bus tree there are only incoming and undirected edges.
Ift some portal's bus id $b$ is not unassigned, then route map[$b$] is valid for each portal.

-

For each other bus tree, either it is not in use or there is exactly one outgoing edge.
For each possible bus id $b$ not equal to any portal's bus id, either (1) route map[$b$] is clean for all portals, or (2) route map[$b$] is forward for one portal and valid for all other portals.

For each bridge within the net:

-

The portals in the bridge have consistent net identity and direction information.
Both portals have the same prime and mute value.

-

For each bus tree in use, each directed edge in the net tree corresponds to a directed edge in the bus tree.
If mute is false, for each bus id $b$, either route map[$b$] is clean for both portals or it is forward for one portal and valid for the other;

-

Each undirected edge in the net tree corresponds to an undirected edge in the bus tree.
If mute is true, for each bus id $b$, route map[$b$] is equal for both portals and it is either clean or valid;

-

The portals in the bridge have a consistent direction.
For at most one portal alpha is true and the portal's unique id is not equal to prime

-

The portals in the bridge have consistent distance information.
If mute is false, for one portal alpha is true, the portal's unique id is not equal to prime, and its hops to prime is 1 greater than its co-portal's hops to prime.

For each portal within a bridge:

-

If mute is true, alpha is true only if the portal's unique id is equal to prime

-

The prime portal has distance 0.
If the portal's unique id is equal to prime, then alpha is true and hops to prime is 0.