From d06c5b4a0c2b054bfbaae4d7bbb66ddb859e7ee1 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Thu, 16 Oct 2014 15:06:40 +0200
Subject: [PATCH] Fixed simplify.
Former-commit-id: 85504746d707e4be129f8031f7cf13c58b3103a0
---
.../reachability/SparseSccModelChecker.cpp | 6 +++++-
src/utility/ConstantsComparator.cpp | 11 ++---------
src/utility/ConstantsComparator.h | 5 +----
3 files changed, 8 insertions(+), 14 deletions(-)
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<ValueType> 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<std::pair<storm::storage::sparse::state_type, std::size_t>> 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<storm::storage::sparse::state_type, std::size_t> 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<typename ValueType>
- 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<typename ValueType>
- 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<ValueType>(value);
}
template<typename ValueType>
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<typename ValueType>
- ValueType& simplify(ValueType& value);
-
- template<typename ValueType>
- ValueType&& simplify(ValueType&& value);
+ ValueType simplify(ValueType value);
// A class that can be used for comparing constants.
template<typename ValueType>