From 75cfa17966e468e82400272af22d39de73ddd82a Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Thu, 9 May 2019 16:32:01 +0200
Subject: [PATCH 01/11] Fixed compile issue on Linux

---
 src/storm-dft/storage/dft/DFTIsomorphism.h | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/storm-dft/storage/dft/DFTIsomorphism.h b/src/storm-dft/storage/dft/DFTIsomorphism.h
index 24a7e4252..34287b540 100644
--- a/src/storm-dft/storage/dft/DFTIsomorphism.h
+++ b/src/storm-dft/storage/dft/DFTIsomorphism.h
@@ -309,7 +309,7 @@ namespace storage {
                 case storm::storage::DFTElementType::BE_CONST:
                 {
                     auto beConst = std::static_pointer_cast<BEConst<ValueType> const>(be);
-                    depColour[dep->id()] = std::pair<ValueType, ValueType>(dep->probability(), beConst->failed());
+                    depColour[dep->id()] = std::pair<ValueType, ValueType>(dep->probability(), beConst->failed() ? storm::utility::one<ValueType>() : storm::utility::zero<ValueType>());
                     break;
                 }
                 default:

From 2d203656744cf43335c7dfd5342d10307de8f0f3 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Thu, 9 May 2019 17:02:18 +0200
Subject: [PATCH 02/11] Travis: support for Ubuntu 19.04

---
 .travis.yml               | 258 ++++++++++++++++++++++++++++++--------
 travis/generate_travis.py |  10 +-
 2 files changed, 211 insertions(+), 57 deletions(-)

diff --git a/.travis.yml b/.travis.yml
index f8ac4ef4e..d38637977 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -40,11 +40,11 @@ jobs:
     # Stage: Build Carl
     ###
 
-    # ubuntu-18.04 - DefaultDebugTravis
+    # ubuntu-19.04 - DefaultDebugTravis
     - stage: Build Carl
       os: linux
       compiler: gcc
-      env: CONFIG=DefaultDebugTravis LINUX=ubuntu-18.04 COMPILER=gcc
+      env: CONFIG=DefaultDebugTravis LINUX=ubuntu-19.04 COMPILER=gcc
       install:
         - travis/install_linux.sh
       before_script:
@@ -53,11 +53,11 @@ jobs:
         - travis/build_carl.sh
       after_success:
         - travis/deploy_carl.sh
-    # ubuntu-18.04 - DefaultReleaseTravis
+    # ubuntu-19.04 - DefaultReleaseTravis
     - stage: Build Carl
       os: linux
       compiler: gcc
-      env: CONFIG=DefaultReleaseTravis LINUX=ubuntu-18.04 COMPILER=gcc
+      env: CONFIG=DefaultReleaseTravis LINUX=ubuntu-19.04 COMPILER=gcc
       install:
         - travis/install_linux.sh
       before_script:
@@ -71,6 +71,38 @@ jobs:
     # Stage: Build (1st run)
     ###
 
+    # ubuntu-18.04 - DefaultDebug
+    - stage: Build (1st run)
+      os: linux
+      compiler: gcc
+      env: CONFIG=DefaultDebug LINUX=ubuntu-18.04 COMPILER=gcc
+      install:
+        - rm -rf build
+        - travis/install_linux.sh
+      before_script:
+        - python -c "import fcntl; fcntl.fcntl(1, fcntl.F_SETFL, 0)" # Workaround for nonblocking mode
+      script:
+        - travis/build.sh Build1
+      before_cache:
+        - docker cp storm:/opt/storm/. .
+      after_failure:
+        - find build -iname '*err*.log' -type f -print -exec cat {} \;
+    # ubuntu-18.04 - DefaultRelease
+    - stage: Build (1st run)
+      os: linux
+      compiler: gcc
+      env: CONFIG=DefaultRelease LINUX=ubuntu-18.04 COMPILER=gcc
+      install:
+        - rm -rf build
+        - travis/install_linux.sh
+      before_script:
+        - python -c "import fcntl; fcntl.fcntl(1, fcntl.F_SETFL, 0)" # Workaround for nonblocking mode
+      script:
+        - travis/build.sh Build1
+      before_cache:
+        - docker cp storm:/opt/storm/. .
+      after_failure:
+        - find build -iname '*err*.log' -type f -print -exec cat {} \;
     # debian-9 - DefaultDebug
     - stage: Build (1st run)
       os: linux
@@ -103,11 +135,11 @@ jobs:
         - docker cp storm:/opt/storm/. .
       after_failure:
         - find build -iname '*err*.log' -type f -print -exec cat {} \;
-    # ubuntu-18.04 - DefaultDebugTravis
+    # ubuntu-18.10 - DefaultDebug
     - stage: Build (1st run)
       os: linux
       compiler: gcc
-      env: CONFIG=DefaultDebugTravis LINUX=ubuntu-18.04 COMPILER=gcc
+      env: CONFIG=DefaultDebug LINUX=ubuntu-18.10 COMPILER=gcc
       install:
         - rm -rf build
         - travis/install_linux.sh
@@ -119,11 +151,11 @@ jobs:
         - docker cp storm:/opt/storm/. .
       after_failure:
         - find build -iname '*err*.log' -type f -print -exec cat {} \;
-    # ubuntu-18.04 - DefaultReleaseTravis
+    # ubuntu-18.10 - DefaultRelease
     - stage: Build (1st run)
       os: linux
       compiler: gcc
-      env: CONFIG=DefaultReleaseTravis LINUX=ubuntu-18.04 COMPILER=gcc
+      env: CONFIG=DefaultRelease LINUX=ubuntu-18.10 COMPILER=gcc
       install:
         - rm -rf build
         - travis/install_linux.sh
@@ -135,11 +167,11 @@ jobs:
         - docker cp storm:/opt/storm/. .
       after_failure:
         - find build -iname '*err*.log' -type f -print -exec cat {} \;
-    # ubuntu-18.04 - DefaultDebug
+    # ubuntu-19.04 - DefaultDebugTravis
     - stage: Build (1st run)
       os: linux
       compiler: gcc
-      env: CONFIG=DefaultDebug LINUX=ubuntu-18.04 COMPILER=gcc
+      env: CONFIG=DefaultDebugTravis LINUX=ubuntu-19.04 COMPILER=gcc
       install:
         - rm -rf build
         - travis/install_linux.sh
@@ -151,11 +183,11 @@ jobs:
         - docker cp storm:/opt/storm/. .
       after_failure:
         - find build -iname '*err*.log' -type f -print -exec cat {} \;
-    # ubuntu-18.04 - DefaultRelease
+    # ubuntu-19.04 - DefaultReleaseTravis
     - stage: Build (1st run)
       os: linux
       compiler: gcc
-      env: CONFIG=DefaultRelease LINUX=ubuntu-18.04 COMPILER=gcc
+      env: CONFIG=DefaultReleaseTravis LINUX=ubuntu-19.04 COMPILER=gcc
       install:
         - rm -rf build
         - travis/install_linux.sh
@@ -172,6 +204,36 @@ jobs:
     # Stage: Build (2nd run)
     ###
 
+    # ubuntu-18.04 - DefaultDebug
+    - stage: Build (2nd run)
+      os: linux
+      compiler: gcc
+      env: CONFIG=DefaultDebug LINUX=ubuntu-18.04 COMPILER=gcc
+      install:
+        - travis/install_linux.sh
+      before_script:
+        - python -c "import fcntl; fcntl.fcntl(1, fcntl.F_SETFL, 0)" # Workaround for nonblocking mode
+      script:
+        - travis/build.sh Build2
+      before_cache:
+        - docker cp storm:/opt/storm/. .
+      after_failure:
+        - find build -iname '*err*.log' -type f -print -exec cat {} \;
+    # ubuntu-18.04 - DefaultRelease
+    - stage: Build (2nd run)
+      os: linux
+      compiler: gcc
+      env: CONFIG=DefaultRelease LINUX=ubuntu-18.04 COMPILER=gcc
+      install:
+        - travis/install_linux.sh
+      before_script:
+        - python -c "import fcntl; fcntl.fcntl(1, fcntl.F_SETFL, 0)" # Workaround for nonblocking mode
+      script:
+        - travis/build.sh Build2
+      before_cache:
+        - docker cp storm:/opt/storm/. .
+      after_failure:
+        - find build -iname '*err*.log' -type f -print -exec cat {} \;
     # debian-9 - DefaultDebug
     - stage: Build (2nd run)
       os: linux
@@ -202,11 +264,11 @@ jobs:
         - docker cp storm:/opt/storm/. .
       after_failure:
         - find build -iname '*err*.log' -type f -print -exec cat {} \;
-    # ubuntu-18.04 - DefaultDebugTravis
+    # ubuntu-18.10 - DefaultDebug
     - stage: Build (2nd run)
       os: linux
       compiler: gcc
-      env: CONFIG=DefaultDebugTravis LINUX=ubuntu-18.04 COMPILER=gcc
+      env: CONFIG=DefaultDebug LINUX=ubuntu-18.10 COMPILER=gcc
       install:
         - travis/install_linux.sh
       before_script:
@@ -217,11 +279,11 @@ jobs:
         - docker cp storm:/opt/storm/. .
       after_failure:
         - find build -iname '*err*.log' -type f -print -exec cat {} \;
-    # ubuntu-18.04 - DefaultReleaseTravis
+    # ubuntu-18.10 - DefaultRelease
     - stage: Build (2nd run)
       os: linux
       compiler: gcc
-      env: CONFIG=DefaultReleaseTravis LINUX=ubuntu-18.04 COMPILER=gcc
+      env: CONFIG=DefaultRelease LINUX=ubuntu-18.10 COMPILER=gcc
       install:
         - travis/install_linux.sh
       before_script:
@@ -232,11 +294,11 @@ jobs:
         - docker cp storm:/opt/storm/. .
       after_failure:
         - find build -iname '*err*.log' -type f -print -exec cat {} \;
-    # ubuntu-18.04 - DefaultDebug
+    # ubuntu-19.04 - DefaultDebugTravis
     - stage: Build (2nd run)
       os: linux
       compiler: gcc
-      env: CONFIG=DefaultDebug LINUX=ubuntu-18.04 COMPILER=gcc
+      env: CONFIG=DefaultDebugTravis LINUX=ubuntu-19.04 COMPILER=gcc
       install:
         - travis/install_linux.sh
       before_script:
@@ -247,11 +309,11 @@ jobs:
         - docker cp storm:/opt/storm/. .
       after_failure:
         - find build -iname '*err*.log' -type f -print -exec cat {} \;
-    # ubuntu-18.04 - DefaultRelease
+    # ubuntu-19.04 - DefaultReleaseTravis
     - stage: Build (2nd run)
       os: linux
       compiler: gcc
-      env: CONFIG=DefaultRelease LINUX=ubuntu-18.04 COMPILER=gcc
+      env: CONFIG=DefaultReleaseTravis LINUX=ubuntu-19.04 COMPILER=gcc
       install:
         - travis/install_linux.sh
       before_script:
@@ -267,6 +329,36 @@ jobs:
     # Stage: Build (3rd run)
     ###
 
+    # ubuntu-18.04 - DefaultDebug
+    - stage: Build (3rd run)
+      os: linux
+      compiler: gcc
+      env: CONFIG=DefaultDebug LINUX=ubuntu-18.04 COMPILER=gcc
+      install:
+        - travis/install_linux.sh
+      before_script:
+        - python -c "import fcntl; fcntl.fcntl(1, fcntl.F_SETFL, 0)" # Workaround for nonblocking mode
+      script:
+        - travis/build.sh Build3
+      before_cache:
+        - docker cp storm:/opt/storm/. .
+      after_failure:
+        - find build -iname '*err*.log' -type f -print -exec cat {} \;
+    # ubuntu-18.04 - DefaultRelease
+    - stage: Build (3rd run)
+      os: linux
+      compiler: gcc
+      env: CONFIG=DefaultRelease LINUX=ubuntu-18.04 COMPILER=gcc
+      install:
+        - travis/install_linux.sh
+      before_script:
+        - python -c "import fcntl; fcntl.fcntl(1, fcntl.F_SETFL, 0)" # Workaround for nonblocking mode
+      script:
+        - travis/build.sh Build3
+      before_cache:
+        - docker cp storm:/opt/storm/. .
+      after_failure:
+        - find build -iname '*err*.log' -type f -print -exec cat {} \;
     # debian-9 - DefaultDebug
     - stage: Build (3rd run)
       os: linux
@@ -297,11 +389,11 @@ jobs:
         - docker cp storm:/opt/storm/. .
       after_failure:
         - find build -iname '*err*.log' -type f -print -exec cat {} \;
-    # ubuntu-18.04 - DefaultDebugTravis
+    # ubuntu-18.10 - DefaultDebug
     - stage: Build (3rd run)
       os: linux
       compiler: gcc
-      env: CONFIG=DefaultDebugTravis LINUX=ubuntu-18.04 COMPILER=gcc
+      env: CONFIG=DefaultDebug LINUX=ubuntu-18.10 COMPILER=gcc
       install:
         - travis/install_linux.sh
       before_script:
@@ -312,11 +404,11 @@ jobs:
         - docker cp storm:/opt/storm/. .
       after_failure:
         - find build -iname '*err*.log' -type f -print -exec cat {} \;
-    # ubuntu-18.04 - DefaultReleaseTravis
+    # ubuntu-18.10 - DefaultRelease
     - stage: Build (3rd run)
       os: linux
       compiler: gcc
-      env: CONFIG=DefaultReleaseTravis LINUX=ubuntu-18.04 COMPILER=gcc
+      env: CONFIG=DefaultRelease LINUX=ubuntu-18.10 COMPILER=gcc
       install:
         - travis/install_linux.sh
       before_script:
@@ -327,11 +419,11 @@ jobs:
         - docker cp storm:/opt/storm/. .
       after_failure:
         - find build -iname '*err*.log' -type f -print -exec cat {} \;
-    # ubuntu-18.04 - DefaultDebug
+    # ubuntu-19.04 - DefaultDebugTravis
     - stage: Build (3rd run)
       os: linux
       compiler: gcc
-      env: CONFIG=DefaultDebug LINUX=ubuntu-18.04 COMPILER=gcc
+      env: CONFIG=DefaultDebugTravis LINUX=ubuntu-19.04 COMPILER=gcc
       install:
         - travis/install_linux.sh
       before_script:
@@ -342,11 +434,11 @@ jobs:
         - docker cp storm:/opt/storm/. .
       after_failure:
         - find build -iname '*err*.log' -type f -print -exec cat {} \;
-    # ubuntu-18.04 - DefaultRelease
+    # ubuntu-19.04 - DefaultReleaseTravis
     - stage: Build (3rd run)
       os: linux
       compiler: gcc
-      env: CONFIG=DefaultRelease LINUX=ubuntu-18.04 COMPILER=gcc
+      env: CONFIG=DefaultReleaseTravis LINUX=ubuntu-19.04 COMPILER=gcc
       install:
         - travis/install_linux.sh
       before_script:
@@ -362,6 +454,36 @@ jobs:
     # Stage: Build (4th run)
     ###
 
+    # ubuntu-18.04 - DefaultDebug
+    - stage: Build (4th run)
+      os: linux
+      compiler: gcc
+      env: CONFIG=DefaultDebug LINUX=ubuntu-18.04 COMPILER=gcc
+      install:
+        - travis/install_linux.sh
+      before_script:
+        - python -c "import fcntl; fcntl.fcntl(1, fcntl.F_SETFL, 0)" # Workaround for nonblocking mode
+      script:
+        - travis/build.sh BuildLast
+      before_cache:
+        - docker cp storm:/opt/storm/. .
+      after_failure:
+        - find build -iname '*err*.log' -type f -print -exec cat {} \;
+    # ubuntu-18.04 - DefaultRelease
+    - stage: Build (4th run)
+      os: linux
+      compiler: gcc
+      env: CONFIG=DefaultRelease LINUX=ubuntu-18.04 COMPILER=gcc
+      install:
+        - travis/install_linux.sh
+      before_script:
+        - python -c "import fcntl; fcntl.fcntl(1, fcntl.F_SETFL, 0)" # Workaround for nonblocking mode
+      script:
+        - travis/build.sh BuildLast
+      before_cache:
+        - docker cp storm:/opt/storm/. .
+      after_failure:
+        - find build -iname '*err*.log' -type f -print -exec cat {} \;
     # debian-9 - DefaultDebug
     - stage: Build (4th run)
       os: linux
@@ -392,11 +514,11 @@ jobs:
         - docker cp storm:/opt/storm/. .
       after_failure:
         - find build -iname '*err*.log' -type f -print -exec cat {} \;
-    # ubuntu-18.04 - DefaultDebugTravis
+    # ubuntu-18.10 - DefaultDebug
     - stage: Build (4th run)
       os: linux
       compiler: gcc
-      env: CONFIG=DefaultDebugTravis LINUX=ubuntu-18.04 COMPILER=gcc
+      env: CONFIG=DefaultDebug LINUX=ubuntu-18.10 COMPILER=gcc
       install:
         - travis/install_linux.sh
       before_script:
@@ -407,11 +529,11 @@ jobs:
         - docker cp storm:/opt/storm/. .
       after_failure:
         - find build -iname '*err*.log' -type f -print -exec cat {} \;
-    # ubuntu-18.04 - DefaultReleaseTravis
+    # ubuntu-18.10 - DefaultRelease
     - stage: Build (4th run)
       os: linux
       compiler: gcc
-      env: CONFIG=DefaultReleaseTravis LINUX=ubuntu-18.04 COMPILER=gcc
+      env: CONFIG=DefaultRelease LINUX=ubuntu-18.10 COMPILER=gcc
       install:
         - travis/install_linux.sh
       before_script:
@@ -422,11 +544,11 @@ jobs:
         - docker cp storm:/opt/storm/. .
       after_failure:
         - find build -iname '*err*.log' -type f -print -exec cat {} \;
-    # ubuntu-18.04 - DefaultDebug
+    # ubuntu-19.04 - DefaultDebugTravis
     - stage: Build (4th run)
       os: linux
       compiler: gcc
-      env: CONFIG=DefaultDebug LINUX=ubuntu-18.04 COMPILER=gcc
+      env: CONFIG=DefaultDebugTravis LINUX=ubuntu-19.04 COMPILER=gcc
       install:
         - travis/install_linux.sh
       before_script:
@@ -437,11 +559,11 @@ jobs:
         - docker cp storm:/opt/storm/. .
       after_failure:
         - find build -iname '*err*.log' -type f -print -exec cat {} \;
-    # ubuntu-18.04 - DefaultRelease
+    # ubuntu-19.04 - DefaultReleaseTravis
     - stage: Build (4th run)
       os: linux
       compiler: gcc
-      env: CONFIG=DefaultRelease LINUX=ubuntu-18.04 COMPILER=gcc
+      env: CONFIG=DefaultReleaseTravis LINUX=ubuntu-19.04 COMPILER=gcc
       install:
         - travis/install_linux.sh
       before_script:
@@ -457,6 +579,36 @@ jobs:
     # Stage: Test all
     ###
 
+    # ubuntu-18.04 - DefaultDebug
+    - stage: Test all
+      os: linux
+      compiler: gcc
+      env: CONFIG=DefaultDebug LINUX=ubuntu-18.04 COMPILER=gcc
+      install:
+        - travis/install_linux.sh
+      before_script:
+        - python -c "import fcntl; fcntl.fcntl(1, fcntl.F_SETFL, 0)" # Workaround for nonblocking mode
+      script:
+        - travis/build.sh TestAll
+      before_cache:
+        - docker cp storm:/opt/storm/. .
+      after_failure:
+        - find build -iname '*err*.log' -type f -print -exec cat {} \;
+    # ubuntu-18.04 - DefaultRelease
+    - stage: Test all
+      os: linux
+      compiler: gcc
+      env: CONFIG=DefaultRelease LINUX=ubuntu-18.04 COMPILER=gcc
+      install:
+        - travis/install_linux.sh
+      before_script:
+        - python -c "import fcntl; fcntl.fcntl(1, fcntl.F_SETFL, 0)" # Workaround for nonblocking mode
+      script:
+        - travis/build.sh TestAll
+      before_cache:
+        - docker cp storm:/opt/storm/. .
+      after_failure:
+        - find build -iname '*err*.log' -type f -print -exec cat {} \;
     # debian-9 - DefaultDebug
     - stage: Test all
       os: linux
@@ -487,11 +639,11 @@ jobs:
         - docker cp storm:/opt/storm/. .
       after_failure:
         - find build -iname '*err*.log' -type f -print -exec cat {} \;
-    # ubuntu-18.04 - DefaultDebugTravis
+    # ubuntu-18.10 - DefaultDebug
     - stage: Test all
       os: linux
       compiler: gcc
-      env: CONFIG=DefaultDebugTravis LINUX=ubuntu-18.04 COMPILER=gcc
+      env: CONFIG=DefaultDebug LINUX=ubuntu-18.10 COMPILER=gcc
       install:
         - travis/install_linux.sh
       before_script:
@@ -502,13 +654,11 @@ jobs:
         - docker cp storm:/opt/storm/. .
       after_failure:
         - find build -iname '*err*.log' -type f -print -exec cat {} \;
-      after_success:
-        - travis/deploy_storm.sh
-    # ubuntu-18.04 - DefaultReleaseTravis
+    # ubuntu-18.10 - DefaultRelease
     - stage: Test all
       os: linux
       compiler: gcc
-      env: CONFIG=DefaultReleaseTravis LINUX=ubuntu-18.04 COMPILER=gcc
+      env: CONFIG=DefaultRelease LINUX=ubuntu-18.10 COMPILER=gcc
       install:
         - travis/install_linux.sh
       before_script:
@@ -519,13 +669,11 @@ jobs:
         - docker cp storm:/opt/storm/. .
       after_failure:
         - find build -iname '*err*.log' -type f -print -exec cat {} \;
-      after_success:
-        - travis/deploy_storm.sh
-    # ubuntu-18.04 - DefaultDebug
+    # ubuntu-19.04 - DefaultDebugTravis
     - stage: Test all
       os: linux
       compiler: gcc
-      env: CONFIG=DefaultDebug LINUX=ubuntu-18.04 COMPILER=gcc
+      env: CONFIG=DefaultDebugTravis LINUX=ubuntu-19.04 COMPILER=gcc
       install:
         - travis/install_linux.sh
       before_script:
@@ -536,11 +684,13 @@ jobs:
         - docker cp storm:/opt/storm/. .
       after_failure:
         - find build -iname '*err*.log' -type f -print -exec cat {} \;
-    # ubuntu-18.04 - DefaultRelease
+      after_success:
+        - travis/deploy_storm.sh
+    # ubuntu-19.04 - DefaultReleaseTravis
     - stage: Test all
       os: linux
       compiler: gcc
-      env: CONFIG=DefaultRelease LINUX=ubuntu-18.04 COMPILER=gcc
+      env: CONFIG=DefaultReleaseTravis LINUX=ubuntu-19.04 COMPILER=gcc
       install:
         - travis/install_linux.sh
       before_script:
@@ -551,20 +701,22 @@ jobs:
         - docker cp storm:/opt/storm/. .
       after_failure:
         - find build -iname '*err*.log' -type f -print -exec cat {} \;
+      after_success:
+        - travis/deploy_storm.sh
   allow_failures:
     - stage: Build (1st run)
       os: linux
-      env: CONFIG=DefaultReleaseTravis LINUX=ubuntu-18.04 COMPILER=gcc
+      env: CONFIG=DefaultReleaseTravis LINUX=ubuntu-19.04 COMPILER=gcc
     - stage: Build (2nd run)
       os: linux
-      env: CONFIG=DefaultReleaseTravis LINUX=ubuntu-18.04 COMPILER=gcc
+      env: CONFIG=DefaultReleaseTravis LINUX=ubuntu-19.04 COMPILER=gcc
     - stage: Build (3rd run)
       os: linux
-      env: CONFIG=DefaultReleaseTravis LINUX=ubuntu-18.04 COMPILER=gcc
+      env: CONFIG=DefaultReleaseTravis LINUX=ubuntu-19.04 COMPILER=gcc
     - stage: Build (4th run)
       os: linux
-      env: CONFIG=DefaultReleaseTravis LINUX=ubuntu-18.04 COMPILER=gcc
+      env: CONFIG=DefaultReleaseTravis LINUX=ubuntu-19.04 COMPILER=gcc
     - stage: Test all
       os: linux
-      env: CONFIG=DefaultReleaseTravis LINUX=ubuntu-18.04 COMPILER=gcc
+      env: CONFIG=DefaultReleaseTravis LINUX=ubuntu-19.04 COMPILER=gcc
 
diff --git a/travis/generate_travis.py b/travis/generate_travis.py
index 258ea6e2c..3ca733d24 100644
--- a/travis/generate_travis.py
+++ b/travis/generate_travis.py
@@ -3,12 +3,14 @@
 # Configuration for Linux
 configs_linux = [
     # OS, compiler, build type
-    ("debian-9", "gcc", "DefaultDebug"),
-    ("debian-9", "gcc", "DefaultRelease"),
-    ("ubuntu-18.04", "gcc", "DefaultDebugTravis"),
-    ("ubuntu-18.04", "gcc", "DefaultReleaseTravis"),
     ("ubuntu-18.04", "gcc", "DefaultDebug"),
     ("ubuntu-18.04", "gcc", "DefaultRelease"),
+    ("debian-9", "gcc", "DefaultDebug"),
+    ("debian-9", "gcc", "DefaultRelease"),
+    ("ubuntu-18.10", "gcc", "DefaultDebug"),
+    ("ubuntu-18.10", "gcc", "DefaultRelease"),
+    ("ubuntu-19.04", "gcc", "DefaultDebugTravis"),
+    ("ubuntu-19.04", "gcc", "DefaultReleaseTravis"),
 ]
 
 # Configurations for Mac

From 426c2930900611bb518d9b9060e235f9232a022a Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Fri, 10 May 2019 10:23:05 +0200
Subject: [PATCH 03/11] Travis: disable installation of carl-parser

---
 travis/build_carl_helper.sh | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/travis/build_carl_helper.sh b/travis/build_carl_helper.sh
index 595f0576a..49cd954e5 100755
--- a/travis/build_carl_helper.sh
+++ b/travis/build_carl_helper.sh
@@ -13,17 +13,19 @@ travis_fold() {
 run() {
   travis_fold start install_dependencies
   apt-get update
-  apt-get install -qq -y openjdk-8-jdk maven uuid-dev pkg-config
+  #apt-get install -qq -y openjdk-8-jdk maven uuid-dev pkg-config
+  apt-get install -qq -y uuid-dev pkg-config
   travis_fold end install_dependencies
 
   travis_fold start install_carl
   git clone https://github.com/smtrat/carl.git
   cd carl
-  git checkout 18.08
+  git checkout master14
   mkdir build
   cd build
   cmake .. "${CMAKE_ARGS[@]}"
-  make lib_carl addons -j$N_JOBS
+  #make lib_carl addons -j$N_JOBS
+  make lib_carl -j$N_JOBS
   travis_fold end install_carl
 }
 

From a34037bff4746eb45fde093847e03b7a7f5fbb8f Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Fri, 10 May 2019 10:04:16 +0200
Subject: [PATCH 04/11] Added utility function for rounding.

---
 src/storm/utility/constants.cpp | 17 +++++++++++++++++
 src/storm/utility/constants.h   |  3 +++
 2 files changed, 20 insertions(+)

diff --git a/src/storm/utility/constants.cpp b/src/storm/utility/constants.cpp
index b1944c267..fdaa62a51 100644
--- a/src/storm/utility/constants.cpp
+++ b/src/storm/utility/constants.cpp
@@ -256,6 +256,11 @@ namespace storm {
             return std::ceil(number);
         }
         
+        template<typename ValueType>
+        ValueType round(ValueType const& number) {
+            return std::round(number);
+        }
+        
         template<typename ValueType>
         ValueType log(ValueType const& number) {
             return std::log(number);
@@ -417,6 +422,11 @@ namespace storm {
             return carl::ceil(number);
         }
         
+        template<>
+        ClnRationalNumber round(storm::ClnRationalNumber const& number) {
+            return carl::round(number);
+        }
+        
         template<>
         ClnRationalNumber log(ClnRationalNumber const& number) {
             return carl::log(number);
@@ -610,6 +620,11 @@ namespace storm {
             return carl::ceil(number);
         }
         
+        template<>
+        GmpRationalNumber round(storm::GmpRationalNumber const& number) {
+            return carl::round(number);
+        }
+        
         template<>
         GmpRationalNumber log(GmpRationalNumber const& number) {
             return carl::log(number);
@@ -886,6 +901,7 @@ namespace storm {
         template double abs(double const& number);
         template double floor(double const& number);
         template double ceil(double const& number);
+        template double round(double const& number);
         template double log(double const& number);
         template double log10(double const& number);
         template typename NumberTraits<double>::IntegerType trunc(double const& number);
@@ -918,6 +934,7 @@ namespace storm {
         template float abs(float const& number);
         template float floor(float const& number);
         template float ceil(float const& number);
+        template float round(float const& number);
         template float log(float const& number);
         template std::string to_string(float const& value);
 
diff --git a/src/storm/utility/constants.h b/src/storm/utility/constants.h
index 80e1ef336..ddd125edb 100644
--- a/src/storm/utility/constants.h
+++ b/src/storm/utility/constants.h
@@ -155,6 +155,9 @@ namespace storm {
         template<typename ValueType>
         ValueType ceil(ValueType const& number);
 
+        template<typename ValueType>
+        ValueType round(ValueType const& number);
+
         template<typename ValueType>
         ValueType log(ValueType const& number);
 

From d201580d92fd301305c98e9abaab8fd0bf0f9643 Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Fri, 10 May 2019 10:14:20 +0200
Subject: [PATCH 05/11] Refactored simplification of
 UnaryNumericalFunctionExpression.

---
 .../UnaryNumericalFunctionExpression.cpp      | 50 +++++++++----------
 1 file changed, 24 insertions(+), 26 deletions(-)

diff --git a/src/storm/storage/expressions/UnaryNumericalFunctionExpression.cpp b/src/storm/storage/expressions/UnaryNumericalFunctionExpression.cpp
index 770c7b9f1..1b4b5d0da 100644
--- a/src/storm/storage/expressions/UnaryNumericalFunctionExpression.cpp
+++ b/src/storm/storage/expressions/UnaryNumericalFunctionExpression.cpp
@@ -40,6 +40,7 @@ namespace storm {
                 int_fast64_t result = this->getOperand()->evaluateAsInt(valuation);
                 return -result;
             } else {
+                // TODO: this should evaluate the operand as a rational.
                 double result = this->getOperand()->evaluateAsDouble(valuation);
                 switch (this->getOperatorType()) {
                     case OperatorType::Floor: return static_cast<int_fast64_t>(std::floor(result)); break;
@@ -67,39 +68,36 @@ namespace storm {
             std::shared_ptr<BaseExpression const> operandSimplified = this->getOperand()->simplify();
             
             if (operandSimplified->isLiteral()) {
-                boost::variant<int_fast64_t, storm::RationalNumber> operandEvaluation;
                 if (operandSimplified->hasIntegerType()) {
-                    operandEvaluation = operandSimplified->evaluateAsInt();
-                } else {
-                    operandEvaluation = operandSimplified->evaluateAsRational();
-                }
-                
-                bool rationalToInteger = this->getOperatorType() == OperatorType::Floor || this->getOperatorType() == OperatorType::Ceil;
-                if (operandSimplified->hasIntegerType()) {
-                    int_fast64_t value = 0;
+                    int_fast64_t value = operandSimplified->evaluateAsInt();
                     switch (this->getOperatorType()) {
-                        case OperatorType::Minus: value = -boost::get<int_fast64_t>(operandEvaluation); break;
-                        case OperatorType::Floor: value = std::floor(boost::get<int_fast64_t>(operandEvaluation)); break;
-                        case OperatorType::Ceil: value = std::ceil(boost::get<int_fast64_t>(operandEvaluation)); break;
-                    }
-                    return std::shared_ptr<BaseExpression>(new IntegerLiteralExpression(this->getManager(), value));
-                } else if (rationalToInteger) {
-                    int_fast64_t value = 0;
-                    switch (this->getOperatorType()) {
-                        case OperatorType::Floor: value = storm::utility::convertNumber<int_fast64_t>(storm::RationalNumber(carl::floor(boost::get<storm::RationalNumber>(operandEvaluation)))); break;
-                        case OperatorType::Ceil: value = storm::utility::convertNumber<int_fast64_t>(storm::RationalNumber(carl::ceil(boost::get<storm::RationalNumber>(operandEvaluation)))); break;
-                        default:
-                            STORM_LOG_ASSERT(false, "Unexpected rational to integer conversion.");
+                        case OperatorType::Minus: value = -value; break;
+                        // Nothing to be done for the other cases:
+                        // case OperatorType::Floor:
+                        // case OperatorType::Ceil:
                     }
                     return std::shared_ptr<BaseExpression>(new IntegerLiteralExpression(this->getManager(), value));
                 } else {
-                    storm::RationalNumber value = storm::utility::zero<storm::RationalNumber>();
+                    storm::RationalNumber value = operandSimplified->evaluateAsRational();
+                    bool convertToInteger = false;
                     switch (this->getOperatorType()) {
-                        case OperatorType::Minus: value = -boost::get<storm::RationalNumber>(operandEvaluation); break;
-                        case OperatorType::Floor: value = carl::floor(boost::get<storm::RationalNumber>(operandEvaluation)); break;
-                        case OperatorType::Ceil: value = carl::ceil(boost::get<storm::RationalNumber>(operandEvaluation)); break;
+                        case OperatorType::Minus:
+                            value = -value;
+                            break;
+                        case OperatorType::Floor:
+                            value = storm::utility::floor(value);
+                            convertToInteger = true;
+                            break;
+                        case OperatorType::Ceil:
+                            value = storm::utility::ceil(value);
+                            convertToInteger = true;
+                            break;
+                    }
+                    if (convertToInteger) {
+                        return std::shared_ptr<BaseExpression>(new IntegerLiteralExpression(this->getManager(), storm::utility::convertNumber<int64_t>(value)));
+                    } else {
+                        return std::shared_ptr<BaseExpression>(new RationalLiteralExpression(this->getManager(), value));
                     }
-                    return std::shared_ptr<BaseExpression>(new RationalLiteralExpression(this->getManager(), value));
                 }
             }
             

From 0e180469343579b4f5caed3d071ac5a1ef8c1eb6 Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Fri, 10 May 2019 10:48:12 +0200
Subject: [PATCH 06/11] Fixed translating ceil(x) to mathsat expressions.

---
 src/storm/adapters/MathsatExpressionAdapter.h | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/src/storm/adapters/MathsatExpressionAdapter.h b/src/storm/adapters/MathsatExpressionAdapter.h
index e99c7d0c5..88ed84dcd 100644
--- a/src/storm/adapters/MathsatExpressionAdapter.h
+++ b/src/storm/adapters/MathsatExpressionAdapter.h
@@ -257,13 +257,11 @@ namespace storm {
 				switch (expression.getOperatorType()) {
 					case storm::expressions::UnaryNumericalFunctionExpression::OperatorType::Minus:
 						return msat_make_times(env, msat_make_number(env, "-1"), childResult);
-						break;
                     case storm::expressions::UnaryNumericalFunctionExpression::OperatorType::Floor:
                         return msat_make_floor(env, childResult);
-                        break;
                     case storm::expressions::UnaryNumericalFunctionExpression::OperatorType::Ceil:
-                        return msat_make_plus(env, msat_make_floor(env, childResult), msat_make_number(env, "1"));
-                        break;
+                        // Mathsat does not support ceil... but ceil(x) = -floor(-x)  wheeii \o/
+                        return msat_make_times(env, msat_make_number(env, "-1"), msat_make_floor(env, msat_make_times(env, msat_make_number(env, "-1"), childResult)));
 					default:
                         STORM_LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Cannot evaluate expression: unknown numerical unary operator: '" << static_cast<uint_fast64_t>(expression.getOperatorType()) << "' in expression " << expression << ".");
 				}

From b70f28b10e4302641d8ddec33050230fdb4bcf93 Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Fri, 10 May 2019 10:56:07 +0200
Subject: [PATCH 07/11] Ensured that utility function for rounding always
 rounds towards infinity.

---
 src/storm/utility/constants.cpp | 15 ++++-----------
 1 file changed, 4 insertions(+), 11 deletions(-)

diff --git a/src/storm/utility/constants.cpp b/src/storm/utility/constants.cpp
index fdaa62a51..a5e1c14f5 100644
--- a/src/storm/utility/constants.cpp
+++ b/src/storm/utility/constants.cpp
@@ -258,7 +258,8 @@ namespace storm {
         
         template<typename ValueType>
         ValueType round(ValueType const& number) {
-            return std::round(number);
+            // Rounding towards infinity
+            return floor<ValueType >(number + storm::utility::convertNumber<ValueType>(0.5));
         }
         
         template<typename ValueType>
@@ -422,11 +423,6 @@ namespace storm {
             return carl::ceil(number);
         }
         
-        template<>
-        ClnRationalNumber round(storm::ClnRationalNumber const& number) {
-            return carl::round(number);
-        }
-        
         template<>
         ClnRationalNumber log(ClnRationalNumber const& number) {
             return carl::log(number);
@@ -620,11 +616,6 @@ namespace storm {
             return carl::ceil(number);
         }
         
-        template<>
-        GmpRationalNumber round(storm::GmpRationalNumber const& number) {
-            return carl::round(number);
-        }
-        
         template<>
         GmpRationalNumber log(GmpRationalNumber const& number) {
             return carl::log(number);
@@ -991,6 +982,7 @@ namespace storm {
         template storm::ClnRationalNumber maximum(std::vector<storm::ClnRationalNumber> const&);
         template storm::ClnRationalNumber max(storm::ClnRationalNumber const& first, storm::ClnRationalNumber const& second);
         template storm::ClnRationalNumber min(storm::ClnRationalNumber const& first, storm::ClnRationalNumber const& second);
+        template storm::ClnRationalNumber round(storm::ClnRationalNumber const& number);
         template std::string to_string(storm::ClnRationalNumber const& value);
 #endif
 
@@ -1015,6 +1007,7 @@ namespace storm {
         template storm::GmpRationalNumber maximum(std::vector<storm::GmpRationalNumber> const&);
         template storm::GmpRationalNumber max(storm::GmpRationalNumber const& first, storm::GmpRationalNumber const& second);
         template storm::GmpRationalNumber min(storm::GmpRationalNumber const& first, storm::GmpRationalNumber const& second);
+        template storm::GmpRationalNumber round(storm::GmpRationalNumber const& number);
         template std::string to_string(storm::GmpRationalNumber const& value);
 #endif
 

From 66a7bd595444202cf27c01fa8fca4f73bf3df878 Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Fri, 10 May 2019 13:07:41 +0200
Subject: [PATCH 08/11] implemented creation of round expression.

---
 src/storm/storage/expressions/Expression.cpp | 5 +++++
 src/storm/storage/expressions/Expression.h   | 2 ++
 2 files changed, 7 insertions(+)

diff --git a/src/storm/storage/expressions/Expression.cpp b/src/storm/storage/expressions/Expression.cpp
index f6459ba85..77d318606 100644
--- a/src/storm/storage/expressions/Expression.cpp
+++ b/src/storm/storage/expressions/Expression.cpp
@@ -414,6 +414,11 @@ namespace storm {
             STORM_LOG_THROW(first.hasNumericalType(), storm::exceptions::InvalidTypeException, "Operator 'ceil' requires numerical operand.");
             return Expression(std::shared_ptr<BaseExpression>(new UnaryNumericalFunctionExpression(first.getBaseExpression().getManager(), first.getType().floorCeil(), first.getBaseExpressionPointer(), UnaryNumericalFunctionExpression::OperatorType::Ceil)));
         }
+        
+        Expression round(Expression const& first) {
+            STORM_LOG_THROW(first.hasNumericalType(), storm::exceptions::InvalidTypeException, "Operator 'round' requires numerical operand.");
+            return floor(first + first.getManager().rational(0.5));
+        }
 
         Expression abs(Expression const& first) {
             STORM_LOG_THROW(first.hasNumericalType(), storm::exceptions::InvalidTypeException, "Abs is only defined for numerical operands");
diff --git a/src/storm/storage/expressions/Expression.h b/src/storm/storage/expressions/Expression.h
index 262e09208..e07e1cf1a 100644
--- a/src/storm/storage/expressions/Expression.h
+++ b/src/storm/storage/expressions/Expression.h
@@ -56,6 +56,7 @@ namespace storm {
             friend Expression sign(Expression const& first);
             friend Expression floor(Expression const& first);
             friend Expression ceil(Expression const& first);
+            friend Expression round(Expression const& first);
             friend Expression minimum(Expression const& first, Expression const& second);
             friend Expression maximum(Expression const& first, Expression const& second);
 
@@ -434,6 +435,7 @@ namespace storm {
         Expression sign(Expression const& first);
         Expression floor(Expression const& first);
         Expression ceil(Expression const& first);
+        Expression round(Expression const& first);
         Expression minimum(Expression const& first, Expression const& second);
         Expression maximum(Expression const& first, Expression const& second);
         Expression disjunction(std::vector<storm::expressions::Expression> const& expressions);

From a829c52a0d8df2c12d054d2a5c80a411f11f99dd Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Fri, 10 May 2019 13:08:16 +0200
Subject: [PATCH 09/11] ExpressionParser can now parse round expressions.

---
 src/storm-parsers/parser/ExpressionCreator.cpp | 11 +++++++++++
 src/storm-parsers/parser/ExpressionCreator.h   |  1 +
 src/storm-parsers/parser/ExpressionParser.cpp  | 10 +++++++++-
 src/storm-parsers/parser/ExpressionParser.h    |  1 +
 4 files changed, 22 insertions(+), 1 deletion(-)

diff --git a/src/storm-parsers/parser/ExpressionCreator.cpp b/src/storm-parsers/parser/ExpressionCreator.cpp
index 682342e29..f9a8ad0c2 100644
--- a/src/storm-parsers/parser/ExpressionCreator.cpp
+++ b/src/storm-parsers/parser/ExpressionCreator.cpp
@@ -220,6 +220,17 @@ namespace storm {
             return manager.boolean(false);
         }
         
+        storm::expressions::Expression ExpressionCreator::createRoundExpression(storm::expressions::Expression const& e1, bool& pass) const {
+            if (this->createExpressions) {
+                try {
+                    return storm::expressions::round(e1);
+                } catch (storm::exceptions::InvalidTypeException const& e) {
+                    pass = false;
+                }
+            }
+            return manager.boolean(false);
+        }
+        
         storm::expressions::Expression ExpressionCreator::getIdentifierExpression(std::string const& identifier, bool& pass) const {
             if (this->createExpressions) {
                 STORM_LOG_THROW(this->identifiers != nullptr, storm::exceptions::WrongFormatException, "Unable to substitute identifier expressions without given mapping.");
diff --git a/src/storm-parsers/parser/ExpressionCreator.h b/src/storm-parsers/parser/ExpressionCreator.h
index 4c137325b..fb034c95e 100644
--- a/src/storm-parsers/parser/ExpressionCreator.h
+++ b/src/storm-parsers/parser/ExpressionCreator.h
@@ -70,6 +70,7 @@ namespace storm {
             storm::expressions::Expression createBooleanLiteralExpression(bool value, bool& pass) const;
             storm::expressions::Expression createMinimumMaximumExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const;
             storm::expressions::Expression createFloorCeilExpression(storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e1, bool& pass) const;
+            storm::expressions::Expression createRoundExpression(storm::expressions::Expression const& e1, bool& pass) const;
             storm::expressions::Expression getIdentifierExpression(std::string const& identifier, bool& pass) const;
             
             
diff --git a/src/storm-parsers/parser/ExpressionParser.cpp b/src/storm-parsers/parser/ExpressionParser.cpp
index deaaa93bc..0596b1b4e 100644
--- a/src/storm-parsers/parser/ExpressionParser.cpp
+++ b/src/storm-parsers/parser/ExpressionParser.cpp
@@ -50,6 +50,13 @@ namespace storm {
             }
             floorCeilExpression.name("floor/ceil expression");
             
+            if (allowBacktracking) {
+                roundExpression = ((qi::lit("round") >> qi::lit("(")) >> expression >> qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionCreator::createRoundExpression, phoenix::ref(*expressionCreator), qi::_1, qi::_pass)];
+            } else {
+                roundExpression = ((qi::lit("round") >> qi::lit("(")) > expression > qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionCreator::createRoundExpression, phoenix::ref(*expressionCreator), qi::_1, qi::_pass)];
+            }
+            roundExpression.name("round expression");
+            
             if (allowBacktracking) {
                 minMaxExpression = ((minMaxOperator_[qi::_a = qi::_1] >> qi::lit("(")) >> expression[qi::_val = qi::_1] >> +(qi::lit(",") >> expression)[qi::_val = phoenix::bind(&ExpressionCreator::createMinimumMaximumExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_a, qi::_1, qi::_pass)]) >> qi::lit(")");
             } else {
@@ -75,7 +82,7 @@ namespace storm {
                 | qi::int_[qi::_val = phoenix::bind(&ExpressionCreator::createIntegerLiteralExpression, phoenix::ref(*expressionCreator), qi::_1, qi::_pass)];
             literalExpression.name("literal expression");
             
-            atomicExpression = floorCeilExpression | prefixPowerModuloExpression | minMaxExpression | (qi::lit("(") >> expression >> qi::lit(")")) | identifierExpression | literalExpression;
+            atomicExpression = floorCeilExpression | roundExpression | prefixPowerModuloExpression | minMaxExpression | (qi::lit("(") >> expression >> qi::lit(")")) | identifierExpression | literalExpression;
             atomicExpression.name("atomic expression");
             
             unaryExpression = (-unaryOperator_ >> atomicExpression)[qi::_val = phoenix::bind(&ExpressionCreator::createUnaryExpression, phoenix::ref(*expressionCreator), qi::_1, qi::_2, qi::_pass)];
@@ -173,6 +180,7 @@ namespace storm {
                 qi::on_error<qi::fail>(identifierExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
                 qi::on_error<qi::fail>(minMaxExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
                 qi::on_error<qi::fail>(floorCeilExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+                qi::on_error<qi::fail>(roundExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
             }
         }
         
diff --git a/src/storm-parsers/parser/ExpressionParser.h b/src/storm-parsers/parser/ExpressionParser.h
index 4bd3cfaab..7a4b91a39 100644
--- a/src/storm-parsers/parser/ExpressionParser.h
+++ b/src/storm-parsers/parser/ExpressionParser.h
@@ -232,6 +232,7 @@ namespace storm {
             qi::rule<Iterator, storm::expressions::Expression(), Skipper> identifierExpression;
             qi::rule<Iterator, storm::expressions::Expression(), qi::locals<storm::expressions::OperatorType>, Skipper> minMaxExpression;
             qi::rule<Iterator, storm::expressions::Expression(), qi::locals<storm::expressions::OperatorType>, Skipper> floorCeilExpression;
+            qi::rule<Iterator, storm::expressions::Expression(), Skipper> roundExpression;
             qi::rule<Iterator, std::string(), Skipper> identifier;
             
             // Parser that is used to recognize doubles only (as opposed to Spirit's double_ parser).

From b4f652bbc8ffbb650d7ea307add7137b22a2ff53 Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Fri, 10 May 2019 14:13:03 +0200
Subject: [PATCH 10/11] Reducing the nesting when creating a
 expression::sum(...).

---
 .../SparseCbAchievabilityQuery.cpp            | 10 ++--
 .../helper/rewardbounded/CostLimitClosure.cpp |  1 -
 src/storm/storage/expressions/Expression.cpp  | 48 +++++++++++++++++--
 src/storm/storage/expressions/Expression.h    |  1 +
 src/storm/utility/ExpressionHelper.cpp        | 28 -----------
 src/storm/utility/ExpressionHelper.h          | 28 -----------
 6 files changed, 51 insertions(+), 65 deletions(-)
 delete mode 100644 src/storm/utility/ExpressionHelper.cpp
 delete mode 100644 src/storm/utility/ExpressionHelper.h

diff --git a/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.cpp b/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.cpp
index 5a65bd502..475bab05a 100644
--- a/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.cpp
+++ b/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.cpp
@@ -9,7 +9,6 @@
 #include "storm/utility/vector.h"
 #include "storm/utility/solver.h"
 #include "storm/utility/Stopwatch.h"
-#include "storm/utility/ExpressionHelper.h"
 #include "storm/settings/SettingsManager.h"
 #include "storm/settings/modules/GeneralSettings.h"
 #include "storm/settings/modules/CoreSettings.h"
@@ -82,7 +81,7 @@ namespace storm {
                 uint_fast64_t numStates = this->preprocessedModel->getNumberOfStates();
                 uint_fast64_t numChoices = this->preprocessedModel->getNumberOfChoices();
                 uint_fast64_t numBottomStates = this->reward0EStates.getNumberOfSetBits();
-                
+                STORM_LOG_THROW(numBottomStates > 0, storm::exceptions::UnexpectedException, "No bottom states in the preprocessed model.");
                 storm::expressions::Expression zero = this->expressionManager->rational(storm::utility::zero<ValueType>());
                 storm::expressions::Expression one = this->expressionManager->rational(storm::utility::one<ValueType>());
                 
@@ -106,7 +105,7 @@ namespace storm {
                     solver->add(var.getExpression() >= zero);
                     bottomStateVarsAsExpression.push_back(var.getExpression());
                 }
-                auto bottomStateSum = storm::utility::ExpressionHelper(this->expressionManager).sum(std::move(bottomStateVarsAsExpression));
+                auto bottomStateSum = storm::expressions::sum(bottomStateVarsAsExpression).simplify();
                 solver->add(bottomStateSum == one);
                 
                 // assert that the "incoming" value of each state equals the "outgoing" value
@@ -149,7 +148,10 @@ namespace storm {
                             objectiveValues.push_back(this->expressionManager->rational(rewards[choice]) * expectedChoiceVariables[choice].getExpression());
                         }
                     }
-                    auto objValue = storm::utility::ExpressionHelper(this->expressionManager).sum(std::move(objectiveValues));
+                    if (objectiveValues.empty()) {
+                        objectiveValues.push_back(this->expressionManager->rational(storm::utility::zero<storm::RationalNumber>()));
+                    }
+                    auto objValue = storm::expressions::sum(objectiveValues).simplify();
                     
                     // We need to actually evaluate the threshold as rational number. Otherwise a threshold like '<=16/9' might be considered as 1 due to integer division
                     storm::expressions::Expression threshold = this->expressionManager->rational(obj.formula->getThreshold().evaluateAsRational());
diff --git a/src/storm/modelchecker/prctl/helper/rewardbounded/CostLimitClosure.cpp b/src/storm/modelchecker/prctl/helper/rewardbounded/CostLimitClosure.cpp
index 657703b93..2471093d7 100644
--- a/src/storm/modelchecker/prctl/helper/rewardbounded/CostLimitClosure.cpp
+++ b/src/storm/modelchecker/prctl/helper/rewardbounded/CostLimitClosure.cpp
@@ -1,4 +1,3 @@
-#include <storm/utility/ExpressionHelper.h>
 #include "storm/modelchecker/prctl/helper/rewardbounded/CostLimitClosure.h"
 #include "storm/utility/macros.h"
 #include "storm/exceptions/IllegalArgumentException.h"
diff --git a/src/storm/storage/expressions/Expression.cpp b/src/storm/storage/expressions/Expression.cpp
index 77d318606..0221628db 100644
--- a/src/storm/storage/expressions/Expression.cpp
+++ b/src/storm/storage/expressions/Expression.cpp
@@ -436,19 +436,19 @@ namespace storm {
         }
 
         Expression disjunction(std::vector<storm::expressions::Expression> const& expressions) {
-            return apply(expressions, [] (Expression const& e1, Expression const& e2) { return e1 || e2; });
+            return applyAssociative(expressions, [] (Expression const& e1, Expression const& e2) { return e1 || e2; });
         }
 
         Expression conjunction(std::vector<storm::expressions::Expression> const& expressions) {
-            return apply(expressions, [] (Expression const& e1, Expression const& e2) { return e1 && e2; });
+            return applyAssociative(expressions, [] (Expression const& e1, Expression const& e2) { return e1 && e2; });
         }
         
         Expression sum(std::vector<storm::expressions::Expression> const& expressions) {
-            return apply(expressions, [] (Expression const& e1, Expression const& e2) { return e1 + e2; });
+            return applyAssociative(expressions, [] (Expression const& e1, Expression const& e2) { return e1 + e2; });
         }
         
         Expression apply(std::vector<storm::expressions::Expression> const& expressions, std::function<Expression (Expression const&, Expression const&)> const& function) {
-            STORM_LOG_THROW(!expressions.empty(), storm::exceptions::InvalidArgumentException, "Cannot build disjunction of empty expression list.");
+            STORM_LOG_THROW(!expressions.empty(), storm::exceptions::InvalidArgumentException, "Cannot build function application of empty expression list.");
             auto it = expressions.begin();
             auto ite = expressions.end();
             Expression result = *it;
@@ -460,5 +460,45 @@ namespace storm {
             
             return result;
         }
+        
+        Expression applyAssociative(std::vector<storm::expressions::Expression> const& expressions, std::function<Expression (Expression const&, Expression const&)> const& function) {
+            STORM_LOG_THROW(!expressions.empty(), storm::exceptions::InvalidArgumentException, "Cannot build function application of empty expression list.");
+            
+            // Balance the syntax tree if there are enough operands
+            if (expressions.size() >= 4) {
+                // we treat operands and literals seperately so that a subsequent call to simplify() is more successful (see, e.g., (a + 1) + (b + 1))
+                std::vector<std::vector<storm::expressions::Expression>> operandTypes(2);
+                auto& nonliterals = operandTypes[0];
+                auto& literals = operandTypes[1];
+                for (auto const& expression : expressions) {
+                    if (expression.isLiteral()) {
+                        literals.push_back(expression);
+                    } else {
+                        nonliterals.push_back(expression);
+                    }
+                }
+                
+                for (auto& operands : operandTypes) {
+                    auto opIt = operands.begin();
+                    while (operands.size() > 1) {
+                        if (opIt == operands.end() || opIt == operands.end() - 1) {
+                            opIt = operands.begin();
+                        }
+                        *opIt = function(*opIt, operands.back());
+                        operands.pop_back();
+                        ++opIt;
+                    }
+                }
+                if (nonliterals.empty()) {
+                    return literals.front();
+                } else if (literals.empty()) {
+                    return nonliterals.front();
+                } else {
+                    return function(literals.front(), nonliterals.front());
+                }
+            } else {
+                return apply(expressions, function);
+            }
+        }
     }
 }
diff --git a/src/storm/storage/expressions/Expression.h b/src/storm/storage/expressions/Expression.h
index e07e1cf1a..f8741440e 100644
--- a/src/storm/storage/expressions/Expression.h
+++ b/src/storm/storage/expressions/Expression.h
@@ -442,6 +442,7 @@ namespace storm {
         Expression conjunction(std::vector<storm::expressions::Expression> const& expressions);
         Expression sum(std::vector<storm::expressions::Expression> const& expressions);
         Expression apply(std::vector<storm::expressions::Expression> const& expressions, std::function<Expression (Expression const&, Expression const&)> const& function);
+        Expression applyAssociative(std::vector<storm::expressions::Expression> const& expressions, std::function<Expression (Expression const&, Expression const&)> const& function);
 
     }
 }
diff --git a/src/storm/utility/ExpressionHelper.cpp b/src/storm/utility/ExpressionHelper.cpp
deleted file mode 100644
index fd99855f8..000000000
--- a/src/storm/utility/ExpressionHelper.cpp
+++ /dev/null
@@ -1,28 +0,0 @@
-#include "storm/utility/ExpressionHelper.h"
-#include "storm/utility/constants.h"
-
-namespace storm {
-    namespace utility {
-        
-        ExpressionHelper::ExpressionHelper(std::shared_ptr<storm::expressions::ExpressionManager> const& expressionManager) : manager(expressionManager) {
-            // Intentionally left empty
-        }
-
-        storm::expressions::Expression ExpressionHelper::sum(std::vector<storm::expressions::Expression>&& summands) const {
-            if (summands.empty()) {
-                return manager->rational(storm::utility::zero<storm::RationalNumber>());
-            }
-            storm::expressions::Expression res = summands.front();
-            bool first = true;
-            for (auto& s : summands) {
-                if (first) {
-                    first = false;
-                } else {
-                    res = res + s;
-                }
-            }
-            return res.simplify().reduceNesting();
-        }
-        
-    }
-}
\ No newline at end of file
diff --git a/src/storm/utility/ExpressionHelper.h b/src/storm/utility/ExpressionHelper.h
deleted file mode 100644
index 6c171a286..000000000
--- a/src/storm/utility/ExpressionHelper.h
+++ /dev/null
@@ -1,28 +0,0 @@
-#pragma once
-
-#include <vector>
-#include <memory>
-#include "storm/storage/expressions/Expression.h"
-#include "storm/storage/expressions/ExpressionManager.h"
-
-namespace storm {
-    namespace utility {
-    
-        class ExpressionHelper {
-
-        public:
-            ExpressionHelper(std::shared_ptr<storm::expressions::ExpressionManager> const& expressionManager);
-            
-            /*!
-             * Creates an expression that is the sum over all the given summands.
-             */
-            storm::expressions::Expression sum(std::vector<storm::expressions::Expression>&& summands) const;
-
-        private:
-            
-            std::shared_ptr<storm::expressions::ExpressionManager> manager;
-        };
-    
-    
-    }
-}
\ No newline at end of file

From 63a9b4485b4976506e110597b4f2a16eadda93ac Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Fri, 10 May 2019 15:41:32 +0200
Subject: [PATCH 11/11] FormulaParserGrammar: Adding support for time-bounded
 formulas with exact time-bound, e.g., F=12 "target"

---
 src/storm-parsers/parser/FormulaParserGrammar.cpp | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/storm-parsers/parser/FormulaParserGrammar.cpp b/src/storm-parsers/parser/FormulaParserGrammar.cpp
index 69c317a21..139c3e226 100644
--- a/src/storm-parsers/parser/FormulaParserGrammar.cpp
+++ b/src/storm-parsers/parser/FormulaParserGrammar.cpp
@@ -85,7 +85,9 @@ namespace storm {
             timeBound = ((timeBoundReference >> qi::lit("[")) > expressionParser > qi::lit(",") > expressionParser > qi::lit("]"))
                             [qi::_val = phoenix::bind(&FormulaParserGrammar::createTimeBoundFromInterval, phoenix::ref(*this), qi::_2, qi::_3, qi::_1)]
                         | ( timeBoundReference >> (qi::lit("<=")[qi::_a = true, qi::_b = false] | qi::lit("<")[qi::_a = true, qi::_b = true] | qi::lit(">=")[qi::_a = false, qi::_b = false] | qi::lit(">")[qi::_a = false, qi::_b = true]) >> expressionParser)
-                            [qi::_val = phoenix::bind(&FormulaParserGrammar::createTimeBoundFromSingleBound, phoenix::ref(*this), qi::_2, qi::_a, qi::_b, qi::_1)];
+                            [qi::_val = phoenix::bind(&FormulaParserGrammar::createTimeBoundFromSingleBound, phoenix::ref(*this), qi::_2, qi::_a, qi::_b, qi::_1)]
+                        | ( timeBoundReference >> qi::lit("=") >> expressionParser)
+                            [qi::_val = phoenix::bind(&FormulaParserGrammar::createTimeBoundFromInterval, phoenix::ref(*this), qi::_2, qi::_2, qi::_1)];
             timeBound.name("time bound");
             
             timeBounds = (timeBound % qi::lit(",")) | (((-qi::lit("^") >> qi::lit("{")) >> (timeBound % qi::lit(","))) >> qi::lit("}"));