We provide our example Promela source code and template here allowing others to further test the B.A.T.M.A.N. protocol.To run the SPIN model checker, please first install the appropriate software from SPIN’s official website (http://spinroot.com/spin/Man/README.html)
Next, due to upload file type, please download the following files and convert it to the correct file type.
This file should be type .py: RunBatman
The there are three options to run the source codes
- Run it with Batman.pml, our example code. Use the command
$ python RunBatman.py Batman.pml
to run the example source code which contains a network of nine nodes. The result will be written into the file Batman OUTPUT.txt
- Run it with Batman Violation.pml, our example violation code. Use the command
$ python RunBatman.py Batman Violation.pml
to run the example violation source code. This test-run includes a series of violation statements to ensure our implementation of B.A.T.M.A.N. correctly identifies them. The result will be written into the file Batman Violation OUTPUT.txt
- Run it with Batman Template.pml, our template code allowing users to specify the num- ber of nodes in the network. Use the command
$ python RunBatman.py Batman Template.pml N
to run the example code with N2 nodes in the network. The initial topology of the network is created as an N xN matrix with N 2 nodes, where N is user’s input. After the command, a new file with N 2 nodes is created and named as Batman Nodes N.pml. The result will be written into the file Batman Nodes N OUTPUT.txt
With any of the three options of running the source file, the user also has the following two options to include additional information about the network and the model in the output file.
- -r : Includes all the routing tables at the end of the simulation in the output file. Otherwise, by default, the routing tables are not included in the output file.
- -p : Turns off the assertions, which (when on) will stop the program if false, and instead will just include which properties succeeded and which did not in the output file. By default, the assertion is on.