Commit fa6cd418 authored by Michaela Klauck's avatar Michaela Klauck
Browse files

add instructions how to run the tool

parent 4b8a69f5
......@@ -6,6 +6,14 @@ To download and install the tool with all dependencies for Linux please execute
To use it in Windows just download [this archive](, unzip it and execute `FretLrtdp.exe`
# How to run the tool
To call the tool on a JANI (`example.jani`) or Modest model (`example.modest`) execute the following command in the Modest Fret-pi LRTDP folder which is created during the download and install procedure:
FretLrtdp.exe example.jani
More information about usable parameters are displayed when adding the option `-help`.
# About Modest FRET-π LRTDP
Because of the results of the performance comparison between the planning algorithms usable for model checking purposes in Fast Downward and mcsta in the Modest toolset (partially presented in Klauck et al., Compiling Probabilistic Model Checking into Probabilistic Planning, ICAPS 2018), we decided to implement the planning algorithm FRET-π LRTDP in the Modest toolset.
Supports Markdown
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