Car crash scenario generation - tester

Installation

The tool uses python and PRISM.

For python, an environment.yml file is provided, so you can create a conda environment:

  conda env create -f environment.yml

For PRISM, download the latest version compatible with your OS here:

https://www.prismmodelchecker.org/download.php

Follow the installation instructions and once installed, add the path to your installation in the config.yml file.

Structure/Usage

The src folder contains most of the relevant code of the project. In particular, the file prism_convert.py contains the class Converter, that reads parameters from the inputs folder, and generates a prism file with the model corresponding to the parameters read. You can execute it as

python prism_convert.py

The file compare_prism_files.py is a script that generates the prism file, executes it on prism and output the results.

The inputs folder contains the different json files with behaviour of the environment, pedestrian and car.

The models folder contains the prism model and properties files.

The data file contains some generated traces, as well as the runner.ipynb notebook, to make experiments.