From 57580ffe7a154161ce8b5e087a22c0bb3cec8dd6 Mon Sep 17 00:00:00 2001 From: Roman Andriushchenko Date: Thu, 21 Dec 2023 11:59:05 +0100 Subject: [PATCH] update installation script and instructions --- .github/workflows/buildtest.yml | 8 ++--- .gitignore | 2 ++ Dockerfile | 5 +-- README.md | 63 +++++++++++++++------------------ install.sh | 54 ++++++++++++++-------------- 5 files changed, 64 insertions(+), 68 deletions(-) diff --git a/.github/workflows/buildtest.yml b/.github/workflows/buildtest.yml index ff2a229d6..3c8220da3 100644 --- a/.github/workflows/buildtest.yml +++ b/.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 }} diff --git a/.gitignore b/.gitignore index 9174f3971..1082f85b0 100644 --- a/.gitignore +++ b/.gitignore @@ -1,2 +1,4 @@ __pycache__/ +*.egg-info/ + prerequisites/ diff --git a/Dockerfile b/Dockerfile index 987cfa958..e9230365e 100644 --- a/Dockerfile +++ b/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 diff --git a/README.md b/README.md index 851544c73..4c96d9188 100644 --- a/README.md +++ b/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,24 +15,41 @@ 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 @@ -40,7 +57,7 @@ The script will automatically install dependencies and compile all the prerequis 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: diff --git a/install.sh b/install.sh index 707c83582..024da6c74 100755 --- a/install.sh +++ b/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