Commit 98fa16f4 authored by Michaela Klauck's avatar Michaela Klauck

more readme content

parent 8330aa50
Additional material for the MMB2020 paper "A Modest Race for Deep Statistical Model Checking":
- racetrack models (in ASCII format, Jani-Files can be generated using the generator)
- generator/scripts to generate Jani representations of the racetrack models
- the version of The Modest Toolset with the Oracle option to resolve nondeterminism in modes used in the paper
\ No newline at end of file
- generator/scripts to generate Jani representations of the racetrack models:
* see readme for the gernerator: generator.py path/to/ASCIImap.track --out path/to/janiOutput.jani --prob 0.9 --collision dead --noise nochange --start-point allnonwalls --individual-jani-for-each-start-point
to generate the noisy version for all possible start states on the map, you can also list individual start points 00:05, 04:95, nondeterminism is resolved by a handwritten controller policy when using -d. Then only a single jani file for one start point can be generated at a time.
- the version of The Modest Toolset with the Oracle option to resolve nondeterminism in modes used in the paper
* statistical model checker modes: ./modes path/to/map.jani -R Oracle --cycle-bound 0 --props "goal_prob" --Map path/to/ASCIImap.track -NN path/to/NN/files
* mcsta
\ No newline at end of file
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment