README for PROPhESY
-------------------

1) In order to use the web-frontend of the tool, please first start the webservice by
double-clicking on "Prophesy Server" on the desktop and waiting for the line "Starting
webservice..." to appear. Then, you can access the frontend via the browser. To do so,
double-click on "Prophesy GUI" on the desktop. You can then use the GUI as illustrated by
the video on the website. For example, you can select precomputed rational functions by
clicking "select result" on the right-hand side of the screen and selecting any of the
models.

2) In order for you to be able to reproduce our benchmark results, we have included the core
of the verification procedure, i.e. the model checker computing the rational function, in
the virtual machine. The executable "pstorm" can be found at /home/prophesy/bin. If you
want to run any of the experiments from the paper, please open a terminal (for example
by right-clicking the desktop and selecting "Open terminal here" and then changing to the
right directory by typing

cd /home/prophesy/bin

The model checker binary (pstorm) can then be run by invoking

./pstorm [...]

To make things easy, we included a script for each of our benchmark instances that should
help reproduce our results. For example, you can check the reachability property on the brp
(128,2) instance by running

sh scripts/reach-brp128-2.sh

from the bin directory. Note that it is important to run this script from the
/home/prophesy/bin directory, since otherwise the model files and/or executable are not
found. The scripts for the other benchmark instances and properties follow a similar naming
scheme and can be run in the same fashion. If you want some more statistics, you can
manually add "-stats" as an option to the pstorm executable. This will enable more detailed
reports on the time used for model building, bisimulation and the actual model checking.