Test it with Our Model

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.

These three files should be type .pml : Batman_Violation Batman_Template batmain.doc

This file should be type .py: RunBatman

The there are three options to run the source codes

  1. 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

  2. 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

  3. 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.

 

Advertisements
This entry was posted in Uncategorized. Bookmark the permalink.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s