Data for thesis "Model Checking for Trustworthy Reasoning in Autonomous Driving"

By Christopher Chandler


CHAPTER 4: REAL-TIME OBSTACLE AVOIDANCE

The folder "preliminary" contains data for preliminary results.  Structure:

preliminary
     |___Comparison 1
     |       |___baseline
     |	     |___mc
     |___Comparison 2
             |___baseline
	     |___mc

There are two comparisons between the baseline and model checking (mc).  Each "baseline" and "mc" folder
contains log data in autoctrl.txt with plan details and processing latency (model checking only). It also
contains "run.mp4" which is a video of the run - the trajectory can be extracted using optical flow in OpenCV.  
Map data for each LiDAR scan is also included, however this was not required for the analysis.  

The folder "case_study_1" contains data for the extended case study.  Structure:

case_study_1
     |___cul-de-sac
     |       |___0000
     |	     |___ ...
     |	     |___2114
     |___playground
             |___01
	     |___02
	     |___11
             |___12

There are two scenarios "cul-de-sac" and "playground".  In the cul-de-sac scenarios, there are 90 runs in total 
ranging from 0000 to 2114.  The digits in the folders containing data for each run have a specific meaning: 

- First digit is the starting position (0: centre, 1: right 2: left)
- Second digit is the method (0: baseline, 1: model checking)
- Last digit the index of the run (00 - 14)

Each run folder contains log data in autoctrl.txt which contains plan and processing latency data.  There is also 
a video of the run which is used to extract the trajectory using OpenCV. Files of form dfsXXX.dat contain data on 
the memory usage of model checking (only for model checking runs).  Finally, the file usage.txt contains data on 
process memory usage.  Map data for each LiDAR scan also collected but again was not used in the analysis. 


CHAPTER 5: GOAL-DIRECTED OBSTACLE AVOIDANCE

The folder "case_study_2" contains data for the case study in chapter 5 of the thesis. Structure:

case_study_1
     |___0000
     |___ ...
     |___2114

There are 90 runs in total ranging from 0000 to 1214.  The digits for the folders containing data for each run mean the following:

- First digit is whether the passable gap is on the left or right (0: right, 1: left)
- Second digit is the method (0: baseline, 1: no limit model checking, 2: limit model checking)
- Last digit the index of the run (00 - 14)

Each run folder contains log data in autoctrl.txt which contains plan and processing latency data.  There is also 
a video of the run which is used to extract the trajectory using OpenCV. Files of form dfsXXX.dat contain data on 
the memory usage of model checking for the TDTS and files of the form bfsXXX.dat contain data on memory usage 
of model checking for the AATS (only for model checking runs).  Finally, the file usage.txt contains data on 
process memory usage.  Map data for each LiDAR scan also collected but again was not used in the analysis. 
Finally XXXX.json contains metadata for the run, the number of collisions and whether the robot reached the goal.