Merge branch 'master' of https://srv-i2.informatik.rwth-aachen.de/scm/git/storm

CMakeLists.txt

@@ -190,6 +190,10 @@ elseif ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "AppleClang")
 	# using AppleClang
 	if (CMAKE_CXX_COMPILER_VERSION VERSION_LESS 7.3)
 		message(FATAL_ERROR "AppleClang version must be at least 7.3.")
+	elseif ((CMAKE_CXX_COMPILER_VERSION VERSION_EQUAL 11.0) OR (CMAKE_CXX_COMPILER_VERSION VERSION_GREATER 11.0))
+		message(WARNING "Temporarily disabling stack checks for AppleClang 11.0 or higher.")
+		# TODO: In release mode, stack checks currently fail at runtime. Might be a compiler bug as there does not seem to be faulty behavior. 
+		set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -fno-stack-check")
 	endif()
 
 	set(STORM_COMPILER_APPLECLANG ON)

resources/3rdparty/CMakeLists.txt

@@ -390,7 +390,9 @@ get_filename_component(GMPXX_LIB_LOCATION ${GMPXX_LIB} DIRECTORY)
 ##
 #############################################################
 
-get_target_property(CLN_INCLUDE_DIR CLN_SHARED INTERFACE_INCLUDE_DIRECTORIES)
+if(STORM_USE_CLN_RF OR STORM_USE_CLN_EA)
+	get_target_property(CLN_INCLUDE_DIR CLN_SHARED INTERFACE_INCLUDE_DIRECTORIES)
+endif()
 
 #############################################################
 ##

src/storm-parsers/parser/ExpressionParser.h

