Run DryVR Verfication¶
To run DryVR verfication, please run:
python main.py input/*/[input_file]
python main.py input/daginput/input_thermo.json
Run DryVR Control Synthesis¶
To run DryVR graph search algorithm, please run:
python rrt.py input/*/[input_file]
python rrt.py input/rrtinput/mazefinder.json
After you run the our tool, a reachtube.txt file will be generated in output folder unless the model is determined unsafe during simulation test.
To plot the reachtube, please run:
python plotter.py -x [x dimension number] -y [y dimension number list] -f [input file name] -o [output file name]
-x is the dimension number for x-axis, the default value will be 0, which is the dimension of time.
-y is dimension number lists indicates the dimension you want to draw for y-axis. For example -y [1,2]. The default value will be .
-f is the file path for reach tube file that you want to plot, the default value will be output/reachtube.txt.
-o is output file option, the default value is plotResult.png.
To get help for plotter, please run:
python plotter.py -h
Note that the dimension 0 is local time and last dimension is global time. For example, input_AEB’s inital set is [[0.0,-23.0,0.0,1.0,0.0,-15.0,0.0,1.0],[0.0,-22.8,0.0,1.0,0.0,-15.0,0.0,1.0]]. Therefore, it has 8 dimensions in total. You can choose to plot dimension from 0 to 9. Where dimension 0 is the local time and dimension 9 is global time. Dimension 1~8 is corresponding to the dimension you specify in initial set.
python plotter.py -y [1,2] -f output/reachtube.txt
More plot results can be found at the Examples and Performance Evaluation page.