update installation script and instructions

.github/workflows/buildtest.yml

@@ -31,19 +31,19 @@ jobs:
     steps:
       - name: Git clone
         uses: actions/checkout@v4
-      - name: Build stormpy from Dockerfile
+      - name: Build paynt image from Dockerfile
         run: docker build -t ${{ matrix.buildType.imageName }}:${{ matrix.buildType.dockerTag }} . --build-arg setup_args=${{ matrix.buildType.setupArgs }} --build-arg setup_args_pycarl=${{ matrix.buildType.setupArgs }} --build-arg no_threads=${NR_JOBS}
-      - name: Build image for learner
+      - name: Build paynt image with learner dependencies
         run: docker build -t ${{ matrix.buildType.imageName }}-learner:${{ matrix.buildType.dockerTag }} . -f paynt-learner.dockerfile --build-arg paynt_base=${{ matrix.buildType.imageName }}:${{ matrix.buildType.dockerTag }}
       - name: Login into docker
         # Only login if using master on original repo (and not for pull requests or forks)
         if: github.repository_owner == 'randriu' && github.ref == 'refs/heads/master'
         run: echo '${{ secrets.STORMPY_CI_DOCKER_PASSWORD }}' | docker login -u randriu --password-stdin
-      - name: Deploy paynt
+      - name: Deploy paynt image
         # Only deploy if using master on original repo (and not for pull requests or forks)
         if: github.repository_owner == 'randriu' && github.ref == 'refs/heads/master'
         run: docker push ${{ matrix.buildType.imageName }}:${{ matrix.buildType.dockerTag }}
-      - name: Deploy paynt with learner dependencies
+      - name: Deploy paynt image with learner dependencies
         # Only deploy if using master on original repo (and not for pull requests or forks)
         if: github.repository_owner == 'randriu' && github.ref == 'refs/heads/master'
         run: docker push ${{ matrix.buildType.imageName }}-learner:${{ matrix.buildType.dockerTag }}

.gitignore

@@ -1,2 +1,4 @@
 __pycache__/
+*.egg-info/
+
 prerequisites/

Dockerfile

@@ -12,14 +12,15 @@ RUN apt-get update -qq
 RUN apt-get install -y graphviz
 RUN pip install click z3-solver graphviz
 
-# build payntbind
+# build paynt
 WORKDIR /opt/paynt
 COPY . .
 WORKDIR /opt/paynt/payntbind
 RUN python setup.py build_ext $setup_args -j $no_threads develop
 
-# install paynt
 WORKDIR /opt/paynt
+
+# (optional) install paynt
 RUN pip install -e .
 
 # TODO tests

README.md

@@ -1,6 +1,6 @@
 # PAYNT
 