@@ -49,8 +49,8 @@ namespace storm {
             ExpressionParser(storm::expressions::ExpressionManager const& manager, qi::symbols<char, uint_fast64_t> const& invalidIdentifiers_ = qi::symbols<char, uint_fast64_t>(), bool enableErrorHandling = true, bool allowBacktracking = false);
             ~ExpressionParser();
             
-            ExpressionParser(ExpressionParser const& other) = default;
-            ExpressionParser& operator=(ExpressionParser const& other) = default;
+            ExpressionParser(ExpressionParser const& other) = delete;
+            ExpressionParser& operator=(ExpressionParser const& other) = delete;
             
             /*!
              * Sets an identifier mapping that is used to determine valid variables in the expression. The mapped-to

src/storm-parsers/parser/FormulaParserGrammar.h

@@ -25,8 +25,8 @@ namespace storm {
             FormulaParserGrammar(std::shared_ptr<storm::expressions::ExpressionManager const> const& manager);
             FormulaParserGrammar(std::shared_ptr<storm::expressions::ExpressionManager> const& manager);
             
-            FormulaParserGrammar(FormulaParserGrammar const& other) = default;
-            FormulaParserGrammar& operator=(FormulaParserGrammar const& other) = default;
+            FormulaParserGrammar(FormulaParserGrammar const& other) = delete;
+            FormulaParserGrammar& operator=(FormulaParserGrammar const& other) = delete;
             
             /*!
              * Adds an identifier and the expression it is supposed to be replaced with. This can, for example be used

src/storm-pomdp/transformer/BinaryPomdpTransformer.cpp

@@ -83,7 +83,7 @@ namespace storm {
             storm::storage::SparseMatrixBuilder<ValueType> builder(0,0,0,true,true);
             uint64_t currRow = 0;
             std::vector<uint64_t> origRowToSimpleRowMap(pomdp.getNumberOfChoices(), std::numeric_limits<uint64_t>::max());
-            uint64 currAuxState = queue.size();
+            uint64_t currAuxState = queue.size();
             while (!queue.empty()) {
                 auto group = std::move(queue.front());
                 queue.pop();

src/storm/builder/ExplicitModelBuilder.cpp

@@ -349,7 +349,7 @@ namespace storm {
                         bool foundActionSet = false;
                         std::vector<std::string> actionNames;
                         bool addedAnonymousAction = false;
-                        for (uint64 choice = modelComponents.transitionMatrix.getRowGroupIndices()[bitVectorIndexPair.second];
+                        for (uint64_t choice = modelComponents.transitionMatrix.getRowGroupIndices()[bitVectorIndexPair.second];
                              choice < modelComponents.transitionMatrix.getRowGroupIndices()[bitVectorIndexPair.second +
                                                                                             1]; ++choice) {
                             if (modelComponents.choiceLabeling.get().getLabelsOfChoice(choice).empty()) {

src/storm/generator/NextStateGenerator.h

@@ -63,7 +63,7 @@ namespace storm {
             
             storm::expressions::SimpleValuation toValuation(CompressedState const& state) const;
 
-            uint32 observabilityClass(CompressedState const& state) const;
+            uint32_t observabilityClass(CompressedState const& state) const;
 
             virtual storm::models::sparse::StateLabeling label(storm::storage::sparse::StateStorage<StateType> const& stateStorage, std::vector<StateType> const& initialStateIndices = {}, std::vector<StateType> const& deadlockStateIndices = {}) = 0;
 

src/storm/solver/SmtSolver.h

@@ -73,8 +73,8 @@ namespace storm {
 			SmtSolver(SmtSolver const& other) = default;
 
 			SmtSolver(SmtSolver&& other) = default;
-			SmtSolver& operator=(SmtSolver const& other) = default;
-			SmtSolver& operator=(SmtSolver&& other) = default;
+			SmtSolver& operator=(SmtSolver const& other) = delete;
+			SmtSolver& operator=(SmtSolver&& other) = delete;
    
 			/*!
              * Pushes a backtracking point on the solver's stack. A following call to pop() deletes exactly those

src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp

@@ -81,6 +81,7 @@ namespace storm {
                     if (scc.size() == 1) {
                         returnValue = solveTrivialScc(*scc.begin(), dir, x, b) && returnValue;
                     } else {
+                        STORM_LOG_TRACE("Solving SCC of size " << scc.size() << ".");
                         sccRowGroupsAsBitVector.clear();
                         sccRowsAsBitVector.clear();
                         for (auto const& group : scc) {

src/storm/solver/helper/SoundValueIterationHelper.cpp

@@ -54,12 +54,14 @@ namespace storm {
             
             template<typename ValueType>
             void SoundValueIterationHelper<ValueType>::setLowerBound(ValueType const& value) {
+                STORM_LOG_TRACE("Set lower bound to " << value << ".");
                 hasLowerBound = true;
                 lowerBound = value;
             }
             
             template<typename ValueType>
             void SoundValueIterationHelper<ValueType>::setUpperBound(ValueType const& value) {
+                STORM_LOG_TRACE("Set upper bound to " << value << ".");
                 hasUpperBound = true;
                 upperBound = value;
             }
@@ -223,6 +225,7 @@ namespace storm {
                                 ValueType newDecisionValue = (xTmp[i] - xBest) / deltaY;
                                 if (!hasDecisionValue || better<dir>(newDecisionValue, decisionValue)) {
                                     decisionValue = std::move(newDecisionValue);
+                                    STORM_LOG_TRACE("Update decision value to " << decisionValue);
                                     hasDecisionValue = true;
                                 }
                             }
@@ -347,6 +350,7 @@ namespace storm {
                         }
                     }
                 }
+                STORM_LOG_TRACE("Phase 1 converged: all y values are < 1.");
                 convergencePhase1 = false;
                 return true;
             }
@@ -415,6 +419,7 @@ namespace storm {
                 if (!decisionValueBlocks && hasDecisionValue && better<dir>(decisionValue, getPrimaryBound<dir>())) {
                     getPrimaryBound<dir>() = decisionValue;
                     decisionValueBlocks = true;
+                    STORM_LOG_TRACE("Decision value blocks primary bound to " << decisionValue << ".");
                 }
             }
             

src/storm/storage/expressions/BinaryRelationExpression.h

@@ -26,9 +26,9 @@ namespace storm {
             
             // Instantiate constructors and assignments with their default implementations.
             BinaryRelationExpression(BinaryRelationExpression const& other) = default;
-            BinaryRelationExpression& operator=(BinaryRelationExpression const& other) = default;
+            BinaryRelationExpression& operator=(BinaryRelationExpression const& other) = delete;
             BinaryRelationExpression(BinaryRelationExpression&&) = default;
-            BinaryRelationExpression& operator=(BinaryRelationExpression&&) = default;
+            BinaryRelationExpression& operator=(BinaryRelationExpression&&) = delete;
 
             virtual ~BinaryRelationExpression() = default;
             

src/storm/storage/expressions/ExpressionManager.h

@@ -25,8 +25,7 @@ namespace storm {
             enum class VariableSelection { OnlyRegularVariables, OnlyAuxiliaryVariables, AllVariables };
             
             VariableIterator(ExpressionManager const& manager, std::unordered_map<std::string, uint_fast64_t>::const_iterator nameIndexIterator, std::unordered_map<std::string, uint_fast64_t>::const_iterator nameIndexIteratorEnd, VariableSelection const& selection);
-            VariableIterator(VariableIterator const& other) = default;
-            VariableIterator& operator=(VariableIterator const& other) = default;
+            VariableIterator(VariableIterator&& other) = default;
             
             // Define the basic input iterator operations.
             bool operator==(VariableIterator const& other);