Given that only one of the property among the five does not hold, we also inserted violations of all properties to check the algorithm we implemented correctly identifies those violations. The violations we inserted for each property is described below,
1. Violation 1: We only remove nodes from the network when t > 20. In this way, we are simu- lating the case where packets are injected into the network but are not recovered. Therefore, the assertion that the number of packets sent into the network is the same as the number of packets coming out of the network is false.
2. Violation2: We set the variable seqNum to 0 without flagging the node[id].seqWrapAround flag. Therefore, since the sequence number is not monotonically increasing (modulo 216), the sequence number is invalid and the assertion is false.
3. Violation 3: We force the best first-hop link to be a link that does not have the maximum number of packets received among all direct links. Therefore, there exists a better first-hop for a packet to use, and therefore the assertion that the algorithm correctly routes is false.
4. Violation 4: We purposely choose a node we already visit to be the next hop node. Therefore, the next time that node is visited, the LoopCheck data structure will show that we have already visited that node, and therefore a loop exists in the routing path.
5. Violation 5: Upon receipt of an originator message that matches the address of the receiving node, we change the last bi-directional sequence number to be outside the range of LINK TIMEOUT. Therefore, the bi-directional link check will fail and the link is cast as unidirectional.
By running Batman Violation.pml with all those violations inserted, our model correctly catch them and print out each violation.
The characteristics of ad-hoc networks, such as dynamic membership, asymmetric connections, and frequent packet loss make designing a desirable routing protocol challenging. The fresh design ap- proach of the B.A.T.M.A.N. routing protocol provides a different way of routing. Despite its unique- ness, the protocol is not flawless yet and it requires greater study and more experiments. As we have shown in the previous section, among the five properties we listed, only the property that says the protocol guarantees the network is loop-free seems to be demonstrably false. It is perhaps the case that the other conditions may prove to be false as well under further stress.
As B.A.T.M.A.N. is still a work in progress, we hope study could potentially provide further improvement to the protocol design, introduce B.A.T.M.A.N. to more professionals, and welcome more studies to be conducted on the protocol.