From 2df4679fbc2a0e8f996950d8432d72fb0383600f Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Thu, 27 Feb 2020 22:27:52 +0100
Subject: [PATCH] Slight optimization in performProb1A
---
src/storm/utility/graph.cpp | 44 +++++++++++++++++++++++++------------
1 file changed, 30 insertions(+), 14 deletions(-)
diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp
index b774c65da..02082ee96 100644
--- a/src/storm/utility/graph.cpp
+++ b/src/storm/utility/graph.cpp
@@ -882,36 +882,46 @@ namespace storm {
size_t numberOfStates = phiStates.size();
// Initialize the environment for the iterative algorithm.
- storm::storage::BitVector currentStates(numberOfStates, true);
+ storm::storage::BitVector bv1, bv2;
+ storm::storage::BitVector* currentStates = &bv1;
+ *currentStates = phiStates;
+ storm::storage::BitVector* nextStates = &bv2;
+ *nextStates = psiStates;
std::vector<uint_fast64_t> stack;
stack.reserve(numberOfStates);
+ // Simplify comparison between next and current states by keeping track of the number of set bits
+ uint64_t currentStatesSetBits = numberOfStates;
+ uint64_t numPsiStates = psiStates.getNumberOfSetBits();
+ uint64_t nextStatesSetBits = numPsiStates;
+
// Perform the loop as long as the set of states gets smaller.
bool done = false;
uint_fast64_t currentState;
while (!done) {
stack.clear();
- storm::storage::BitVector nextStates(psiStates);
stack.insert(stack.end(), psiStates.begin(), psiStates.end());
while (!stack.empty()) {
currentState = stack.back();
stack.pop_back();
- for(typename storm::storage::SparseMatrix<T>::const_iterator predecessorEntryIt = backwardTransitions.begin(currentState), predecessorEntryIte = backwardTransitions.end(currentState); predecessorEntryIt != predecessorEntryIte; ++predecessorEntryIt) {
- if (phiStates.get(predecessorEntryIt->getColumn()) && !nextStates.get(predecessorEntryIt->getColumn())) {
+ for(auto const& predecessor : backwardTransitions.getRow(currentState)) {
+ auto predecessorState = predecessor.getColumn();
+ if (phiStates.get(predecessorState) && !nextStates->get(predecessorState)) {
// Check whether the predecessor has only successors in the current state set for all of the
// nondeterminstic choices and that for each choice there exists a successor that is already
// in the next states.
bool addToStatesWithProbability1 = true;
- for (uint_fast64_t row = nondeterministicChoiceIndices[predecessorEntryIt->getColumn()]; row < nondeterministicChoiceIndices[predecessorEntryIt->getColumn() + 1]; ++row) {
+ for (uint_fast64_t row = nondeterministicChoiceIndices[predecessorState]; row < nondeterministicChoiceIndices[predecessorState + 1]; ++row) {
bool hasAtLeastOneSuccessorWithProbability1 = false;
- for (typename storm::storage::SparseMatrix<T>::const_iterator successorEntryIt = transitionMatrix.begin(row), successorEntryIte = transitionMatrix.end(row); successorEntryIt != successorEntryIte; ++successorEntryIt) {
- if (!currentStates.get(successorEntryIt->getColumn())) {
+ for (auto const& successor : transitionMatrix.getRow(row)) {
+ auto successorState = successor.getColumn();
+ if (!currentStates->get(successorState)) {
addToStatesWithProbability1 = false;
goto afterCheckLoop;
}
- if (nextStates.get(successorEntryIt->getColumn())) {
+ if (!hasAtLeastOneSuccessorWithProbability1 && nextStates->get(successorState)) {
hasAtLeastOneSuccessorWithProbability1 = true;
}
}
@@ -927,21 +937,27 @@ namespace storm {
// add it to the set of states for the next iteration and perform a backward search from
// that state.
if (addToStatesWithProbability1) {
- nextStates.set(predecessorEntryIt->getColumn(), true);
- stack.push_back(predecessorEntryIt->getColumn());
+ ++nextStatesSetBits;
+ nextStates->set(predecessorState, true);
+ stack.push_back(predecessorState);
}
}
}
}
-
// Check whether we need to perform an additional iteration.
- if (currentStates == nextStates) {
+ if (currentStatesSetBits == nextStatesSetBits && *currentStates == *nextStates) {
done = true;
} else {
- currentStates = std::move(nextStates);
+ // Prepare next iteration.
+ // The nextStates become the new currentStates.
+ std::swap(currentStates, nextStates);
+ currentStatesSetBits = nextStatesSetBits;
+ *nextStates = psiStates;
+ nextStatesSetBits = numPsiStates;
+
}
}
- return currentStates;
+ return *currentStates;
}
template <typename T>