merge

Former-commit-id: 7ab67684c1

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)

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

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

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

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.

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.

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

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

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

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

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