To test our implementation of the B.A.T.M.A.N routing protocol, we run the program using the SPIN model checker. The results of the simulations show that at least one property among the five does not hold. During the simulation, the assertion for the fourth property fails. Recall that the fourth property specifies that there are no routing loops in the network.
Although we do not know the exact series of events that caused the SPIN model checker to catch the flag the assertion as false, we can illustrate a counter-example to show that the protocol does not guarantee loop freedom. In the figure below, consider the case where node A tries to send an Originator message to the network. Let the number on each link represent the strength of the link, where 1 is the weakest and 5 is the strongest. When the OGM has been broadcasted to B from A, B re-broadcasts it to C and A with a decremented time-to-live (TTL = 4). However, the re-broadcasted OGM from B to A is dropped due to a weak link. Then, the same OGM is re-broadcasted back and forth between B and C until TTL = 0. At each opportunity for B to broadcast to A, the send fails. This would lead to a situation where C’s best route to A is through B (its only choice), but B thinks its best route to A is through C. This is because B has only received one OGM from A, but has received multiple OGMs from C via re-broadcasting. In other words, since it is the same OGM routing through each node, the sequence number will not be incremented, and the routing loop situation will not be recognizable by the receive() function.