You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
 
 
 
Anna Glaser 1eef647194 fixed original prob plotting, grouping sum of differences, fixed changed hit label 2 years ago
data fixed original prob plotting, grouping sum of differences, fixed changed hit label 2 years ago
inputs fixed original prob plotting, grouping sum of differences, fixed changed hit label 2 years ago
models fixed original prob plotting, grouping sum of differences, fixed changed hit label 2 years ago
src fixed original prob plotting, grouping sum of differences, fixed changed hit label 2 years ago
writeups added explanation for car_strategy_2 2 years ago
.gitignore added local configuration for prismmodelchecker into gitignore 2 years ago
README.md Clean refactor 2 years ago
config.yml added local configuration for prismmodelchecker into gitignore 2 years ago
environment.yml car evil strategy works... may not be super evil 2 years ago

README.md

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.