diff --git a/CMakeLists.txt b/CMakeLists.txt
index a1b8c29b3..c0179e39d 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -114,8 +114,10 @@ if(CMAKE_COMPILER_IS_GNUCC)
set(STORM_COMPILED_BY "GCC")
# Set standard flags for GCC
set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -funroll-loops")
+ set(CMAKE_C_FLAGS_RELEASE "${CMAKE_C_FLAGS_RELEASE} -funroll-loops")
add_definitions(-DBOOST_RESULT_OF_USE_DECLTYPE)
- set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++11 -Wall -pedantic")
+ set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++11 -Wall -pedantic -Wno-deprecated-declarations")
+ set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wall -pedantic -Wno-deprecated-declarations")
# Turn on popcnt instruction if desired (yes by default)
if (STORM_USE_POPCNT)
@@ -123,7 +125,7 @@ if(CMAKE_COMPILER_IS_GNUCC)
endif(STORM_USE_POPCNT)
# Set the no-strict-aliasing target for GCC
- set_source_files_properties(${CONVERSIONHELPER_TARGET} PROPERTIES COMPILE_FLAGS " -fno-strict-aliasing ")
+ set_source_files_properties(${CONVERSIONHELPER_TARGET} PROPERTIES COMPILE_FLAGS " -fno-strict-aliasing")
elseif(MSVC)
set(STORM_COMPILED_BY "MSVC")
# required for GMM to compile, ugly error directive in their code
@@ -146,7 +148,7 @@ else(CLANG)
# As CLANG is not set as a variable, we need to set it in case we have not matched another compiler.
set (CLANG ON)
# Set standard flags for clang
- set (CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -funroll-loops -O3")
+ set (CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -funroll-loops -O4")
if(UNIX AND NOT APPLE AND NOT USE_LIBCXX)
set(CLANG_STDLIB libstdc++)
message(STATUS "StoRM - Linking against libstdc++")
@@ -162,6 +164,7 @@ else(CLANG)
add_definitions(-DBOOST_RESULT_OF_USE_DECLTYPE)
set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++11 -stdlib=${CLANG_STDLIB} -Wall -pedantic -Wno-unused-variable -ftemplate-depth=1024")
+ set (CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wall -pedantic")
# Turn on popcnt instruction if desired (yes by default)
if (STORM_USE_POPCNT)
diff --git a/resources/3rdparty/cudd-2.5.0/CMakeLists.txt b/resources/3rdparty/cudd-2.5.0/CMakeLists.txt
index 4d08513de..c9f821a21 100644
--- a/resources/3rdparty/cudd-2.5.0/CMakeLists.txt
+++ b/resources/3rdparty/cudd-2.5.0/CMakeLists.txt
@@ -20,9 +20,13 @@ include_directories("${PROJECT_SOURCE_DIR}/src/nanotrav")
include_directories("${PROJECT_SOURCE_DIR}/src/st")
include_directories("${PROJECT_SOURCE_DIR}/src/util")
-if(MSVC)
+if(CMAKE_COMPILER_IS_GNUCC)
+ set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wno-unused-variable -Wno-unused-but-set-variable -Wno-unused-function")
+elseif(MSVC)
# required for GMM to compile, ugly error directive in their code
add_definitions(/D_SCL_SECURE_NO_DEPRECATE /D_CRT_SECURE_NO_WARNINGS)
+else(CLANG)
+ set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wno-unused-variable -Wno-unused-but-set-variable -Wno-unused-function")
endif()
# Since we do not target Alphas, this symbol is always set
diff --git a/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.cc b/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.cc
index 3262108aa..b8f7d3983 100644
--- a/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.cc
+++ b/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.cc
@@ -2815,7 +2815,7 @@ Cudd::Walsh(
size_t n = x.size();
DdNode **X = new DdNode *[n];
DdNode **Y = new DdNode *[n];
- for (int i = 0; i < n; i++) {
+ for (size_t i = 0; i < n; i++) {
X[i] = x[i].getNode();
Y[i] = y[i].getNode();
}
@@ -3612,7 +3612,7 @@ ADD::SwapVariables(
DdManager *mgr = p->manager;
DdNode **X = new DdNode *[n];
DdNode **Y = new DdNode *[n];
- for (int i = 0; i < n; i++) {
+ for (size_t i = 0; i < n; i++) {
X[i] = x[i].node;
Y[i] = y[i].node;
}
@@ -3646,7 +3646,7 @@ BDD::SwapVariables(
DdManager *mgr = p->manager;
DdNode **X = new DdNode *[n];
DdNode **Y = new DdNode *[n];
- for (int i = 0; i < n; i++) {
+ for (size_t i = 0; i < n; i++) {
X[i] = x[i].node;
Y[i] = y[i].node;
}
@@ -3666,7 +3666,7 @@ BDD::AdjPermuteX(
size_t n = x.size();
DdManager *mgr = p->manager;
DdNode **X = new DdNode *[n];
- for (int i = 0; i < n; i++) {
+ for (size_t i = 0; i < n; i++) {
X[i] = x[i].node;
}
DdNode *result = Cudd_bddAdjPermuteX(mgr, node, X, static_cast<int>(n));
diff --git a/resources/3rdparty/glpk-4.53/CMakeLists.txt b/resources/3rdparty/glpk-4.53/CMakeLists.txt
index b09ec9e1c..24ee34121 100644
--- a/resources/3rdparty/glpk-4.53/CMakeLists.txt
+++ b/resources/3rdparty/glpk-4.53/CMakeLists.txt
@@ -53,7 +53,7 @@ message(STATUS "GLPK - CMAKE_BUILD_TYPE (ENV): $ENV{CMAKE_BUILD_TYPE}")
if(CMAKE_COMPILER_IS_GNUCC)
message(STATUS "GLPK - Using Compiler Configuration: GCC")
# Set standard flags for GCC
- set(CMAKE_C_FLAGS "${CMAKE_CXX_FLAGS} -Wno-return-type")
+ set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wno-return-type -Wno-parentheses -Wno-unused-variable -Wno-unused-but-set-variable -Wno-unused-value -Wno-unused-function -Wno-address -Wno-unused-label")
add_definitions(-DHAVE_CONFIG_H=1)
elseif(MSVC)
message(STATUS "GLPK - Using Compiler Configuration: MSVC")
diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
index 518d21972..adf65d728 100644
--- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
+++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
@@ -343,7 +343,6 @@ namespace storm {
// Get some data members for convenience.
typename storm::storage::SparseMatrix<ValueType> const& transitionMatrix = this->getModel().getTransitionMatrix();
std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = this->getModel().getNondeterministicChoiceIndices();
- ValueType one = storm::utility::one<ValueType>();
ValueType zero = storm::utility::zero<ValueType>();
//first calculate LRA for the Maximal End Components.
diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
index e4087ad52..498370e02 100644
--- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
+++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
@@ -692,23 +692,10 @@ namespace storm {
return maximalDepth;
}
- namespace {
- static int chunkCounter = 0;
- static int counter = 0;
- }
-
template<typename ValueType>
void SparseDtmcEliminationModelChecker<ValueType>::eliminateState(FlexibleSparseMatrix& matrix, std::vector<ValueType>& oneStepProbabilities, uint_fast64_t state, FlexibleSparseMatrix& backwardTransitions, boost::optional<std::vector<ValueType>>& stateRewards, bool removeForwardTransitions, bool constrained, storm::storage::BitVector const& predecessorConstraint) {
auto eliminationStart = std::chrono::high_resolution_clock::now();
- ++counter;
- STORM_LOG_TRACE("Eliminating state " << state << ".");
- if (counter > matrix.getNumberOfRows() / 10) {
- ++chunkCounter;
- STORM_LOG_INFO("Eliminated " << (chunkCounter * 10) << "% of the states." << std::endl);
- counter = 0;
- }
-
bool hasSelfLoop = false;
ValueType loopProbability = storm::utility::zero<ValueType>();
@@ -752,7 +739,6 @@ namespace storm {
// Now connect the predecessors of the state being eliminated with its successors.
typename FlexibleSparseMatrix::row_type& currentStatePredecessors = backwardTransitions.getRow(state);
- std::size_t numberOfPredecessors = currentStatePredecessors.size();
std::size_t predecessorForwardTransitionCount = 0;
// In case we have a constrained elimination, we need to keep track of the new predecessors.
diff --git a/src/parser/AutoParser.cpp b/src/parser/AutoParser.cpp
index 23764fd61..065ad4327 100644
--- a/src/parser/AutoParser.cpp
+++ b/src/parser/AutoParser.cpp
@@ -69,7 +69,7 @@ namespace storm {
#ifdef WINDOWS
sscanf_s(filehintBuffer, formatString.c_str(), hint, STORM_PARSER_AUTOPARSER_HINT_LENGTH + 1);
#else
- int ret = sscanf(filehintBuffer, formatString.c_str(), hint);
+ sscanf(filehintBuffer, formatString.c_str(), hint);
#endif
for (char* c = hint; *c != '\0'; c++) *c = toupper(*c);
diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp
index bff8c71b8..ddb348249 100644
--- a/src/parser/PrismParser.cpp
+++ b/src/parser/PrismParser.cpp
@@ -378,7 +378,8 @@ namespace storm {
if (!actionName.empty()) {
auto const& nameIndexPair = globalProgramInformation.actionIndices.find(actionName);
if (nameIndexPair == globalProgramInformation.actionIndices.end()) {
- globalProgramInformation.actionIndices[actionName] = globalProgramInformation.actionIndices.size();
+ std::size_t nextIndex = globalProgramInformation.actionIndices.size();
+ globalProgramInformation.actionIndices[actionName] = nextIndex;
}
}
@@ -392,7 +393,8 @@ namespace storm {
// Register the action name if it has not appeared earlier.
auto const& nameIndexPair = globalProgramInformation.actionIndices.find(actionName);
if (nameIndexPair == globalProgramInformation.actionIndices.end()) {
- globalProgramInformation.actionIndices[actionName] = globalProgramInformation.actionIndices.size();
+ std::size_t nextIndex = globalProgramInformation.actionIndices.size();
+ globalProgramInformation.actionIndices[actionName] = nextIndex;
}
}
@@ -518,7 +520,8 @@ namespace storm {
if (!newActionName.empty()) {
auto const& nameIndexPair = globalProgramInformation.actionIndices.find(newActionName);
if (nameIndexPair == globalProgramInformation.actionIndices.end()) {
- globalProgramInformation.actionIndices[newActionName] = globalProgramInformation.actionIndices.size();
+ std::size_t nextIndex = globalProgramInformation.actionIndices.size();
+ globalProgramInformation.actionIndices[newActionName] = nextIndex;
}
}
diff --git a/src/storage/dd/CuddAdd.cpp b/src/storage/dd/CuddAdd.cpp
index 5eaded696..dbee2e94a 100644
--- a/src/storage/dd/CuddAdd.cpp
+++ b/src/storage/dd/CuddAdd.cpp
@@ -1,5 +1,6 @@
#include <cstring>
#include <algorithm>
+#include <boost/algorithm/string/join.hpp>
#include "src/storage/dd/CuddAdd.h"
#include "src/storage/dd/CuddBdd.h"
@@ -1055,7 +1056,12 @@ namespace storm {
}
std::ostream& operator<<(std::ostream& out, const Add<DdType::CUDD>& add) {
- add.exportToDot();
+ out << "ADD with " << add.getNonZeroCount() << " nnz, " << add.getNodeCount() << " nodes, " << add.getLeafCount() << " leaves" << std::endl;
+ std::vector<std::string> variableNames;
+ for (auto const& variable : add.getContainedMetaVariables()) {
+ variableNames.push_back(variable.getName());
+ }
+ out << "contained variables: " << boost::algorithm::join(variableNames, ", ") << std::endl;
return out;
}
diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp
index 3792bea94..4a595181f 100644
--- a/src/storage/prism/Program.cpp
+++ b/src/storage/prism/Program.cpp
@@ -12,6 +12,7 @@
namespace storm {
namespace prism {
+<<<<<<< HEAD
Program::Program(std::shared_ptr<storm::expressions::ExpressionManager> manager, ModelType modelType, std::vector<Constant> const& constants, std::vector<BooleanVariable> const& globalBooleanVariables, std::vector<IntegerVariable> const& globalIntegerVariables, std::vector<Formula> const& formulas, std::vector<Module> const& modules, std::map<std::string, uint_fast64_t> const& actionToIndexMap, std::vector<RewardModel> const& rewardModels, bool fixInitialConstruct, storm::prism::InitialConstruct const& initialConstruct, std::vector<Label> const& labels, std::string const& filename, uint_fast64_t lineNumber, bool finalModel)
: LocatedInformation(filename, lineNumber), manager(manager),
modelType(modelType), constants(constants), constantToIndexMap(),
@@ -22,8 +23,10 @@ namespace storm {
labels(labels), actionToIndexMap(actionToIndexMap), indexToActionMap(), actions(),
actionIndices(), actionIndicesToModuleIndexMap(), variableToModuleIndexMap()
{
+
+ // Start by creating the necessary mappings from the given ones.
this->createMappings();
-
+
// Create a new initial construct if the corresponding flag was set.
if (fixInitialConstruct) {
storm::expressions::Expression newInitialExpression = manager->boolean(true);
diff --git a/test/functional/builder/DdPrismModelBuilderTest.cpp b/test/functional/builder/DdPrismModelBuilderTest.cpp
index ea88d24f1..db6adc88f 100644
--- a/test/functional/builder/DdPrismModelBuilderTest.cpp
+++ b/test/functional/builder/DdPrismModelBuilderTest.cpp
@@ -72,7 +72,7 @@ TEST(DdPrismModelBuilderTest, Mdp) {
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
std::shared_ptr<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>> mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
-
+
EXPECT_EQ(169, mdp->getNumberOfStates());
EXPECT_EQ(436, mdp->getNumberOfTransitions());
EXPECT_EQ(254, mdp->getNumberOfChoices());