From 9d70b9d768b96d33446b7a2f6b2fb9bad5edb0b9 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@rwth-aachen.de>
Date: Fri, 17 Feb 2017 17:35:12 +0100
Subject: [PATCH 01/16] fixed typo in an #include statement.

---
 src/storm/storage/geometry/NativePolytope.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/storm/storage/geometry/NativePolytope.cpp b/src/storm/storage/geometry/NativePolytope.cpp
index 29f7b594f..e095fe4ed 100644
--- a/src/storm/storage/geometry/NativePolytope.cpp
+++ b/src/storm/storage/geometry/NativePolytope.cpp
@@ -3,7 +3,7 @@
 
 #include "storm/utility/macros.h"
 #include "storm/utility/solver.h"
-#include "storm/solver/Z3LPSolver.h"
+#include "storm/solver/Z3LpSolver.h"
 #include "storm/solver/SmtSolver.h"
 #include "storm/storage/geometry/nativepolytopeconversion/QuickHull.h"
 #include "storm/storage/geometry/nativepolytopeconversion/HyperplaneEnumeration.h"

From 3c9363a323de4840a5e739c13dc8b52a6201d52e Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Mon, 20 Feb 2017 15:20:19 +0100
Subject: [PATCH 02/16] Fixed compile issue

---
 .../geometry/nativepolytopeconversion/HyperplaneEnumeration.cpp  | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/storm/storage/geometry/nativepolytopeconversion/HyperplaneEnumeration.cpp b/src/storm/storage/geometry/nativepolytopeconversion/HyperplaneEnumeration.cpp
index 52dbad648..1dbca4cdf 100644
--- a/src/storm/storage/geometry/nativepolytopeconversion/HyperplaneEnumeration.cpp
+++ b/src/storm/storage/geometry/nativepolytopeconversion/HyperplaneEnumeration.cpp
@@ -113,7 +113,6 @@ namespace storm {
                     relevantMatrix = EigenMatrix();
                     relevantVector = EigenVector();
                 }
-                STORM_LOG_DEBUG("Invoked generateVerticesFromHalfspaces with " << hPoly.getMatrix().rows() << " hyperplanes and " << resultVertices.size() << " vertices and " << relevantMatrix.rows() << " relevant hyperplanes. Dimension is " << hPoly.dimension());
             }
 
 

From adaa55a61664725c8010bf56b5bb74bc88f5249f Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Mon, 20 Feb 2017 08:59:03 +0100
Subject: [PATCH 03/16] Fixed the printing of two warnings

---
 src/storm/solver/Z3LpSolver.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/storm/solver/Z3LpSolver.cpp b/src/storm/solver/Z3LpSolver.cpp