-PAYNT (Probabilistic progrAm sYNThesizer) is a tool for the automated synthesis of probabilistic programs. PAYNT takes a program with holes (a so-called sketch) and a PCTL specification, and outputs a concrete hole assignment that yields a satisfying program, if such an assignment exists. PAYNT also supports the synthesis of finite-state controllers for POMDPs. Internally, PAYNT interprets the incomplete probabilistic program as a family of Markov chains and uses state-of-the-art synthesis methods on top of the model checker [Storm](https://github.com/moves-rwth/storm) to identify satisfying realization. PAYNT is implemented in Python and uses [Stormpy](https://github.com/randriu/stormpy/tree/synthesis), Python bindings for Storm. PAYNT is hosted on [github](https://github.com/randriu/synthesis).
+PAYNT (Probabilistic progrAm sYNThesizer) is a tool for the automated synthesis of probabilistic programs. PAYNT takes a program with holes (a so-called sketch) and a PCTL specification, and outputs a concrete hole assignment that yields a satisfying program, if such an assignment exists. PAYNT also supports the synthesis of finite-state controllers for POMDPs. Internally, PAYNT interprets the incomplete probabilistic program as a family of Markov chains and uses state-of-the-art synthesis methods on top of the model checker [Storm](https://github.com/moves-rwth/storm) to identify satisfying realization. PAYNT is implemented in Python and uses [Stormpy](https://github.com/moves-rwth/stormpy), Python bindings for Storm. PAYNT is hosted on [github](https://github.com/randriu/synthesis).
 
 PAYNT is described in 
 - [1] PAYNT: A Tool for Inductive Synthesis of Probabilistic Programs by Roman Andriushchenko, Milan Ceska, Sebastian Junges, Joost-Pieter Katoen and Simon Stupinsky
@@ -15,32 +15,49 @@ Most of the algorithms are described in
 
 ## Installation
 
-PAYNT requires [Storm](https://github.com/moves-rwth/storm) and the [synthesis fork of Stormpy](https://github.com/randriu/stormpy/tree/synthesis).
-Upon installing Stormpy within a Python environment, you can activate this environment and call PAYNT, e.g.
+To download PAYNT, use
 
 ```shell
-source env/bin/activate
+git clone https://github.com/randriu/synthesis.git synthesis
+cd synthesis
+```
+
+PAYNT requires [Storm](https://github.com/moves-rwth/storm) and the [Stormpy](https://github.com/moves-rwth/stormpy), Python bindings for Storm
+If you have Stormpy installed (e.g. within a Python environment), PAYNT and its dependencies can be installed by
+
+```shell
+sudo apt install -y graphviz
+source ${VIRTUAL_ENV}/bin/activate
+pip3 install click z3-solver graphviz
+cd payntbind
+python3 setup.py develop
+cd ..
 python3 paynt.py --help
 ```
 
-If you do not have Stormpy installed, you can download this repository, navigate to the root folder and run the installation script described in `alias-paynt.sh`:
+If you do not have Stormpy installed, you can run the installation script `install.sh` to install Storm, Stormpy and other required dependencies. Complete compilation might take up to an hour. The python environment will be available in `prerequisistes/venv`:
 
 ```shell
-git clone https://github.com/randriu/synthesis.git synthesis
-cd synthesis
-source alias-paynt.sh
-synthesis-install
+./install.sh
+source prerequisistes/venv/bin/activate
+python3 paynt.py --help
 ```
 
-The script will automatically install dependencies and compile all the prerequisites necessary to run PAYNT. Complete compilation might take a couple of hours. To accelerate compilation, the install script makes use of multiple cores. Such multi-core compilation is quite memory-intensive: as a rule of thumb, we recommend allocating at least 2 GB RAM per core. For instance, for a machine with 4 CPU cores and at least 8 GB of RAM, the compilation should take around 30 minutes. Any errors you encounter during the compilation are most likely caused by the lack of memory. In such a case, you can modify variable `COMPILE_JOBS` in `alias-paynt.sh` to match your preferences; setting the variable to 1 corresponds to the single-core compilation.
+PAYNT is also available as a docker image:
+
+```shell
+docker pull randriu/paynt
+docker run --rm -it randriu/paynt
+python3 paynt.py --help
+```
 
 
 ## Running PAYNT
 
 Upon enabling the Python environment, e.g.
 
 ```shell
-source env/bin/activate
+source ${VIRTUAL_ENV}/bin/activate
 ```
 
 PAYNT can be executed using the command in the following form:
@@ -95,30 +112,6 @@ deactivate
 ```
 
 
-### Developer notes
-
-The script `alias-paynt.sh` contains useful macros for (re-)compiling Storm/Stormpy. Once loaded from the root folder:
-```shell
-source alias-paynt.sh
-```
-a number of command-line macros become available. Command `synthesis-install` showcases the basic commands in the step-by-step installation of PAYNT.
-
-In the development process, if the source code of Storm has been modified, but not its header files, it needs to be re-built (`storm-build`). If the header files were also modified, the re-configuration as well as Stormpy recompilation are necessary:
-```shell
-storm-config
-storm-build
-stormpy-build
-```
-
-If you need to frequently modify the Storm source code, it might be a good idea to develop it in the debug mode:
-```shell
-storm-config-debug
-storm-build-debug
-```
-Building in the debug mode using the commands above also disables link-time optimizations, accelerating compilation. The script uses different folders for the release (`storm/build`) and the debug (`storm/build_debug`) versions of Storm.
-
-
-
 # PAYNT tutorial
 
 For instance, here is a simple PAYNT call:

install.sh

@@ -7,21 +7,20 @@ COMPILE_JOBS=$(nproc)
 
 # environment variables
 PAYNT_ROOT=`pwd`
+PREREQUISITES=${PAYNT_ROOT}/prerequisites # modify this to install prerequisites outside of Paynt
 
-# storm-dependencies
-sudo apt update
-sudo apt -y install build-essential git automake cmake libboost-all-dev libcln-dev libgmp-dev libginac-dev libglpk-dev libhwloc-dev libz3-dev libxerces-c-dev libeigen3-dev graphviz
-sudo apt -y install maven uuid-dev python3-dev libffi-dev libssl-dev python3-pip python3-venv
-# apt -y install texlive-latex-extra
-# update-alternatives --install /usr/bin/python python /usr/bin/python3 10
+# storm and stormpy dependencies
+sudo apt update -qq
+sudo apt install -y build-essential git cmake libboost-all-dev libcln-dev libgmp-dev libginac-dev automake libglpk-dev libhwloc-dev libz3-dev libxerces-c-dev libeigen3-dev
+sudo apt install -y maven uuid-dev python3-dev python3-venv python3-pip
 
 # prerequisites
-mkdir -p ${PAYNT_ROOT}/prerequisites
+mkdir -p ${PREREQUISITES}
 
 # build cvc5 (optional)
-# cd ${PAYNT_ROOT}/prerequisites
+# cd ${PREREQUISITES}
 # git clone --depth 1 --branch cvc5-1.0.0 https://github.com/cvc5/cvc5.git cvc5
-# cd ${PAYNT_ROOT}/prerequisites/cvc5
+# cd ${PREREQUISITES}/cvc5
 # source ${PAYNT_ROOT}/env/bin/activate
 # ./configure.sh --prefix="." --auto-download --python-bindings
 # cd build
@@ -30,42 +29,43 @@ mkdir -p ${PAYNT_ROOT}/prerequisites
 # deactivate
 
 # build storm
-cd ${PAYNT_ROOT}/prerequisites
+cd ${PREREQUISITES}
 git clone https://github.com/moves-rwth/storm.git storm
 # git clone --branch stable https://github.com/moves-rwth/storm.git storm
-mkdir -p ${PAYNT_ROOT}/storm/build
-cd ${PAYNT_ROOT}/storm/build
+mkdir -p ${PREREQUISITES}/storm/build
+cd ${PREREQUISITES}/storm/build
 cmake ..
 make storm-main storm-pomdp --jobs ${COMPILE_JOBS}
 # make check --jobs ${COMPILE_JOBS}
 
-# setup python environment
-python3 -m venv ${PAYNT_ROOT}/env
-source ${PAYNT_ROOT}/env/bin/activate
-pip3 install pytest pytest-runner pytest-cov numpy scipy toml Cython scikit-build
+# setup and activate python environment
+python3 -m venv ${PREREQUISITES}/venv
+source ${PREREQUISITES}/venv/bin/activate
+pip3 install wheel
 
 # build pycarl
-cd ${PAYNT_ROOT}/prerequisites
+cd ${PREREQUISITES}
 git clone https://github.com/moves-rwth/pycarl.git pycarl
-cd ${PAYNT_ROOT}/prerequisites/pycarl
-python3 setup.py build_ext --jobs ${COMPILE_JOBS} develop
+cd ${PREREQUISITES}/pycarl
+python3 setup.py develop
 #[TEST] python3 setup.py test
 
 # build stormpy
-cd ${PAYNT_ROOT}/prerequisites
+cd ${PREREQUISITES}
 git clone https://github.com/moves-rwth/stormpy.git stormpy
 # git clone --branch stable https://github.com/moves-rwth/stormpy.git stormpy
-cd ${PAYNT_ROOT}/prerequisites/stormpy
-python3 setup.py build_ext --jobs ${COMPILE_JOBS} develop
-# python3 setup.py build_ext --storm-dir ${PAYNT_ROOT}/prerequisites/storm/build --jobs ${COMPILE_JOBS} develop
+cd ${PREREQUISITES}/stormpy
+python3 setup.py develop
 # python3 setup.py test
 
-# build paynt
-pip3 install click z3-solver graphviz
+# paynt dependencies
 sudo apt -y install graphviz
+pip3 install click z3-solver graphviz
+
+# build payntbind
 cd ${PAYNT_ROOT}/payntbind
-python3 setup.py build_ext --jobs ${COMPILE_JOBS} develop
+python3 setup.py develop
+cd ${PAYNT_ROOT}
 
 # done
-cd ${PAYNT_ROOT}
 deactivate