Improve deployment installation (#9)

Signed-off-by: Marco Lampacrescia <[email protected]>

.github/workflows/build_executable.yml

@@ -86,6 +86,19 @@ jobs:
                     cd deployment
                     cat << EOF > install.sh
                     #!/bin/bash
+                    # Check if --install-dependencies is set
+                    if [[ "\$1" == "--install-dependencies" ]]; then
+                      # Check if we need to prepend sudo
+                      if [[ \$(id -u) -ne 0 ]]; then
+                        SUDO=sudo DEBIAN_FRONTEND=noninteractive
+                      else
+                        # Required only when running in docker, as root
+                        export DEBIAN_FRONTEND=noninteractive
+                      fi
+                      # Install the dependencies
+                      \$SUDO apt update
+                      \$SUDO apt install -y --no-install-recommends chrpath libboost-all-dev libcln-dev libgmp-dev libginac-dev libglpk-dev libhwloc-dev libz3-dev libxerces-c-dev libeigen3-dev libgtest-dev
+                    fi
                     SOURCE=\$( cd -- "\$( dirname -- "\${BASH_SOURCE[0]}" )" &> /dev/null && pwd )
                     chrpath -r \$SOURCE/3rd_party \$SOURCE/3rd_party/libspot.so.0
                     chrpath -r \$SOURCE/3rd_party \$SOURCE/3rd_party/libstorm.so

README.md

@@ -3,7 +3,22 @@ A Statistical Model Checker implementation building on top of STORM
 
 ## Installation
 
-### Get the Official Storm installed
+### Using deployed binaries
+
+We provide pre-built binaries that can be used on Ubuntu. They can be found at the [Releases page](https://github.com/convince-project/smc_storm/releases).
+
+To install them on your machine, extract `smc_storm_executable.tar.gz` and follow these steps:
+
+```bash
+cd smc_storm_executable            # This is the extracted archive
+install.sh --install-dependencies  # This flag will install all  packages required by smc_storm and its dependencies
+export PATH=$PATH:$PWD/bin         # This way, smc_storm can be called from anywhere
+smc_storm --help                   # Make sure the binary runs
+```
+
+### Compile from source
+
+#### Get the Official Storm installed
 This package needs Storm to be built on your local machine. To achieve that, follow the [official documentation](https://www.stormchecker.org/documentation/obtain-storm/build.html).
 
 We used the following command to build storm:
@@ -14,7 +29,7 @@ cmake -DSTORM_USE_SPOT_SHIPPED=ON $STORM_DIR && make -j10
 
 We recommend to use the `master` branch, since it provides the latest features as the trigonometric operators.
 
-### Build this module
+#### Build this module
 After cloning this repository, execute the following commands:
 ```bash
 mkdir build && cd build

docs/source/installation.rst

@@ -4,8 +4,25 @@ Installation Guide
 How to install smc_storm
 ------------------------
 
+Use deployed binaries
++++++++++++++++++++++
+
+We provide pre-built binaries that can be used on Ubuntu. They can be found at the `Releases page <https://github.com/convince-project/smc_storm/releases>`_.
+
+To install them on your machine, extract `smc_storm_executable.tar.gz` and follow these steps:
+
+.. code-block:: bash
+
+    cd smc_storm_executable            # This is the extracted archive
+    install.sh --install-dependencies  # This flag will install all  packages required by smc_storm and its dependencies
+    export PATH=$PATH:$PWD/bin         # This way, smc_storm can be called from anywhere
+    smc_storm --help                   # Make sure the binary runs
+
+Build from source
++++++++++++++++++
+
 Install STORM
-+++++++++++++
+_____________
 
 smc_storm needs STORM to be built on the local machine. To achieve that, follow the `official documentation <https://www.stormchecker.org/documentation/obtain-storm/build.html>`_.
 
@@ -19,7 +36,7 @@ We used the following command to build STORM:
     cmake -DSTORM_USE_SPOT_SHIPPED=ON $STORM_DIR && make -j10
 
 Install smc_storm
-+++++++++++++++++
+_________________
 
 Once STORM is installed, smc_storm can be built using the following:
 
@@ -30,21 +47,26 @@ Once STORM is installed, smc_storm can be built using the following:
     cd build
     cmake .. -DCMAKE_BUILD_TYPE=Release && make -j4
 
-Make it available from anywhere
-+++++++++++++++++++++++++++++++
+Make smc_storm available from anywhere
+++++++++++++++++++++++++++++++++++++++
 
 In order to be able to call smc_storm from anywhere in bash, you can add the smc_storm path to the PATH env variable:
 
 .. code-block:: bash
 
-    export PATH=$PATH:$HOME/storm_ws/smc_storm/build/bin
+    export PATH=$PATH:<path-to-smc-storm-repo-bin>
+
+The path will depend on the used installation strategy:
+* If you used the pre-built binaries, the path will be `<path-to-workspace>/smc_storm_executable/bin`
+* If you built from source, the path will be `<path-to-workspace>/smc_storm/build/bin`
 
+The `<path-to-workspace>` is the directory where you extracted the pre-built binaries or where you cloned the smc_storm repository.
 
-Verify everything is working
-----------------------------
+Verify the installation works
+-----------------------------
 
-To verify that everything is working, you can run the following test from the build folder:
+To verify that the binaries are able to execute, you can try to run it and check the execution terminates correctly:
 
 .. code-block:: bash
 
-    ./test_models
+    smc_storm --help

docs/source/tutorials.rst

@@ -14,7 +14,7 @@ Retrieve the available options
 Examples
 ++++++++
 
-Here some examples are provided, to show how to run smc_storm on the exemplary models provided in the `test/test_files` folder:
+Here some examples are provided, to show how to run smc_storm on the exemplary models provided in the `test_files folder <https://github.com/convince-project/smc_storm/tree/main/test/test_files>`_:
 
 .. code-block:: bash