index 95b061f70..e49845eef 100644
--- a/src/storm/solver/Z3LpSolver.cpp
+++ b/src/storm/solver/Z3LpSolver.cpp
@@ -24,7 +24,7 @@ namespace storm {
         
 #ifdef STORM_HAVE_Z3_OPTIMIZE
         Z3LpSolver::Z3LpSolver(std::string const& name, OptimizationDirection const& optDir) : LpSolver(optDir) {
-            STORM_LOG_WARN_COND(name != "", "Z3 does not support names for solvers");
+            STORM_LOG_WARN_COND(name == "", "Z3 does not support names for solvers");
             z3::config config;
             config.set("model", true);
             context = std::unique_ptr<z3::context>(new z3::context(config));
@@ -120,7 +120,7 @@ namespace storm {
         void Z3LpSolver::addConstraint(std::string const& name, storm::expressions::Expression const& constraint) {            
             STORM_LOG_THROW(constraint.isRelationalExpression(), storm::exceptions::InvalidArgumentException, "Illegal constraint is not a relational expression.");
             STORM_LOG_THROW(constraint.getOperator() != storm::expressions::OperatorType::NotEqual, storm::exceptions::InvalidArgumentException, "Illegal constraint uses inequality operator.");
-            STORM_LOG_WARN_COND(name != "", "Z3 does not support names for constraints");
+            STORM_LOG_WARN_COND(name == "", "Z3 does not support names for constraints");
             solver->add(expressionAdapter->translateExpression(constraint));
         }
         

From fd24a2586c0d47909178b5a300d5b9b989e84613 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Wed, 22 Feb 2017 18:52:24 +0100
Subject: [PATCH 04/16] added implementation for Z3LpSolver::getValue() when
 z3_optimize is not available

---
 src/storm/solver/Z3LpSolver.cpp | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/storm/solver/Z3LpSolver.cpp b/src/storm/solver/Z3LpSolver.cpp
index e49845eef..45ffbd7be 100644
--- a/src/storm/solver/Z3LpSolver.cpp
+++ b/src/storm/solver/Z3LpSolver.cpp
@@ -188,7 +188,7 @@ namespace storm {
             z3::expr z3Var = this->expressionAdapter->translateExpression(variable);
 			return this->expressionAdapter->translateExpression(lastCheckModel->eval(z3Var, true));
         }
-
+        
         double Z3LpSolver::getContinuousValue(storm::expressions::Variable const& variable) const {
             storm::expressions::Expression value = getValue(variable);
             if(value.getBaseExpression().isIntegerLiteralExpression()) {
@@ -398,6 +398,10 @@ namespace storm {
             bool Z3LpSolver::isOptimal() const {
                 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
             }
+            
+            storm::expressions::Expression Z3LpSolver::getValue(storm::expressions::Variable const& variable) const {
+                throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
+            }
 
             double Z3LpSolver::getContinuousValue(storm::expressions::Variable const&) const {
                 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";

From a22ec04f10415f2d2997be1ea8dde0bb7c6ba4d4 Mon Sep 17 00:00:00 2001
From: Tom Janson <tom.janson@rwth-aachen.de>
Date: Fri, 24 Feb 2017 22:57:51 +0100
Subject: [PATCH 05/16] fix old KSP test include

actually still works fine
---
 src/test/utility/GraphTest.cpp | 1 -
 src/test/utility/KSPTest.cpp   | 8 +-------
 2 files changed, 1 insertion(+), 8 deletions(-)

diff --git a/src/test/utility/GraphTest.cpp b/src/test/utility/GraphTest.cpp
index 051612984..ac646d99a 100644
--- a/src/test/utility/GraphTest.cpp
+++ b/src/test/utility/GraphTest.cpp
@@ -12,7 +12,6 @@
 #include "storm/builder/DdPrismModelBuilder.h"
 #include "storm/builder/ExplicitModelBuilder.h"
 #include "storm/utility/graph.h"
-#include "storm/utility/shortestPaths.cpp"
 #include "storm/storage/dd/Add.h"
 #include "storm/storage/dd/Bdd.h"
 #include "storm/storage/dd/DdManager.h"
diff --git a/src/test/utility/KSPTest.cpp b/src/test/utility/KSPTest.cpp
index 3d28ccae6..df8b4f212 100644
--- a/src/test/utility/KSPTest.cpp
+++ b/src/test/utility/KSPTest.cpp
@@ -6,15 +6,13 @@
 #include "storm/parser/PrismParser.h"
 #include "storm/storage/SymbolicModelDescription.h"
 #include "storm/utility/graph.h"
-#include "storm/utility/shortestPaths.cpp"
+#include "storm/utility/shortestPaths.h"
 
 // NOTE: The KSPs / distances of these tests were generated by the
 //       KSP-Generator itself and checked for gross implausibility, but no
 //       more than that.
 //       An independent verification of the values would be really nice ...
 
-// FIXME: (almost) all of these fail; the question is: is there actually anything wrong or does the new parser yield a different order of states?
-
 std::shared_ptr<storm::models::sparse::Model<double>> buildExampleModel() {
 	std::string prismModelPath = STORM_TEST_RESOURCES_DIR "/dtmc/brp-16-2.pm";
     storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(prismModelPath);
@@ -61,16 +59,12 @@ TEST(KSPTest, groupTarget) {
     auto groupTarget = std::vector<storm::utility::ksp::state_t>{50, 90};
     auto spg = storm::utility::ksp::ShortestPathsGenerator<double>(*model, groupTarget);
 
-    // FIXME comments are outdated (but does it even matter?)
-    // this path should lead to 90
     double dist1 = spg.getDistance(8);
     EXPECT_DOUBLE_EQ(0.00018449245583999996, dist1);
 
-    // this one to 50
     double dist2 = spg.getDistance(9);
     EXPECT_DOUBLE_EQ(0.00018449245583999996, dist2);
 
-    // this one to 90 again
     double dist3 = spg.getDistance(12);
     EXPECT_DOUBLE_EQ(7.5303043199999984e-06, dist3);
 }

From 1c322737089d61573491a31dced8e3a70d0e2202 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 3 Mar 2017 14:19:57 +0100
Subject: [PATCH 06/16] made storm_developer not override build_type if one was
 explicitly set

---
 CMakeLists.txt | 16 +++++++++-------
 1 file changed, 9 insertions(+), 7 deletions(-)

diff --git a/CMakeLists.txt b/CMakeLists.txt
index ee5bf36be..02e32c8ad 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -72,23 +72,25 @@ set(LIB_INSTALL_DIR lib/ CACHE PATH "Installation directory for libraries")
 set(BIN_INSTALL_DIR lib/ CACHE PATH "Installation directory for executables")
 
 
-# By default, we build a release version.
-if (NOT CMAKE_BUILD_TYPE)
-    set(CMAKE_BUILD_TYPE "RELEASE")
-endif()
 # Install dir for cmake files (info for other libraries that include storm)
 set(DEF_INSTALL_CMAKE_DIR "lib/CMake/storm")
 set(CMAKE_INSTALL_DIR ${DEF_INSTALL_CMAKE_DIR} CACHE PATH  "Installation directory for CMake files")
 
 message("CMAKE_INSTALL_DIR: ${CMAKE_INSTALL_DIR}")
 
-# If the STORM_DEVELOPER option was turned on, we target a debug version.
+# If the STORM_DEVELOPER option was turned on, by default we target a debug version, otherwise a release version.
 if (STORM_DEVELOPER)
-    set(CMAKE_BUILD_TYPE "DEBUG")
-    set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -DSTORM_DEV")
+    if (NOT CMAKE_BUILD_TYPE)
+        set(CMAKE_BUILD_TYPE "DEBUG")
+    endif()
+    add_definitions(-DSTORM_DEV)
 else()
     set(STORM_LOG_DISABLE_DEBUG ON)
+    if (NOT CMAKE_BUILD_TYPE)
+        set(CMAKE_BUILD_TYPE "RELEASE")
+    endif()
 endif()
+
 message(STATUS "storm - Building ${CMAKE_BUILD_TYPE} version.")
 
 if(STORM_COMPILE_WITH_CCACHE)

From e5404a27e9289aeea7c42782bfb379a4cfb62e74 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Sun, 5 Mar 2017 19:58:59 +0100
Subject: [PATCH 07/16] Implemented parsing for
 UnaryNumericalFunctionExpression

---
 .../storage/expressions/ToRationalFunctionVisitor.cpp | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

diff --git a/src/storm/storage/expressions/ToRationalFunctionVisitor.cpp b/src/storm/storage/expressions/ToRationalFunctionVisitor.cpp
index 6fa620157..870014f60 100644
--- a/src/storm/storage/expressions/ToRationalFunctionVisitor.cpp
+++ b/src/storm/storage/expressions/ToRationalFunctionVisitor.cpp
@@ -94,8 +94,15 @@ namespace storm {
         }
         
         template<typename RationalFunctionType>
-        boost::any ToRationalFunctionVisitor<RationalFunctionType>::visit(UnaryNumericalFunctionExpression const&, boost::any const&) {
-            STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational function.");
+        boost::any ToRationalFunctionVisitor<RationalFunctionType>::visit(UnaryNumericalFunctionExpression const& expression, boost::any const& data) {
+            RationalFunctionType operandAsRationalFunction = boost::any_cast<RationalFunctionType>(expression.getOperand()->accept(*this, data));
+            switch (expression.getOperatorType()) {
+                case UnaryNumericalFunctionExpression::OperatorType::Minus:
+                    return -operandAsRationalFunction;
+                default:
+                    STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational function.");
+            }
+            return boost::any();
         }
         
         template<typename RationalFunctionType>

From 0b6c481cf20d7c4777fef85af537bcccca2ce495 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Tue, 7 Mar 2017 20:17:10 +0100
Subject: [PATCH 08/16] fix for sparse mdp model checker: computing cumulative
 rewards did one step too much

---
 .../modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp   | 9 ++-------
 1 file changed, 2 insertions(+), 7 deletions(-)

diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
index 2db593ac9..fc1649d19 100644
--- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
+++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
@@ -226,13 +226,8 @@ namespace storm {
                 // Compute the reward vector to add in each step based on the available reward models.
                 std::vector<ValueType> totalRewardVector = rewardModel.getTotalRewardVector(transitionMatrix);
                 
-                // Initialize result to either the state rewards of the model or the null vector.
-                std::vector<ValueType> result;
-                if (rewardModel.hasStateRewards()) {
-                    result = rewardModel.getStateRewardVector();
-                } else {
-                    result.resize(transitionMatrix.getRowGroupCount());
-                }
+                // Initialize result to the zero vector.
+                std::vector<ValueType> result(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
                 
                 std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = minMaxLinearEquationSolverFactory.create(transitionMatrix);
                 solver->repeatedMultiply(dir, result, &totalRewardVector, stepBound);

From b3a02b6e8af3ffb1ae9d0741aa6dd39ef7feab7b Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Wed, 8 Mar 2017 11:25:54 +0100
Subject: [PATCH 09/16] fix in sparse ctmc model checker: bounded until
 returned empty result in case there are no non-prob0-states

---
 src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp       | 2 ++
 .../modelchecker/results/ExplicitQuantitativeCheckResult.cpp    | 1 +
 2 files changed, 3 insertions(+)

diff --git a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
index 10995f9b7..1dff5b454 100644
--- a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
+++ b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
@@ -186,6 +186,8 @@ namespace storm {
                             }
                         }
                     }
+                } else {
+                    result = std::vector<ValueType>(numberOfStates, storm::utility::zero<ValueType>());
                 }
                 
                 return result;
diff --git a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp
index 5ea662a57..f9231a22c 100644
--- a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp
+++ b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp
@@ -61,6 +61,7 @@ namespace storm {
 
             if (this->isResultForAllStates()) {
                 map_type newMap;
+                
                 for (auto const& element : filterTruthValues) {
                     STORM_LOG_THROW(element < this->getValueVector().size(), storm::exceptions::InvalidAccessException, "Invalid index in results.");
                     newMap.emplace(element, this->getValueVector()[element]);

From 3f0afe952682dc810e7c0fc9a5be92c360d3c19e Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 10 Mar 2017 11:47:44 +0100
Subject: [PATCH 10/16] allowing underscore and dots as identifier symbols in
 exprtk

---
 resources/3rdparty/exprtk/exprtk.hpp | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/resources/3rdparty/exprtk/exprtk.hpp b/resources/3rdparty/exprtk/exprtk.hpp
index 04f37d9a1..079ee1b6f 100755
--- a/resources/3rdparty/exprtk/exprtk.hpp
+++ b/resources/3rdparty/exprtk/exprtk.hpp
@@ -97,7 +97,11 @@ namespace exprtk
         inline bool is_letter(const char_t c)
         {
             return (('a' <= c) && (c <= 'z')) ||
-            (('A' <= c) && (c <= 'Z')) ;
+            (('A' <= c) && (c <= 'Z'))
+#ifdef MODIFICATION
+            || ('.' == c) || ('_' == c)
+#endif
+            ;
         }
         
         inline bool is_digit(const char_t c)

From a323d217518e54a476bf0353270d1587b6efe7a2 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 10 Mar 2017 21:44:10 +0100
Subject: [PATCH 11/16] fixed some wrong capitalization

---
 src/storm-dft-cli/storm-dyftee.cpp            |  4 +-
 src/storm-gspn-cli/storm-gspn.cpp             |  4 +-
 src/storm-gspn/parser/GspnParser.cpp          |  2 +-
 src/storm-pgcl-cli/storm-pgcl.cpp             |  4 +-
 src/storm/CMakeLists.txt                      |  4 +-
 src/storm/parser/JaniParser.cpp               | 14 +++----
 src/storm/solver/MathsatSmtSolver.cpp         | 32 ++++++++--------
 .../TopologicalMinMaxLinearEquationSolver.h   |  8 ++--
 src/storm/solver/Z3SmtSolver.cpp              | 38 +++++++++----------
 src/storm/storage/jani/JSONExporter.cpp       |  2 +-
 src/storm/storm.cpp                           |  4 +-
 src/test/storm-test.cpp                       |  2 +-
 12 files changed, 59 insertions(+), 59 deletions(-)

diff --git a/src/storm-dft-cli/storm-dyftee.cpp b/src/storm-dft-cli/storm-dyftee.cpp
index c018108ec..4feb408a6 100644
--- a/src/storm-dft-cli/storm-dyftee.cpp
+++ b/src/storm-dft-cli/storm-dyftee.cpp
@@ -80,7 +80,7 @@ void analyzeWithSMT(std::string filename) {
  * Initialize the settings manager.
  */
 void initializeSettings() {
-    storm::settings::mutableManager().setName("storm-DyFTeE", "storm-dft");
+    storm::settings::mutableManager().setName("Storm-DyFTeE", "storm-dft");
     
     // Register all known settings modules.
     storm::settings::addModule<storm::settings::modules::GeneralSettings>();
@@ -118,7 +118,7 @@ void initializeSettings() {
 int main(const int argc, const char** argv) {
     try {
         storm::utility::setUp();
-        storm::cli::printHeader("storm-DyFTeE", argc, argv);
+        storm::cli::printHeader("Storm-DyFTeE", argc, argv);
         initializeSettings();
         
         bool optionsCorrect = storm::cli::parseOptions(argc, argv);
diff --git a/src/storm-gspn-cli/storm-gspn.cpp b/src/storm-gspn-cli/storm-gspn.cpp
index bbff2c9cc..e7e03b157 100644
--- a/src/storm-gspn-cli/storm-gspn.cpp
+++ b/src/storm-gspn-cli/storm-gspn.cpp
@@ -40,7 +40,7 @@
  * Initialize the settings manager.
  */
 void initializeSettings() {
-    storm::settings::mutableManager().setName("storm-GSPN", "storm-gspn");
+    storm::settings::mutableManager().setName("Storm-GSPN", "storm-gspn");
     
     // Register all known settings modules.
     storm::settings::addModule<storm::settings::modules::GeneralSettings>();
@@ -75,7 +75,7 @@ std::unordered_map<std::string, uint64_t> parseCapacitiesList(std::string const&
 int main(const int argc, const char **argv) {
     try {
         storm::utility::setUp();
-        storm::cli::printHeader("storm-GSPN", argc, argv);
+        storm::cli::printHeader("Storm-GSPN", argc, argv);
         initializeSettings();
         
         bool optionsCorrect = storm::cli::parseOptions(argc, argv);
diff --git a/src/storm-gspn/parser/GspnParser.cpp b/src/storm-gspn/parser/GspnParser.cpp
index cf5c698f0..b92b6f006 100644
--- a/src/storm-gspn/parser/GspnParser.cpp
+++ b/src/storm-gspn/parser/GspnParser.cpp
@@ -81,7 +81,7 @@ namespace storm {
             delete errHandler;
             xercesc::XMLPlatformUtils::Terminate();
 #else
-            STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "storm is not compiled with XML support: " << filename << " can not be parsed");
+            STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Storm is not compiled with XML support: " << filename << " can not be parsed");
 #endif
         }
     }
diff --git a/src/storm-pgcl-cli/storm-pgcl.cpp b/src/storm-pgcl-cli/storm-pgcl.cpp
index 2fa9385a2..4e4031ee4 100644
--- a/src/storm-pgcl-cli/storm-pgcl.cpp
+++ b/src/storm-pgcl-cli/storm-pgcl.cpp
@@ -25,7 +25,7 @@
  * Initialize the settings manager.
  */
 void initializeSettings() {
-    storm::settings::mutableManager().setName("storm-PGCL", "storm-pgcl");
+    storm::settings::mutableManager().setName("Storm-PGCL", "storm-pgcl");
     
     // Register all known settings modules.
     storm::settings::addModule<storm::settings::modules::GeneralSettings>();
@@ -56,7 +56,7 @@ void programGraphToDotFile(storm::ppg::ProgramGraph const& prog) {
 int main(const int argc, const char** argv) {
     try {
         storm::utility::setUp();
-        storm::cli::printHeader("storm-PGCL", argc, argv);
+        storm::cli::printHeader("Storm-PGCL", argc, argv);
         initializeSettings();
         
         bool optionsCorrect = storm::cli::parseOptions(argc, argv);
diff --git a/src/storm/CMakeLists.txt b/src/storm/CMakeLists.txt
index 1a722e207..18ac14200 100644
--- a/src/storm/CMakeLists.txt
+++ b/src/storm/CMakeLists.txt
@@ -20,11 +20,11 @@ set(STORM_MAIN_SOURCES  ${STORM_MAIN_FILE})
 
 # Add custom additional include or link directories
 if (ADDITIONAL_INCLUDE_DIRS)
-	message(STATUS "storm - Using additional include directories ${ADDITIONAL_INCLUDE_DIRS}")
+	message(STATUS "Storm - Using additional include directories ${ADDITIONAL_INCLUDE_DIRS}")
 	include_directories(${ADDITIONAL_INCLUDE_DIRS})
 endif(ADDITIONAL_INCLUDE_DIRS)
 if (ADDITIONAL_LINK_DIRS)
-	message(STATUS "storm - Using additional link directories ${ADDITIONAL_LINK_DIRS}")
+	message(STATUS "Storm - Using additional link directories ${ADDITIONAL_LINK_DIRS}")
 	link_directories(${ADDITIONAL_LINK_DIRS})
 endif(ADDITIONAL_LINK_DIRS)
 
diff --git a/src/storm/parser/JaniParser.cpp b/src/storm/parser/JaniParser.cpp
index 826c8075b..d743d9ced 100644
--- a/src/storm/parser/JaniParser.cpp
+++ b/src/storm/parser/JaniParser.cpp
@@ -237,12 +237,12 @@ namespace storm {
                             }
                         }
                     }
-                    STORM_LOG_THROW(!(accTime && accSteps), storm::exceptions::NotSupportedException, "storm does not allow to accumulate over both time and steps");
+                    STORM_LOG_THROW(!(accTime && accSteps), storm::exceptions::NotSupportedException, "Storm does not allow to accumulate over both time and steps");
                     
                     
                     if (propertyStructure.count("step-instant") > 0) {
                         storm::expressions::Expression stepInstantExpr = parseExpression(propertyStructure.at("step-instant"), "Step instant in " + context);
-                        STORM_LOG_THROW(!stepInstantExpr.containsVariables(), storm::exceptions::NotSupportedException, "storm only allows constant step-instants");
+                        STORM_LOG_THROW(!stepInstantExpr.containsVariables(), storm::exceptions::NotSupportedException, "Storm only allows constant step-instants");
                         int64_t stepInstant = stepInstantExpr.evaluateAsInt();
                         STORM_LOG_THROW(stepInstant >= 0, storm::exceptions::InvalidJaniException, "Only non-negative step-instants are allowed");
                         if(!accTime && !accSteps) {
@@ -262,7 +262,7 @@ namespace storm {
                         }
                     } else if (propertyStructure.count("time-instant") > 0) {
                         storm::expressions::Expression timeInstantExpr = parseExpression(propertyStructure.at("time-instant"), "time instant in " + context);
-                        STORM_LOG_THROW(!timeInstantExpr.containsVariables(), storm::exceptions::NotSupportedException, "storm only allows constant time-instants");
+                        STORM_LOG_THROW(!timeInstantExpr.containsVariables(), storm::exceptions::NotSupportedException, "Storm only allows constant time-instants");
                         double timeInstant = timeInstantExpr.evaluateAsDouble();
                         STORM_LOG_THROW(timeInstant >= 0, storm::exceptions::InvalidJaniException, "Only non-negative time-instants are allowed");
                         if(!accTime && !accSteps) {
@@ -284,7 +284,7 @@ namespace storm {
                         STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Instant/Cumul. Reward for reward constraints not supported currently.");
                     }
                     
-                    //STORM_LOG_THROW(!accTime && !accSteps, storm::exceptions::NotSupportedException, "storm only allows accumulation if a step- or time-bound is given.");
+                    //STORM_LOG_THROW(!accTime && !accSteps, storm::exceptions::NotSupportedException, "Storm only allows accumulation if a step- or time-bound is given.");
                     
                     if (rewExpr.isVariable()) {
                         std::string rewardName = rewExpr.getVariables().begin()->getName();
@@ -328,9 +328,9 @@ namespace storm {
                     }
                     if (propertyStructure.count("step-bounds") > 0) {
                         storm::jani::PropertyInterval pi = parsePropertyInterval(propertyStructure.at("step-bounds"));
-                        STORM_LOG_THROW(pi.hasUpperBound(), storm::exceptions::NotSupportedException, "storm only supports step-bounded until with an upper bound");
+                        STORM_LOG_THROW(pi.hasUpperBound(), storm::exceptions::NotSupportedException, "Storm only supports step-bounded until with an upper bound");
                         if(pi.hasLowerBound()) {
-                            STORM_LOG_THROW(pi.lowerBound.evaluateAsInt() == 0, storm::exceptions::NotSupportedException, "storm only supports step-bounded until without a (non-trivial) lower-bound");
+                            STORM_LOG_THROW(pi.lowerBound.evaluateAsInt() == 0, storm::exceptions::NotSupportedException, "Storm only supports step-bounded until without a (non-trivial) lower-bound");
                         }
                         int64_t upperBound = pi.upperBound.evaluateAsInt();
                         if(pi.upperBoundStrict) {
@@ -340,7 +340,7 @@ namespace storm {
                         return std::make_shared<storm::logic::BoundedUntilFormula const>(args[0], args[1], storm::logic::TimeBound(pi.lowerBoundStrict, pi.lowerBound), storm::logic::TimeBound(pi.upperBoundStrict, pi.upperBound), storm::logic::TimeBoundType::Steps);
                     } else if (propertyStructure.count("time-bounds") > 0) {
                         storm::jani::PropertyInterval pi = parsePropertyInterval(propertyStructure.at("time-bounds"));
-                        STORM_LOG_THROW(pi.hasUpperBound(), storm::exceptions::NotSupportedException, "storm only supports time-bounded until with an upper bound.");
+                        STORM_LOG_THROW(pi.hasUpperBound(), storm::exceptions::NotSupportedException, "Storm only supports time-bounded until with an upper bound.");
                         double lowerBound = 0.0;
                         if(pi.hasLowerBound()) {
                             lowerBound = pi.lowerBound.evaluateAsDouble();
diff --git a/src/storm/solver/MathsatSmtSolver.cpp b/src/storm/solver/MathsatSmtSolver.cpp
index d7501ad53..9b6f7da2b 100644
--- a/src/storm/solver/MathsatSmtSolver.cpp
+++ b/src/storm/solver/MathsatSmtSolver.cpp
@@ -107,7 +107,7 @@ namespace storm {
 #ifdef STORM_HAVE_MSAT
 			msat_push_backtrack_point(env);
 #else
-			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support.");
+			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without MathSAT support.");
 #endif
 		}
 
@@ -115,7 +115,7 @@ namespace storm {
 #ifdef STORM_HAVE_MSAT
 			msat_pop_backtrack_point(env);
 #else
-			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support.");
+			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without MathSAT support.");
 #endif
 		}
 
@@ -123,7 +123,7 @@ namespace storm {
 #ifdef STORM_HAVE_MSAT
             SmtSolver::pop(n);
 #else
-            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support.");
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without MathSAT support.");
 #endif
         }
         
@@ -132,7 +132,7 @@ namespace storm {
 #ifdef STORM_HAVE_MSAT
 			msat_reset_env(env);
 #else
-			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support.");
+			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without MathSAT support.");
 #endif
 		}
 
@@ -141,7 +141,7 @@ namespace storm {
 #ifdef STORM_HAVE_MSAT
 			msat_assert_formula(env, expressionAdapter->translateExpression(e));
 #else
-			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support.");
+			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without MathSAT support.");
 #endif
 		}
 
@@ -162,7 +162,7 @@ namespace storm {
 			}
 			return this->lastResult;
 #else
-			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support.");
+			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without MathSAT support.");
 #endif
 		}
 
@@ -190,7 +190,7 @@ namespace storm {
 			}
 			return this->lastResult;
 #else
-			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support.");
+			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without MathSAT support.");
 #endif
 		}
 
@@ -219,7 +219,7 @@ namespace storm {
 			}
 			return this->lastResult;
 #else
-			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support.");
+			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without MathSAT support.");
 #endif
 		}
 #endif
@@ -230,7 +230,7 @@ namespace storm {
 			STORM_LOG_THROW(this->lastResult == SmtSolver::CheckResult::Sat, storm::exceptions::InvalidStateException, "Unable to create model for formula that was not determined to be satisfiable.");
 			return this->convertMathsatModelToValuation();
 #else
-			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support.");
+			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without MathSAT support.");
 #endif
 		}
         
@@ -239,7 +239,7 @@ namespace storm {
 			STORM_LOG_THROW(this->lastResult == SmtSolver::CheckResult::Sat, storm::exceptions::InvalidStateException, "Unable to create model for formula that was not determined to be satisfiable.");
             return std::shared_ptr<SmtSolver::ModelReference>(new MathsatModelReference(this->getManager(), env, *expressionAdapter));
 #else
-			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support.");
+			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without MathSAT support.");
 #endif
         }
 
@@ -279,7 +279,7 @@ namespace storm {
 			this->allSat(important, [&valuations](storm::expressions::SimpleValuation const& valuation) -> bool { valuations.push_back(valuation); return true; });
 			return valuations;
 #else
-			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support.");
+			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without MathSAT support.");
 #endif
 		}
 
@@ -379,7 +379,7 @@ namespace storm {
             this->pop();
 			return static_cast<uint_fast64_t>(numberOfModels);
 #else
-			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support.");
+			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without MathSAT support.");
 #endif
 		}
 
@@ -405,7 +405,7 @@ namespace storm {
             this->pop();
             return static_cast<uint_fast64_t>(numberOfModels);
 #else
-			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support.");
+			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without MathSAT support.");
 #endif
 		}
 
@@ -426,7 +426,7 @@ namespace storm {
 
 			return unsatAssumptions;
 #else
-			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support.");
+			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without MathSAT support.");
 #endif
 		}
 
@@ -440,7 +440,7 @@ namespace storm {
 			}
 			msat_set_itp_group(env, groupIter->second);
 #else
-			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support.");
+			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without MathSAT support.");
 #endif
 		}
 
@@ -462,7 +462,7 @@ namespace storm {
             
 			return this->expressionAdapter->translateExpression(interpolant);
 #else
-			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support.");
+			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without MathSAT support.");
 #endif
 		}
 	}
diff --git a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.h b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.h
index c8af93f13..70338ce21 100644
--- a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.h
+++ b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.h
@@ -73,7 +73,7 @@ namespace storm {
 #ifdef STORM_HAVE_CUDA
             return basicValueIteration_mvReduce_uint64_double_minimize(maxIterationCount, precision, relativePrecisionCheck, matrixRowIndices, columnIndicesAndValues, x, b, nondeterministicChoiceIndices, iterationCount);
 #else
-            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without CUDA support.");
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without CUDA support.");
 #endif
         }
         template <>
@@ -92,7 +92,7 @@ namespace storm {
 #ifdef STORM_HAVE_CUDA
             return basicValueIteration_mvReduce_uint64_float_minimize(maxIterationCount, precision, relativePrecisionCheck, matrixRowIndices, columnIndicesAndValues, x, b, nondeterministicChoiceIndices, iterationCount);
 #else
-            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without CUDA support.");
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without CUDA support.");
 #endif
         }
         
@@ -116,7 +116,7 @@ namespace storm {
 #ifdef STORM_HAVE_CUDA
             return basicValueIteration_mvReduce_uint64_double_maximize(maxIterationCount, precision, relativePrecisionCheck, matrixRowIndices, columnIndicesAndValues, x, b, nondeterministicChoiceIndices, iterationCount);
 #else
-            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without CUDA support.");
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without CUDA support.");
 #endif
         }
         template <>
@@ -135,7 +135,7 @@ namespace storm {
 #ifdef STORM_HAVE_CUDA
             return basicValueIteration_mvReduce_uint64_float_maximize(maxIterationCount, precision, relativePrecisionCheck, matrixRowIndices, columnIndicesAndValues, x, b, nondeterministicChoiceIndices, iterationCount);
 #else
-            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without CUDA support.");
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without CUDA support.");
 #endif
         }
         
diff --git a/src/storm/solver/Z3SmtSolver.cpp b/src/storm/solver/Z3SmtSolver.cpp
index cb291bcb9..cff81e5e7 100644
--- a/src/storm/solver/Z3SmtSolver.cpp
+++ b/src/storm/solver/Z3SmtSolver.cpp
@@ -19,7 +19,7 @@ namespace storm {
 			z3::expr z3ExprValuation = model.eval(z3Expr, true);
 			return this->expressionAdapter.translateExpression(z3ExprValuation).isTrue();
 #else
-			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support.");
+			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support.");
 #endif
 		}
 
@@ -30,7 +30,7 @@ namespace storm {
 			z3::expr z3ExprValuation = model.eval(z3Expr, true);
 			return this->expressionAdapter.translateExpression(z3ExprValuation).evaluateAsInt();
 #else
-			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support.");
+			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support.");
 #endif
 		}
 
@@ -41,7 +41,7 @@ namespace storm {
 			z3::expr z3ExprValuation = model.eval(z3Expr, true);
 			return this->expressionAdapter.translateExpression(z3ExprValuation).evaluateAsDouble();
 #else
-			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support.");
+			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support.");
 #endif
 		}
         
@@ -68,7 +68,7 @@ namespace storm {
 #ifdef STORM_HAVE_Z3
 			this->solver->push();
 #else
-			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support.");
+			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support.");
 #endif
 		}
 
@@ -77,7 +77,7 @@ namespace storm {
 #ifdef STORM_HAVE_Z3
 			this->solver->pop();
 #else
-			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support.");
+			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support.");
 #endif
 		}
 
@@ -86,7 +86,7 @@ namespace storm {
 #ifdef STORM_HAVE_Z3
 			this->solver->pop(static_cast<unsigned int>(n));
 #else
-			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support.");
+			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support.");
 #endif
 		}
 
@@ -95,7 +95,7 @@ namespace storm {
 #ifdef STORM_HAVE_Z3
 			this->solver->reset();
 #else
-			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support.");
+			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support.");
 #endif
 		}
 
@@ -104,7 +104,7 @@ namespace storm {
 #ifdef STORM_HAVE_Z3
 			this->solver->add(expressionAdapter->translateExpression(assertion));
 #else
-			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support.");
+			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support.");
 #endif
 		}
 
@@ -125,7 +125,7 @@ namespace storm {
 			}
 			return this->lastResult;
 #else
-			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support.");
+			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support.");
 #endif
 		}
 
@@ -152,7 +152,7 @@ namespace storm {
 			}
 			return this->lastResult;
 #else
-			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support.");
+			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support.");
 #endif
 		}
 
@@ -180,7 +180,7 @@ namespace storm {
 			}
 			return this->lastResult;
 #else
-			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support.");
+			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support.");
 #endif
 		}
 #endif
@@ -190,7 +190,7 @@ namespace storm {
 			STORM_LOG_THROW(this->lastResult == SmtSolver::CheckResult::Sat, storm::exceptions::InvalidStateException, "Unable to create model for formula that was not determined to be satisfiable.");
 			return this->convertZ3ModelToValuation(this->solver->get_model());
 #else
-			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support.");
+			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support.");
 #endif
 		}
         
@@ -199,7 +199,7 @@ namespace storm {
 			STORM_LOG_THROW(this->lastResult == SmtSolver::CheckResult::Sat, storm::exceptions::InvalidStateException, "Unable to create model for formula that was not determined to be satisfiable.");
             return std::shared_ptr<SmtSolver::ModelReference>(new Z3ModelReference(this->getManager(), this->solver->get_model(), *this->expressionAdapter));
 #else
-            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support.");
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support.");
 #endif
         }
 
@@ -234,7 +234,7 @@ namespace storm {
 			this->allSat(important, static_cast<std::function<bool(storm::expressions::SimpleValuation&)>>([&valuations](storm::expressions::SimpleValuation const& valuation) -> bool { valuations.push_back(valuation); return true; }));
 			return valuations;
 #else
-			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support.");
+			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support.");
 #endif
 		}
 
@@ -276,7 +276,7 @@ namespace storm {
 			this->pop();
 			return numberOfModels;
 #else
-			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support.");
+			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support.");
 #endif
 		}
 
@@ -317,7 +317,7 @@ namespace storm {
 			this->pop();
 			return numberOfModels;
 #else
-			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support.");
+			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support.");
 #endif
 		}
 
@@ -335,7 +335,7 @@ namespace storm {
 
 			return unsatAssumptions;
 #else
-			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support.");
+			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support.");
 #endif
 		}
         
@@ -346,7 +346,7 @@ namespace storm {
             solver->set(paramObject);
             return true;
 #else
-            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support.");
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support.");
 #endif
         }
         
@@ -357,7 +357,7 @@ namespace storm {
             solver->set(paramObject);
             return true;
 #else
-            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support.");
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support.");
 #endif
         }
 
diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp
index c39a6b79b..fc5346c0d 100644
--- a/src/storm/storage/jani/JSONExporter.cpp
+++ b/src/storm/storage/jani/JSONExporter.cpp
@@ -183,7 +183,7 @@ namespace storm {
         }
         
         boost::any FormulaToJaniJson::visit(storm::logic::CumulativeRewardFormula const&, boost::any const&) const {
-            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm currently does not support translating  cummulative reward formulae");
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm currently does not support translating cumulative reward formulae");
         }
         
         boost::any FormulaToJaniJson::visit(storm::logic::EventuallyFormula const& f, boost::any const& data) const {
diff --git a/src/storm/storm.cpp b/src/storm/storm.cpp
index 73c5a8a15..c21be38a0 100644
--- a/src/storm/storm.cpp
+++ b/src/storm/storm.cpp
@@ -17,8 +17,8 @@ int main(const int argc, const char** argv) {
     try {
         storm::utility::Stopwatch totalTimer(true);
         storm::utility::setUp();
-        storm::cli::printHeader("storm", argc, argv);
-        storm::settings::initializeAll("storm", "storm");
+        storm::cli::printHeader("Storm", argc, argv);
+        storm::settings::initializeAll("Storm", "storm");
         bool optionsCorrect = storm::cli::parseOptions(argc, argv);
         if (!optionsCorrect) {
             return -1;
diff --git a/src/test/storm-test.cpp b/src/test/storm-test.cpp
index a88084304..7f33be83a 100644
--- a/src/test/storm-test.cpp
+++ b/src/test/storm-test.cpp
@@ -2,7 +2,7 @@
 #include "storm/settings/SettingsManager.h"
 
 int main(int argc, char **argv) {
-  storm::settings::initializeAll("storm (Functional) Testing Suite", "test");
+  storm::settings::initializeAll("Storm (Functional) Testing Suite", "test");
   ::testing::InitGoogleTest(&argc, argv);
   return RUN_ALL_TESTS();
 }

From 98d956275af26bb93481e434f82ac5a34eebbc40 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 10 Mar 2017 21:56:00 +0100
Subject: [PATCH 12/16] reworked version detection via git/defaults if not
 available

---
 CMakeLists.txt                    | 94 +++++++++++++------------------
 src/storm/cli/cli.cpp             |  2 +-
 src/storm/utility/storm-version.h | 24 +++++---
 storm-version.cpp.in              |  8 +--
 4 files changed, 60 insertions(+), 68 deletions(-)

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 02e32c8ad..294328776 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -18,7 +18,7 @@ include(imported)
 
 #############################################################
 ##
-##	CMake options of storm
+##	CMake options of Storm
 ##
 #############################################################
 option(STORM_DEVELOPER "Sets whether the development mode is used." OFF)
@@ -44,7 +44,7 @@ option(STORM_COMPILE_WITH_CCACHE "Compile using CCache [if found]" ON)
 mark_as_advanced(STORM_COMPILE_WITH_CCACHE)
 option(STORM_LOG_DISABLE_DEBUG "Disable log and trace message support" OFF)
 option(STORM_USE_CLN_NUMBERS "Sets whether CLN or GMP numbers should be used" ON)
-option(BUILD_SHARED_LIBS "Build the storm library dynamically" OFF)
+option(BUILD_SHARED_LIBS "Build the Storm library dynamically" OFF)
 set(BOOST_ROOT "" CACHE STRING "A hint to the root directory of Boost (optional).")
 set(GUROBI_ROOT "" CACHE STRING "A hint to the root directory of Gurobi (optional).")
 set(Z3_ROOT "" CACHE STRING "A hint to the root directory of Z3 (optional).")
@@ -55,11 +55,6 @@ set(ADDITIONAL_LINK_DIRS "" CACHE STRING "Additional directories added to the li
 set(USE_XERCESC ${XML_SUPPORT})
 mark_as_advanced(USE_XERCESC)
 
-# Sets the source from which storm is obtained. Can be either "git" or "archive". This
-# influences, among other things, the version information.
-set(STORM_SOURCE "git" CACHE STRING "The source from which storm is obtained: either 'git' or 'archive'.")
-mark_as_advanced(STORM_SOURCE)
-
 # Set some CMAKE Variables as advanced
 mark_as_advanced(CMAKE_OSX_ARCHITECTURES)
 mark_as_advanced(CMAKE_OSX_SYSROOT)
@@ -72,7 +67,7 @@ set(LIB_INSTALL_DIR lib/ CACHE PATH "Installation directory for libraries")
 set(BIN_INSTALL_DIR lib/ CACHE PATH "Installation directory for executables")
 
 
-# Install dir for cmake files (info for other libraries that include storm)
+# Install dir for cmake files (info for other libraries that include Storm)
 set(DEF_INSTALL_CMAKE_DIR "lib/CMake/storm")
 set(CMAKE_INSTALL_DIR ${DEF_INSTALL_CMAKE_DIR} CACHE PATH  "Installation directory for CMake files")
 
@@ -91,17 +86,17 @@ else()
     endif()
 endif()
 
-message(STATUS "storm - Building ${CMAKE_BUILD_TYPE} version.")
+message(STATUS "Storm - Building ${CMAKE_BUILD_TYPE} version.")
 
 if(STORM_COMPILE_WITH_CCACHE)
 	find_program(CCACHE_FOUND ccache)
 	mark_as_advanced(CCACHE_FOUND)
 	if(CCACHE_FOUND)
-		message(STATUS "storm - Using ccache")
+		message(STATUS "Storm - Using ccache")
 		set_property(GLOBAL PROPERTY RULE_LAUNCH_COMPILE ccache)
 		set_property(GLOBAL PROPERTY RULE_LAUNCH_LINK ccache)
 	else()
-		message(STATUS "storm - Could not find ccache.")
+		message(STATUS "Storm - Could not find ccache.")
 	endif()
 endif()
 
@@ -127,7 +122,7 @@ else()
     set(OPERATING_SYSTEM "Linux")
     set(LINUX 1)
 ENDIF()
-message(STATUS "storm - Detected operating system ${OPERATING_SYSTEM}.")
+message(STATUS "Storm - Detected operating system ${OPERATING_SYSTEM}.")
 
 set(DYNAMIC_EXT ".so")
 set(STATIC_EXT ".a")
@@ -305,12 +300,12 @@ if ("${CMAKE_GENERATOR}" STREQUAL "Xcode")
 endif()
 
 # Display information about build configuration.
-message(STATUS "storm - Using compiler configuration ${STORM_COMPILER_ID} ${STORM_COMPILER_VERSION}.")
+message(STATUS "Storm - Using compiler configuration ${STORM_COMPILER_ID} ${STORM_COMPILER_VERSION}.")
 if (STORM_DEVELOPER)
-	message(STATUS "storm - CXX Flags: ${CMAKE_CXX_FLAGS}")
-	message(STATUS "storm - CXX Debug Flags: ${CMAKE_CXX_FLAGS_DEBUG}")
-	message(STATUS "storm - CXX Release Flags: ${CMAKE_CXX_FLAGS_RELEASE}")
-	message(STATUS "storm - Build type: ${CMAKE_BUILD_TYPE}")
+	message(STATUS "Storm - CXX Flags: ${CMAKE_CXX_FLAGS}")
+	message(STATUS "Storm - CXX Debug Flags: ${CMAKE_CXX_FLAGS_DEBUG}")
+	message(STATUS "Storm - CXX Release Flags: ${CMAKE_CXX_FLAGS_RELEASE}")
+	message(STATUS "Storm - Build type: ${CMAKE_BUILD_TYPE}")
 endif()
 
 #############################################################
@@ -350,50 +345,41 @@ endif(DOXYGEN_FOUND)
 
 #############################################################
 ##
-##	CMake-generated Config File for storm
+##	CMake-generated Config File for Storm
 ##
 #############################################################
 
-# If storm is built from an archive, we need to skip the version detection based on git.
-if (STORM_SOURCE STREQUAL "archive")
-	if (NOT DEFINED STORM_VERSION_MAJOR OR NOT DEFINED STORM_VERSION_MINOR OR NOT DEFINED STORM_VERSION_PATCH)
-		message(FATAL_ERROR "storm - building from archive requires setting a version via cmake.")
-	endif()
-	message(STATUS "storm - version is ${STORM_VERSION_MAJOR}.${STORM_VERSION_MINOR}.${STORM_VERSION_PATCH} (building from archive).")
-	set(STORM_VERSION_COMMITS_AHEAD boost::none)
-	set(STORM_VERSION_GIT_HASH boost::none)
+# try to obtain the current version from git.
+include(GetGitRevisionDescription)
+get_git_head_revision(STORM_VERSION_REFSPEC STORM_VERSION_GIT_HASH)
+git_describe_checkout(STORM_GIT_VERSION_STRING)
+
+# parse the git tag into variables
+string(REGEX REPLACE "^([0-9]+)\\..*" "\\1" STORM_VERSION_MAJOR "${STORM_GIT_VERSION_STRING}")
+string(REGEX REPLACE "^[0-9]+\\.([0-9]+).*" "\\1" STORM_VERSION_MINOR "${STORM_GIT_VERSION_STRING}")
+string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.([0-9]+).*" "\\1" STORM_VERSION_PATCH "${STORM_GIT_VERSION_STRING}")
+string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.[0-9]+\\-([0-9]+)\\-.*" "\\1" STORM_VERSION_COMMITS_AHEAD "${STORM_GIT_VERSION_STRING}")
+string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.[0-9]+\\-[0-9]+\\-([a-z0-9]+).*" "\\1" STORM_VERSION_TAG_HASH "${STORM_GIT_VERSION_STRING}")
+string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.[0-9]+\\-[0-9]+\\-[a-z0-9]+\\-(.*)" "\\1" STORM_VERSION_APPENDIX "${STORM_GIT_VERSION_STRING}")
+	
+# now check whether the git version lookup failed
+if (STORM_VERSION_MAJOR STREQUAL "HEAD-HASH-NOTFOUND")
+	set(STORM_VERSION_MAJOR 1)
+	set(STORM_VERSION_MINOR 0)
+	set(STORM_VERSION_PATCH 0)
+	set(STORM_VERSION_GIT_HASH "")
+	set(STORM_VERSION_COMMITS_AHEAD 0)
 	set(STORM_VERSION_DIRTY boost::none)
+
+	message(WARN "Storm - git version information not available.")
+	message(STATUS "Storm - version is ${STORM_VERSION_MAJOR}.${STORM_VERSION_MINOR}.${STORM_VERSION_PATCH}.")
 else()
-	if (DEFINED STORM_VERSION_MAJOR OR DEFINED STORM_VERSION_MINOR OR DEFINED STORM_VERSION_PATCH)
-		message(FATAL_ERROR "storm - building from git does not support setting a version via cmake.")
-	endif()
-	
-	# Make a version file containing the current version from git.
-	include(GetGitRevisionDescription)
-	get_git_head_revision(STORM_VERSION_REFSPEC STORM_VERSION_GIT_HASH)
-
-	git_describe_checkout(STORM_GIT_VERSION_STRING)
-	# Parse the git Tag into variables
-	string(REGEX REPLACE "^([0-9]+)\\..*" "\\1" STORM_VERSION_MAJOR "${STORM_GIT_VERSION_STRING}")
-	string(REGEX REPLACE "^[0-9]+\\.([0-9]+).*" "\\1" STORM_VERSION_MINOR "${STORM_GIT_VERSION_STRING}")
-	string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.([0-9]+).*" "\\1" STORM_VERSION_PATCH "${STORM_GIT_VERSION_STRING}")
-	string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.[0-9]+\\-([0-9]+)\\-.*" "\\1" STORM_VERSION_COMMITS_AHEAD "${STORM_GIT_VERSION_STRING}")
-	string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.[0-9]+\\-[0-9]+\\-([a-z0-9]+).*" "\\1" STORM_VERSION_TAG_HASH "${STORM_GIT_VERSION_STRING}")
-	string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.[0-9]+\\-[0-9]+\\-[a-z0-9]+\\-(.*)" "\\1" STORM_VERSION_APPENDIX "${STORM_GIT_VERSION_STRING}")
 	if ("${STORM_VERSION_APPENDIX}" MATCHES "^.*dirty.*$")
-		set(STORM_VERSION_DIRTY 1)
-	else()
-		set(STORM_VERSION_DIRTY 0)
-	endif()
-	if (STORM_VERSION_DIRTY)
-		set(STORM_VERSION_DIRTY_STR "yes")
+		set(STORM_VERSION_DIRTY "true")
 	else()
-		set(STORM_VERSION_DIRTY_STR "no")
+		set(STORM_VERSION_DIRTY "false")
 	endif()
-	message(STATUS "storm - version is ${STORM_VERSION_MAJOR}.${STORM_VERSION_MINOR}.${STORM_VERSION_PATCH} (${STORM_VERSION_COMMITS_AHEAD} commits ahead of tag), building from git: ${STORM_VERSION_GIT_HASH} (dirty: ${STORM_VERSION_DIRTY_STR}).")
-
-	# proper type conversion so we can assign it to an optional
-	set(STORM_VERSION_GIT_HASH "std::string(\"${STORM_VERSION_GIT_HASH}\")")
+	message(STATUS "Storm - version is ${STORM_VERSION_MAJOR}.${STORM_VERSION_MINOR}.${STORM_VERSION_PATCH} (${STORM_VERSION_COMMITS_AHEAD} commits ahead of tag), building from git: ${STORM_VERSION_GIT_HASH} (dirty: ${STORM_VERSION_DIRTY}).")
 endif()
 
 # Configure a header file to pass some of the CMake settings to the source code
@@ -402,7 +388,7 @@ configure_file (
 	"${PROJECT_BINARY_DIR}/include/storm-config.h"
 )
 
-# Configure a source file to pass the storm version to the source code
+# Configure a source file to pass the Storm version to the source code
 configure_file (
 	"${PROJECT_SOURCE_DIR}/storm-version.cpp.in"
 	"${PROJECT_SOURCE_DIR}/src/storm/utility/storm-version.cpp"
diff --git a/src/storm/cli/cli.cpp b/src/storm/cli/cli.cpp
index efdb54d42..314afa700 100644
--- a/src/storm/cli/cli.cpp
+++ b/src/storm/cli/cli.cpp
@@ -93,7 +93,7 @@ namespace storm {
 #endif
 #ifdef STORM_HAVE_CARL
             // TODO get version string
-            STORM_PRINT("Linked with CARL." << std::endl);
+            STORM_PRINT("Linked with CArL." << std::endl);
 #endif
             
 #ifdef STORM_HAVE_CUDA
diff --git a/src/storm/utility/storm-version.h b/src/storm/utility/storm-version.h
index 2cd72c00b..24cf9a36f 100644
--- a/src/storm/utility/storm-version.h
+++ b/src/storm/utility/storm-version.h
@@ -19,13 +19,13 @@ namespace storm {
             const static unsigned versionPatch;
             
             /// The short hash of the git commit this build is based on
-            const static boost::optional<std::string> gitRevisionHash;
+            const static std::string gitRevisionHash;
             
             /// How many commits passed since the tag was last set.
-            const static boost::optional<unsigned> commitsAhead;
+            const static unsigned commitsAhead;
             
             /// 0 iff there no files were modified in the checkout, 1 otherwise.
-            const static boost::optional<unsigned> dirty;
+            const static boost::optional<bool> dirty;
             
             /// The system which has compiled Storm.
             const static std::string systemName;
@@ -48,14 +48,20 @@ namespace storm {
             static std::string longVersionString() {
                 std::stringstream sstream;
                 sstream << "Version " << versionMajor << "." <<  versionMinor << "." << versionPatch;
-                if (commitsAhead && commitsAhead.get() > 0) {
-                    sstream << " (+" << commitsAhead.get() << " commits)";
+                if (commitsAhead) {
+                    sstream << " (+ " << commitsAhead << " commits)";
                 }
-                if (gitRevisionHash) {
-                    sstream << " build from revision " << gitRevisionHash.get();
+                if (!gitRevisionHash.empty()) {
+                    sstream << " build from revision " << gitRevisionHash;
                 }
-                if (dirty && dirty.get() == 1) {
-                    sstream << " (dirty)";
+                if (dirty) {
+                    if (dirty.get()) {
+                        sstream << " (dirty)";
+                    } else {
+                        sstream << " (clean)";
+                    }
+                } else {
+                    sstream << " (potentially dirty)";
                 }
                 return sstream.str();
             }
diff --git a/storm-version.cpp.in b/storm-version.cpp.in
index 23a993169..61d9b4bc5 100644
--- a/storm-version.cpp.in
+++ b/storm-version.cpp.in
@@ -1,4 +1,4 @@
-//AUTO GENERATED -- DO NOT CHANGE 
+//AUTO GENERATED -- DO NOT CHANGE
 // TODO resolve issues when placing this in the build order directly.
 #include "storm/utility/storm-version.h"
 
@@ -8,9 +8,9 @@ namespace storm {
         const unsigned StormVersion::versionMajor = @STORM_VERSION_MAJOR@;
         const unsigned StormVersion::versionMinor = @STORM_VERSION_MINOR@;
         const unsigned StormVersion::versionPatch = @STORM_VERSION_PATCH@;
-        const boost::optional<std::string> StormVersion::gitRevisionHash = @STORM_VERSION_GIT_HASH@;
-        const boost::optional<unsigned> StormVersion::commitsAhead = @STORM_VERSION_COMMITS_AHEAD@;
-        const boost::optional<unsigned> StormVersion::dirty = @STORM_VERSION_DIRTY@;
+        const std::string StormVersion::gitRevisionHash = "@STORM_VERSION_GIT_HASH@";
+        const unsigned StormVersion::commitsAhead = @STORM_VERSION_COMMITS_AHEAD@;
+        const boost::optional<bool> StormVersion::dirty = @STORM_VERSION_DIRTY@;
         const std::string StormVersion::systemName = "@CMAKE_SYSTEM_NAME@";
         const std::string StormVersion::systemVersion = "@CMAKE_SYSTEM_VERSION@";
         const std::string StormVersion::cxxCompiler = "@STORM_COMPILER_ID@ @CMAKE_CXX_COMPILER_VERSION@";

From 97b33cf8b19e1f08f318fef47192fe4cde3971f0 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Sat, 11 Mar 2017 08:39:25 +0100
Subject: [PATCH 13/16] changed version output slightly

---
 src/storm/utility/storm-version.h | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/storm/utility/storm-version.h b/src/storm/utility/storm-version.h
index 24cf9a36f..cfe705304 100644
--- a/src/storm/utility/storm-version.h
+++ b/src/storm/utility/storm-version.h
@@ -24,7 +24,7 @@ namespace storm {
             /// How many commits passed since the tag was last set.
             const static unsigned commitsAhead;
             
-            /// 0 iff there no files were modified in the checkout, 1 otherwise.
+            /// 0 iff there no files were modified in the checkout, 1 otherwise. If none, no information about dirtyness is given.
             const static boost::optional<bool> dirty;
             
             /// The system which has compiled Storm.
@@ -53,6 +53,8 @@ namespace storm {
                 }
                 if (!gitRevisionHash.empty()) {
                     sstream << " build from revision " << gitRevisionHash;
+                } else {
+                    sstream << " built from archive";
                 }
                 if (dirty) {
                     if (dirty.get()) {

From 44dc3e7d8ddfe80dadfb2d5d967bef4f9a953477 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Sat, 11 Mar 2017 08:43:10 +0100
Subject: [PATCH 14/16] fixed version output in cmake

---
 CMakeLists.txt | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 294328776..57e94b8b8 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -371,8 +371,7 @@ if (STORM_VERSION_MAJOR STREQUAL "HEAD-HASH-NOTFOUND")
 	set(STORM_VERSION_COMMITS_AHEAD 0)
 	set(STORM_VERSION_DIRTY boost::none)
 
-	message(WARN "Storm - git version information not available.")
-	message(STATUS "Storm - version is ${STORM_VERSION_MAJOR}.${STORM_VERSION_MINOR}.${STORM_VERSION_PATCH}.")
+	message(WARNING "Storm - git version information not available, statically assuming version ${STORM_VERSION_MAJOR}.${STORM_VERSION_MINOR}.${STORM_VERSION_PATCH}.")
 else()
 	if ("${STORM_VERSION_APPENDIX}" MATCHES "^.*dirty.*$")
 		set(STORM_VERSION_DIRTY "true")

From ad1fdd41ea4121bccb9e2fb783f1468feab25a2e Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Sat, 11 Mar 2017 14:16:28 +0100
Subject: [PATCH 15/16] fixed some wrong capitalizations

---
 src/storm-dft-cli/storm-dyftee.cpp | 4 ++--
 src/storm-gspn-cli/storm-gspn.cpp  | 4 ++--
 src/storm-pgcl-cli/storm-pgcl.cpp  | 4 ++--
 src/storm/storm.cpp                | 4 ++--
 4 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/src/storm-dft-cli/storm-dyftee.cpp b/src/storm-dft-cli/storm-dyftee.cpp
index 4feb408a6..0f0aa68fa 100644
--- a/src/storm-dft-cli/storm-dyftee.cpp
+++ b/src/storm-dft-cli/storm-dyftee.cpp
@@ -251,10 +251,10 @@ int main(const int argc, const char** argv) {
         storm::utility::cleanUp();
         return 0;
     } catch (storm::exceptions::BaseException const& exception) {
-        STORM_LOG_ERROR("An exception caused storm-DyFTeE to terminate. The message of the exception is: " << exception.what());
+        STORM_LOG_ERROR("An exception caused Storm-DyFTeE to terminate. The message of the exception is: " << exception.what());
         return 1;
     } catch (std::exception const& exception) {
-        STORM_LOG_ERROR("An unexpected exception occurred and caused storm-DyFTeE to terminate. The message of this exception is: " << exception.what());
+        STORM_LOG_ERROR("An unexpected exception occurred and caused Storm-DyFTeE to terminate. The message of this exception is: " << exception.what());
         return 2;
     }
 }
diff --git a/src/storm-gspn-cli/storm-gspn.cpp b/src/storm-gspn-cli/storm-gspn.cpp
index e7e03b157..ff1723ff3 100644
--- a/src/storm-gspn-cli/storm-gspn.cpp
+++ b/src/storm-gspn-cli/storm-gspn.cpp
@@ -147,10 +147,10 @@ int main(const int argc, const char **argv) {
         storm::utility::cleanUp();
         return 0;
     } catch (storm::exceptions::BaseException const& exception) {
-        STORM_LOG_ERROR("An exception caused storm to terminate. The message of the exception is: " << exception.what());
+        STORM_LOG_ERROR("An exception caused Storm to terminate. The message of the exception is: " << exception.what());
         return 1;
     } catch (std::exception const& exception) {
-        STORM_LOG_ERROR("An unexpected exception occurred and caused storm to terminate. The message of this exception is: " << exception.what());
+        STORM_LOG_ERROR("An unexpected exception occurred and caused Storm to terminate. The message of this exception is: " << exception.what());
         return 2;
     }
 }
diff --git a/src/storm-pgcl-cli/storm-pgcl.cpp b/src/storm-pgcl-cli/storm-pgcl.cpp
index 4e4031ee4..6e0f03dca 100644
--- a/src/storm-pgcl-cli/storm-pgcl.cpp
+++ b/src/storm-pgcl-cli/storm-pgcl.cpp
@@ -93,10 +93,10 @@ int main(const int argc, const char** argv) {
             
         }
     }catch (storm::exceptions::BaseException const& exception) {
-        STORM_LOG_ERROR("An exception caused storm-PGCL to terminate. The message of the exception is: " << exception.what());
+        STORM_LOG_ERROR("An exception caused Storm-PGCL to terminate. The message of the exception is: " << exception.what());
         return 1;
     } catch (std::exception const& exception) {
-        STORM_LOG_ERROR("An unexpected exception occurred and caused storm-PGCL to terminate. The message of this exception is: " << exception.what());
+        STORM_LOG_ERROR("An unexpected exception occurred and caused Storm-PGCL to terminate. The message of this exception is: " << exception.what());
         return 2;
     }
 }
diff --git a/src/storm/storm.cpp b/src/storm/storm.cpp
index c21be38a0..20126f488 100644
--- a/src/storm/storm.cpp
+++ b/src/storm/storm.cpp
@@ -36,10 +36,10 @@ int main(const int argc, const char** argv) {
         }
         return 0;
     } catch (storm::exceptions::BaseException const& exception) {
-        STORM_LOG_ERROR("An exception caused storm to terminate. The message of the exception is: " << exception.what());
+        STORM_LOG_ERROR("An exception caused Storm to terminate. The message of the exception is: " << exception.what());
         return 1;
     } catch (std::exception const& exception) {
-        STORM_LOG_ERROR("An unexpected exception occurred and caused storm to terminate. The message of this exception is: " << exception.what());
+        STORM_LOG_ERROR("An unexpected exception occurred and caused Storm to terminate. The message of this exception is: " << exception.what());
         return 2;
     }
 }

From b7170b3c3b29962198d56f8cd5df4f6eda6ed7ca Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Mon, 13 Mar 2017 15:01:48 +0100
Subject: [PATCH 16/16] fixed two issues pointed out by Joachim Klein: spirit
 error message (superfluous tab) and wrong treatment of strict upper bounds in
 bounded until and cumulative reward properties

---
 src/storm/logic/BoundedUntilFormula.cpp        | 18 ++++++++++++++++++
 src/storm/logic/BoundedUntilFormula.h          |  3 +++
 src/storm/logic/CumulativeRewardFormula.cpp    | 18 ++++++++++++++++++
 src/storm/logic/CumulativeRewardFormula.h      |  3 +++
 .../csl/HybridCtmcCslModelChecker.cpp          |  4 ++--
 .../csl/SparseCtmcCslModelChecker.cpp          |  4 ++--
 .../SparseMarkovAutomatonCslModelChecker.cpp   |  2 +-
 .../prctl/HybridDtmcPrctlModelChecker.cpp      |  4 ++--
 .../prctl/HybridMdpPrctlModelChecker.cpp       |  4 ++--
 .../prctl/SparseDtmcPrctlModelChecker.cpp      |  4 ++--
 .../prctl/SparseMdpPrctlModelChecker.cpp       |  4 ++--
 .../prctl/SymbolicDtmcPrctlModelChecker.cpp    |  4 ++--
 .../prctl/SymbolicMdpPrctlModelChecker.cpp     |  4 ++--
 src/storm/parser/SpiritErrorHandler.h          |  2 +-
 14 files changed, 60 insertions(+), 18 deletions(-)

diff --git a/src/storm/logic/BoundedUntilFormula.cpp b/src/storm/logic/BoundedUntilFormula.cpp
index 67ece142a..da7ac1862 100644
--- a/src/storm/logic/BoundedUntilFormula.cpp
+++ b/src/storm/logic/BoundedUntilFormula.cpp
@@ -102,6 +102,24 @@ namespace storm {
             return static_cast<uint64_t>(bound);
         }
         
+        template <>
+        double BoundedUntilFormula::getNonStrictUpperBound() const {
+            double bound = getUpperBound<double>();
+            STORM_LOG_THROW(bound > 0, storm::exceptions::InvalidPropertyException, "Cannot retrieve non-strict bound from strict zero-bound.");
+            return bound;
+        }
+
+        template <>
+        uint64_t BoundedUntilFormula::getNonStrictUpperBound() const {
+            int_fast64_t bound = getUpperBound<uint64_t>();
+            if (isUpperBoundStrict()) {
+                STORM_LOG_THROW(bound > 0, storm::exceptions::InvalidPropertyException, "Cannot retrieve non-strict bound from strict zero-bound.");
+                return bound - 1;
+            } else {
+                return bound;
+            }
+        }
+        
         void BoundedUntilFormula::checkNoVariablesInBound(storm::expressions::Expression const& bound) {
             STORM_LOG_THROW(!bound.containsVariables(), storm::exceptions::InvalidOperationException, "Cannot evaluate time-bound '" << bound << "' as it contains undefined constants.");
         }
diff --git a/src/storm/logic/BoundedUntilFormula.h b/src/storm/logic/BoundedUntilFormula.h
index 862871796..5dc2a3889 100644
--- a/src/storm/logic/BoundedUntilFormula.h
+++ b/src/storm/logic/BoundedUntilFormula.h
@@ -40,6 +40,9 @@ namespace storm {
 
             template <typename ValueType>
             ValueType getUpperBound() const;
+            
+            template <typename ValueType>
+            ValueType getNonStrictUpperBound() const;
 
             virtual std::ostream& writeToStream(std::ostream& out) const override;
             
diff --git a/src/storm/logic/CumulativeRewardFormula.cpp b/src/storm/logic/CumulativeRewardFormula.cpp
index 05bf0353b..36c82856c 100644
--- a/src/storm/logic/CumulativeRewardFormula.cpp
+++ b/src/storm/logic/CumulativeRewardFormula.cpp
@@ -64,6 +64,24 @@ namespace storm {
             return value;
         }
         
+        template <>
+        double CumulativeRewardFormula::getNonStrictBound() const {
+            double bound = getBound<double>();
+            STORM_LOG_THROW(bound > 0, storm::exceptions::InvalidPropertyException, "Cannot retrieve non-strict bound from strict zero-bound.");
+            return bound;
+        }
+        
+        template <>
+        uint64_t CumulativeRewardFormula::getNonStrictBound() const {
+            int_fast64_t bound = getBound<uint64_t>();
+            if (isBoundStrict()) {
+                STORM_LOG_THROW(bound > 0, storm::exceptions::InvalidPropertyException, "Cannot retrieve non-strict bound from strict zero-bound.");
+                return bound - 1;
+            } else {
+                return bound;
+            }
+        }
+        
         void CumulativeRewardFormula::checkNoVariablesInBound(storm::expressions::Expression const& bound) {
             STORM_LOG_THROW(!bound.containsVariables(), storm::exceptions::InvalidOperationException, "Cannot evaluate time-bound '" << bound << "' as it contains undefined constants.");
         }
diff --git a/src/storm/logic/CumulativeRewardFormula.h b/src/storm/logic/CumulativeRewardFormula.h
index ad9d5e3c0..fce825271 100644
--- a/src/storm/logic/CumulativeRewardFormula.h
+++ b/src/storm/logic/CumulativeRewardFormula.h
@@ -35,6 +35,9 @@ namespace storm {
             template <typename ValueType>
             ValueType getBound() const;
             
+            template <typename ValueType>
+            ValueType getNonStrictBound() const;
+            
         private:
             static void checkNoVariablesInBound(storm::expressions::Expression const& bound);
 
diff --git a/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp b/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp
index fc221147b..f59273480 100644
--- a/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp
+++ b/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp
@@ -77,7 +77,7 @@ namespace storm {
                 lowerBound = pathFormula.getLowerBound<double>();
             }
             if (pathFormula.hasUpperBound()) {
-                upperBound = pathFormula.getUpperBound<double>();
+                upperBound = pathFormula.getNonStrictUpperBound<double>();
             } else {
                 upperBound = storm::utility::infinity<double>();
             }
@@ -98,7 +98,7 @@ namespace storm {
             storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula();
 
             STORM_LOG_THROW(!rewardPathFormula.isStepBounded(), storm::exceptions::NotImplementedException, "Currently step-bounded properties on CTMCs are not supported.");
-            return storm::modelchecker::helper::HybridCtmcCslHelper<DdType, ValueType>::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound<double>(), *linearEquationSolverFactory);
+            return storm::modelchecker::helper::HybridCtmcCslHelper<DdType, ValueType>::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getNonStrictBound<double>(), *linearEquationSolverFactory);
         }
         
         template<typename ModelType>
diff --git a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp
index 4d6e9407f..1f5c9ee0d 100644
--- a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp
+++ b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp
@@ -67,7 +67,7 @@ namespace storm {
                 lowerBound = pathFormula.getLowerBound<double>();
             }
             if (pathFormula.hasUpperBound()) {
-                upperBound = pathFormula.getUpperBound<double>();
+                upperBound = pathFormula.getNonStrictUpperBound<double>();
             } else {
                 upperBound = storm::utility::infinity<double>();
             }
@@ -108,7 +108,7 @@ namespace storm {
         std::unique_ptr<CheckResult> SparseCtmcCslModelChecker<SparseCtmcModelType>::computeCumulativeRewards(storm::logic::RewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula, ValueType> const& checkTask) {
             storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula();
             STORM_LOG_THROW(!rewardPathFormula.isStepBounded(), storm::exceptions::NotImplementedException, "Currently step-bounded properties on CTMCs are not supported.");
-            std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeCumulativeRewards(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound<double>(), *linearEquationSolverFactory);
+            std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeCumulativeRewards(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getNonStrictBound<double>(), *linearEquationSolverFactory);
             return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
         }
                 
diff --git a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp
index 4aef07d8d..03789fe53 100644
--- a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp
+++ b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp
@@ -61,7 +61,7 @@ namespace storm {
                 lowerBound = pathFormula.getLowerBound<double>();
             }
             if (pathFormula.hasUpperBound()) {
-                upperBound = pathFormula.getUpperBound<double>();
+                upperBound = pathFormula.getNonStrictUpperBound<double>();
             } else {
                 upperBound = storm::utility::infinity<double>();
             }
diff --git a/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp
index 1936e60bd..ebbb34e99 100644
--- a/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp
+++ b/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp
@@ -76,14 +76,14 @@ namespace storm {
             std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
             SymbolicQualitativeCheckResult<DdType> const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult<DdType>();
             SymbolicQualitativeCheckResult<DdType> const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult<DdType>();
-            return storm::modelchecker::helper::HybridDtmcPrctlHelper<DdType, ValueType>::computeBoundedUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound<uint64_t>() + (pathFormula.isUpperBoundStrict() ? 1ull : 0ull), *this->linearEquationSolverFactory);
+            return storm::modelchecker::helper::HybridDtmcPrctlHelper<DdType, ValueType>::computeBoundedUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getNonStrictUpperBound<uint64_t>(), *this->linearEquationSolverFactory);
         }
                 
         template<typename ModelType>
         std::unique_ptr<CheckResult> HybridDtmcPrctlModelChecker<ModelType>::computeCumulativeRewards(storm::logic::RewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula, ValueType> const& checkTask) {
             storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula();
             STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound.");
-            return storm::modelchecker::helper::HybridDtmcPrctlHelper<DdType, ValueType>::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound<uint64_t>() + (rewardPathFormula.isBoundStrict() ? 1ull : 0ull), *this->linearEquationSolverFactory);
+            return storm::modelchecker::helper::HybridDtmcPrctlHelper<DdType, ValueType>::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getNonStrictBound<uint64_t>(), *this->linearEquationSolverFactory);
         }
                 
         template<typename ModelType>
diff --git a/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp
index d42de45dd..ff1785db4 100644
--- a/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp
+++ b/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp
@@ -95,7 +95,7 @@ namespace storm {
             std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
             SymbolicQualitativeCheckResult<DdType> const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult<DdType>();
             SymbolicQualitativeCheckResult<DdType> const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult<DdType>();
-            return storm::modelchecker::helper::HybridMdpPrctlHelper<DdType, ValueType>::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound<uint64_t>() + (pathFormula.isUpperBoundStrict() ? 1ull : 0ull), *this->linearEquationSolverFactory);
+            return storm::modelchecker::helper::HybridMdpPrctlHelper<DdType, ValueType>::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getNonStrictUpperBound<uint64_t>(), *this->linearEquationSolverFactory);
         }
         
         template<typename ModelType>
@@ -103,7 +103,7 @@ namespace storm {
             storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula();
             STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
             STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound.");
-            return storm::modelchecker::helper::HybridMdpPrctlHelper<DdType, ValueType>::computeCumulativeRewards(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound<uint64_t>() + (rewardPathFormula.isBoundStrict() ? 1ull : 0ll), *this->linearEquationSolverFactory);
+            return storm::modelchecker::helper::HybridMdpPrctlHelper<DdType, ValueType>::computeCumulativeRewards(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getNonStrictBound<uint64_t>(), *this->linearEquationSolverFactory);
         }
                 
         template<typename ModelType>
diff --git a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
index 5bbf6cf23..229af5a8a 100644
--- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
+++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
@@ -48,7 +48,7 @@ namespace storm {
             std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
             ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult();
             ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult();
-            std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeBoundedUntilProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound<uint64_t>() + (pathFormula.isUpperBoundStrict() ? 1ull : 0ull), *linearEquationSolverFactory);
+            std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeBoundedUntilProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getNonStrictUpperBound<uint64_t>(), *linearEquationSolverFactory);
             std::unique_ptr<CheckResult> result = std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
             return result;
         }
@@ -86,7 +86,7 @@ namespace storm {
         std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeCumulativeRewards(storm::logic::RewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula, ValueType> const& checkTask) {
             storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula();
             STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound.");
-            std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeCumulativeRewards(this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound<uint64_t>() + (rewardPathFormula.isBoundStrict() ? 1ull : 0ull), *linearEquationSolverFactory);
+            std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeCumulativeRewards(this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getNonStrictBound<uint64_t>(), *linearEquationSolverFactory);
             return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
         }
         
diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
index 2a7f6d725..55f9c1fc6 100644
--- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
+++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
@@ -64,7 +64,7 @@ namespace storm {
             std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
             ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult();
             ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult();
-            std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound<uint64_t>() + (pathFormula.isUpperBoundStrict() ? 1ull : 0ull), *minMaxLinearEquationSolverFactory);
+            std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getNonStrictUpperBound<uint64_t>(), *minMaxLinearEquationSolverFactory);
             return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
         }
         
@@ -125,7 +125,7 @@ namespace storm {
             storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula();
             STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
             STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound.");
-            std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeCumulativeRewards(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound<uint64_t>() + (rewardPathFormula.isBoundStrict() ? 1ull : 0ull), *minMaxLinearEquationSolverFactory);
+            std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeCumulativeRewards(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getNonStrictBound<uint64_t>(), *minMaxLinearEquationSolverFactory);
             return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
         }
         
diff --git a/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp
index c52307315..b7d163f62 100644
--- a/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp
+++ b/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp
@@ -76,7 +76,7 @@ namespace storm {
             std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
             SymbolicQualitativeCheckResult<DdType> const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult<DdType>();
             SymbolicQualitativeCheckResult<DdType> const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult<DdType>();
-            storm::dd::Add<DdType> numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper<DdType, ValueType>::computeBoundedUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound<uint64_t>() + (pathFormula.isUpperBoundStrict() ? 1ull : 0ull), *this->linearEquationSolverFactory);
+            storm::dd::Add<DdType> numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper<DdType, ValueType>::computeBoundedUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getNonStrictUpperBound<uint64_t>(), *this->linearEquationSolverFactory);
             return std::unique_ptr<SymbolicQuantitativeCheckResult<DdType>>(new SymbolicQuantitativeCheckResult<DdType>(this->getModel().getReachableStates(), numericResult));
         }
         
@@ -84,7 +84,7 @@ namespace storm {
         std::unique_ptr<CheckResult> SymbolicDtmcPrctlModelChecker<ModelType>::computeCumulativeRewards(storm::logic::RewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula, ValueType> const& checkTask) {
             storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula();
             STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound.");
-            storm::dd::Add<DdType> numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper<DdType, ValueType>::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound<uint64_t>() + (rewardPathFormula.isBoundStrict() ? 1ull : 0ull), *this->linearEquationSolverFactory);
+            storm::dd::Add<DdType> numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper<DdType, ValueType>::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getNonStrictBound<uint64_t>(), *this->linearEquationSolverFactory);
             return std::unique_ptr<SymbolicQuantitativeCheckResult<DdType>>(new SymbolicQuantitativeCheckResult<DdType>(this->getModel().getReachableStates(), numericResult));
         }
         
diff --git a/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp
index 2ac26509a..e077fbb26 100644
--- a/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp
+++ b/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp
@@ -76,7 +76,7 @@ namespace storm {
             std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
             SymbolicQualitativeCheckResult<DdType> const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult<DdType>();
             SymbolicQualitativeCheckResult<DdType> const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult<DdType>();
-            return storm::modelchecker::helper::SymbolicMdpPrctlHelper<DdType, ValueType>::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound<uint64_t>() + (pathFormula.isUpperBoundStrict() ? 1ull : 0ull), *this->linearEquationSolverFactory);
+            return storm::modelchecker::helper::SymbolicMdpPrctlHelper<DdType, ValueType>::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getNonStrictUpperBound<uint64_t>(), *this->linearEquationSolverFactory);
         }
         
         template<typename ModelType>
@@ -84,7 +84,7 @@ namespace storm {
             storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula();
             STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
             STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound.");
-            return storm::modelchecker::helper::SymbolicMdpPrctlHelper<DdType, ValueType>::computeCumulativeRewards(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound<uint64_t>() + (rewardPathFormula.isBoundStrict() ? 1ull : 0ull), *this->linearEquationSolverFactory);
+            return storm::modelchecker::helper::SymbolicMdpPrctlHelper<DdType, ValueType>::computeCumulativeRewards(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getNonStrictBound<uint64_t>(), *this->linearEquationSolverFactory);
         }
         
         template<typename ModelType>
diff --git a/src/storm/parser/SpiritErrorHandler.h b/src/storm/parser/SpiritErrorHandler.h
index 53a73c9e3..34280e422 100644
--- a/src/storm/parser/SpiritErrorHandler.h
+++ b/src/storm/parser/SpiritErrorHandler.h
@@ -19,7 +19,7 @@ namespace storm {
                 
                 std::stringstream stream;
                 stream << "Parsing error at " << get_line(where) << ":" << boost::spirit::get_column(lineStart, where) << ": " << " expecting " << what << ", here:" << std::endl;
-                stream << "\t" << line << std::endl << "\t";
+                stream << "\t" << line << std::endl;
                 auto caretColumn = boost::spirit::get_column(lineStart, where);
                 stream << "\t" << std::string(caretColumn - 1, ' ') << "^" << std::endl;