Installation¶

We provide a general introduction into setting up prophesy. If you want to get started as quick as possible, try our step-by-step guides (minimal and full)!

Requirements¶

For the base functionality of prophesy, we require Python3 and the latest version of pycarl (including the parser functionality). You can then run the setup.py command with the environment of your choice.

To use the different features of prophesy, we suggest that you at least have

a probabilistic model checker, e.g. storm.
an smt-checker with nonlinear real arithmetic support (QF_NRA), e.g. z3.

It is easiest to first install these or other optional dependencies, and only then install prophesy. This way, chances are that prophesy will find the tools itself.

To make the most out of prophesy, we suggest that you use stormpy, which are python bindings for the model checker storm. These allow an interactive communication with the model checker backend, which drastically improves performance of some methods.

Step-by-step guide (minimal)¶

Change directories to a suitable location:
```
$ cd <location>
```

Obtain carl

Clone the git repository from carl with branch master14, e.g.:

$ git clone https://github.com/smtrat/carl.git -b master14
$ cd carl

Prepare the build:

$ mkdir build && cd build
$ cmake .. -DUSE_CLN_NUMBERS=ON -DUSE_GINAC=ON

Build lib_carl:
```
$ make lib_carl
```
Done:
```
$ cd <location>
```

Obtain carl-parser

Clone the git repository from carl-parser with branch master14, e.g.:

$ git clone https://github.com/smtrat/carl-parser.git -b master14
$ cd carl-parser

Prepare the build:
```
$ mkdir build && cd build
$ cmake ..
```
Build the parser:
```
$ make
```
Done:
```
$ cd <location>
```

Obtain pycarl

Download the latest release:

$ git clone https://github.com/moves-rwth/pycarl
$ cd pycarl

Run setup.py, e.g.:
```
$ python setup.py develop
```
Done:
```
$ cd <location>
```

Obtain prophesy
- Download the latest release
- Run setup.py and write an initial config file:
  $ python setup.py develop --search-path PATH
  The optional argument defines a search path, where to look for the tools (modelcheckers, SMT solvers, etc.).
- Done

Step-by-step guide (full)¶

Change directories to a suitable location:
```
$ cd <location>
```