Merge branch 'master' into dft_case_study

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)

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;

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);

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]);

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));
         }
         
@@ -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.";

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"

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);
 }