readme.txt

Multi-Agent Reachability Installation Guide

Branch of Repo: https://gitlab.engr.illinois.edu/sibai2/multi-drone_simulator/tree/TACAS_artifact

Dependencies:
python 3.6 or newer versions
numpy
scipy
matplotlib
glpk (native installation)
cvxopt
polytope
picos
flowstar

Step 1: Run our installation script with "sudo sh install.sh" to install pip3, glpk, numpy, scipy, matplotlib, cvxopt, polytope, picos

Step 2 (repeat every time you sign in): Set up the Python Path environment variable by running “export PYTHONPATH=$(pwd):$PYTHONPATH” without the quotes

To replicate our experiments from the paper please run commands on our example files from the root directory of our local repo.

For the DryVR fixed-wing drone experiment with symmetry run from root of the local repo: python3 src/VerificationScenario.py examples/scenarios/ThreeFixwingedDrones.json

For the DryVR fixed-wing drone experiment without symmetry run from root of the local repo: python3 src/VerificationScenario.py examples/scenarios/ThreeFixwingedDrones_nosym.json

For the above experiments, directly run the lower agent counts by adjusting the prefix, "Three" of the json file to "Two" or "One".

For the DryVR Linear3D experiment with symmetry run from root of the local repo: python3 src/VerificationScenario.py examples/scenarios/Linear3D_S.json

For the DryVR Linear3D experiment without symmetry run from root of the local repo: python3 src/VerificationScenario.py examples/scenarios/Linear3D_S_nosym.json

For the above experiments, directly run the lower agent counts by adding to the suffix of the json file to "_1agent" or "_2agent".

For the Flow* Linear3D experiment with symmetry run from root of the local repo: python3 src/VerificationScenario.py examples/scenarios/Flow_Linear3D_S.json

For the Flow* Linear3D experiment without symmetry run from root of the local repo: python3 src/VerificationScenario.py examples/scenarios/Flow_Linear3D_S_nosym.json

For the above experiments, directly run the lower agent counts by adding to the suffix of the json file to "_1agent" or "_2agent".

Note that the execution times reported in Table 1 of the paper depend on the computer we are executing the tool on, but should follow the same trend: sym better than nosym and fewer agents take less time than more agents. Moreover, all other measurements in the table should be the same for any platform used.

The computer that we used to do the testing has the following specifications:
Dell precision 5520
32 GB RAM
Intel Xeon Ubuntu 18.04
Quad core 2.4 Ghz