diff --git a/src/modelchecker/reachability/SparseSccModelChecker.cpp b/src/modelchecker/reachability/SparseSccModelChecker.cpp index 3911f1a6f..7aae3f0b4 100644 --- a/src/modelchecker/reachability/SparseSccModelChecker.cpp +++ b/src/modelchecker/reachability/SparseSccModelChecker.cpp @@ -43,6 +43,9 @@ namespace storm { } } + // Make sure that we have eliminated all transitions from the initial state. + STORM_LOG_ASSERT(flexibleMatrix.getRow(*initialStates.begin()).empty(), "The transitions of the initial states are non-empty."); + auto modelCheckingEnd = std::chrono::high_resolution_clock::now(); auto totalTimeEnd = std::chrono::high_resolution_clock::now(); @@ -127,6 +130,7 @@ namespace storm { storm::storage::SparseMatrix submatrix = dtmc.getTransitionMatrix().getSubmatrix(false, maybeStates, maybeStates); // To be able to apply heuristics later, we now determine the distance of each state to the initial state. + // We start by setting up the data structures. std::vector> stateQueue; stateQueue.reserve(submatrix.getRowCount()); storm::storage::BitVector statesInQueue(submatrix.getRowCount()); @@ -138,7 +142,7 @@ namespace storm { statesInQueue.set(initialState); } - // Perform a BFS. + // And then perform the BFS. while (currentPosition < stateQueue.size()) { std::pair const& stateDistancePair = stateQueue[currentPosition]; distances[stateDistancePair.first] = stateDistancePair.second; diff --git a/src/utility/ConstantsComparator.cpp b/src/utility/ConstantsComparator.cpp index 71d2bb165..c83ee9583 100644 --- a/src/utility/ConstantsComparator.cpp +++ b/src/utility/ConstantsComparator.cpp @@ -21,17 +21,10 @@ namespace storm { } template - ValueType& simplify(ValueType& value) { + ValueType simplify(ValueType value) { // In the general case, we don't to anything here, but merely return the value. If something else is // supposed to happen here, the templated function can be specialized for this particular type. - return value; - } - - template - ValueType&& simplify(ValueType&& value) { - // In the general case, we don't to anything here, but merely return the value. If something else is - // supposed to happen here, the templated function can be specialized for this particular type. - return std::move(value); + return std::forward(value); } template diff --git a/src/utility/ConstantsComparator.h b/src/utility/ConstantsComparator.h index 6bc668445..37e27ea46 100644 --- a/src/utility/ConstantsComparator.h +++ b/src/utility/ConstantsComparator.h @@ -28,10 +28,7 @@ namespace storm { ValueType infinity(); template - ValueType& simplify(ValueType& value); - - template - ValueType&& simplify(ValueType&& value); + ValueType simplify(ValueType value); // A class that can be used for comparing constants. template