Material for the special issue of PROLE21 en JLAMP

This is the additional material for the reproducibility of the results of the paper Verification of ROS NavFn Planner using Maude. The following files are available:

• profile-ros-cpp.tar.xz is a minimal ROS environment capable of running the NavFn planner on the maps of the repository. In order to run the tests with launch_tests.sh, white_box, and white_box_dafny.py, the package should be extracted at src/testing.

  This packages includes different compilations of the NavFn planner: a release version for running the black-box tests, a debug version for running the white-box tests, and covclang and gcov versions to run coverage tests with Clang and Gcov, respectively. Switching between the different versions can be done with the switch_navfn.sh script.

• coverage-report.tar.xz includes the reports of the coverage testing with both Clang-llvm-cov and Gcov. They are also available here.

• astar_navfnplanner is the executable of the Dafny implementation of the NavFn planner, generated with the generate-go.sh script using a Go compiler.