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)
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/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);
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]);
diff --git a/src/storm/solver/Z3LpSolver.cpp b/src/storm/solver/Z3LpSolver.cpp
index 95b061f70..45ffbd7be 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));
}
@@ -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.";
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);
}