From 05471d94fdc9e7f03b32634d2af166476ec6d8f3 Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Mon, 2 Mar 2020 14:19:25 +0100
Subject: [PATCH] Optimizations in JaniNextStateGenerator that avoid
unnecessary (re-) allocations of memory. Moreover, before collecting the
complete set of enabled edges for each automaton, we first check whether each
automaton (that synchronizes with that action) has at least one enabled edge.
This avoids checking unnecessarily many edge guards.
---
src/storm/generator/Choice.cpp | 5 +
src/storm/generator/Choice.h | 5 +
.../generator/JaniNextStateGenerator.cpp | 96 +++++++++++++++----
src/storm/storage/Distribution.cpp | 12 +--
src/storm/storage/Distribution.h | 5 +
5 files changed, 96 insertions(+), 27 deletions(-)
diff --git a/src/storm/generator/Choice.cpp b/src/storm/generator/Choice.cpp
index 43189e623..5d69c98ab 100644
--- a/src/storm/generator/Choice.cpp
+++ b/src/storm/generator/Choice.cpp
@@ -163,6 +163,11 @@ namespace storm {
return distribution.size();
}
+ template<typename ValueType, typename StateType>
+ void Choice<ValueType, StateType>::reserve(std::size_t const& size) {
+ distribution.reserve(size);
+ }
+
template<typename ValueType, typename StateType>
std::ostream& operator<<(std::ostream& out, Choice<ValueType, StateType> const& choice) {
out << "<";
diff --git a/src/storm/generator/Choice.h b/src/storm/generator/Choice.h
index 04e0fd311..1dbc41760 100644
--- a/src/storm/generator/Choice.h
+++ b/src/storm/generator/Choice.h
@@ -150,6 +150,11 @@ namespace storm {
*/
std::size_t size() const;
+ /*!
+ * If the size is already known, reserves space in the underlying distribution.
+ */
+ void reserve(std::size_t const& size);
+
private:
// A flag indicating whether this choice is Markovian or not.
bool markovian;
diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp
index 6078d15f8..6c260746b 100644
--- a/src/storm/generator/JaniNextStateGenerator.cpp
+++ b/src/storm/generator/JaniNextStateGenerator.cpp
@@ -820,6 +820,7 @@ namespace storm {
// Add the probabilities/rates to the newly created choice.
ValueType probabilitySum = storm::utility::zero<ValueType>();
+ choice.reserve(std::distance(distribution.begin(), distribution.end()));
for (auto const& stateProbability : distribution) {
choice.addProbability(stateProbability.getState(), stateProbability.getValue());
@@ -853,7 +854,13 @@ namespace storm {
std::vector<Choice<ValueType>> JaniNextStateGenerator<ValueType, StateType>::getActionChoices(std::vector<uint64_t> const& locations, CompressedState const& state, StateToIdCallback stateToIdCallback, EdgeFilter const& edgeFilter) {
std::vector<Choice<ValueType>> result;
- for (auto const& outputAndEdges : edges) {
+ // To avoid reallocations, we declare some memory here here.
+ // This vector will store for each automaton the set of edges with the current output and the current source location
+ std::vector<EdgeSetWithIndices const*> edgeSetsMemory;
+ // This vector will store the 'first' combination of edges that is productive.
+ std::vector<typename EdgeSetWithIndices::const_iterator> edgeIteratorMemory;
+
+ for (OutputAndEdges const& outputAndEdges : edges) {
auto const& edges = outputAndEdges.second;
if (edges.size() == 1) {
// If the synch consists of just one element, it's non-synchronizing.
@@ -885,45 +892,92 @@ namespace storm {
// If the element has more than one set of edges, we need to perform a synchronization.
STORM_LOG_ASSERT(outputAndEdges.first, "Need output action index for synchronization.");
- AutomataEdgeSets automataEdgeSets;
uint64_t outputActionIndex = outputAndEdges.first.get();
+ // Find out whether this combination is productive
bool productiveCombination = true;
- EdgeSetWithIndices enabledEdgesOfAutomaton;
+ // First check, whether each automaton has at least one edge with the current output and the current source location
+ // We will also store the edges of each automaton with the current outputAction
+ edgeSetsMemory.clear();
for (auto const& automatonAndEdges : outputAndEdges.second) {
uint64_t automatonIndex = automatonAndEdges.first;
-
- bool atLeastOneEdge = false;
- auto edgesIt = automatonAndEdges.second.find(locations[automatonIndex]);
- if (edgesIt != automatonAndEdges.second.end()) {
- for (auto const& indexAndEdge : edgesIt->second) {
+ LocationsAndEdges const& locationsAndEdges = automatonAndEdges.second;
+ auto edgesIt = locationsAndEdges.find(locations[automatonIndex]);
+ if (edgesIt == locationsAndEdges.end()) {
+ productiveCombination = false;
+ break;
+ }
+ edgeSetsMemory.push_back(&edgesIt->second);
+ }
+
+ if (productiveCombination) {
+ // second, check whether each automaton has at least one enabled action
+ edgeIteratorMemory.clear(); // Store the first enabled edge in each automaton.
+ for (auto const& edgesIt : edgeSetsMemory) {
+ bool atLeastOneEdge = false;
+ EdgeSetWithIndices const& edgeSetWithIndices = *edgesIt;
+ for (auto indexAndEdgeIt = edgeSetWithIndices.begin(), indexAndEdgeIte = edgeSetWithIndices.end(); indexAndEdgeIt != indexAndEdgeIte; ++indexAndEdgeIt) {
+ // check whether we do not consider this edge
if (edgeFilter != EdgeFilter::All) {
STORM_LOG_ASSERT(edgeFilter == EdgeFilter::WithRate || edgeFilter == EdgeFilter::WithoutRate, "Unexpected edge filter.");
- if ((edgeFilter == EdgeFilter::WithRate) != indexAndEdge.second->hasRate()) {
+ if ((edgeFilter == EdgeFilter::WithRate) != indexAndEdgeIt->second->hasRate()) {
continue;
}
}
- if (!this->evaluator->asBool(indexAndEdge.second->getGuard())) {
+
+ if (!this->evaluator->asBool(indexAndEdgeIt->second->getGuard())) {
continue;
}
+ // If we reach this point, the edge is considered enabled.
atLeastOneEdge = true;
- enabledEdgesOfAutomaton.emplace_back(indexAndEdge);
+ edgeIteratorMemory.push_back(indexAndEdgeIt);
+ break;
+ }
+
+ // If there is no enabled edge of this automaton, the whole combination is not productive.
+ if (!atLeastOneEdge) {
+ productiveCombination = false;
+ break;
}
}
-
- // If there is no enabled edge of this automaton, the whole combination is not productive.
- if (!atLeastOneEdge) {
- STORM_LOG_ASSERT(enabledEdgesOfAutomaton.empty(), "enabledEdgesOfAutomaton should be empty at this point.");
- productiveCombination = false;
- break;
- }
-
- automataEdgeSets.emplace_back(std::move(automatonIndex), std::move(enabledEdgesOfAutomaton));
- enabledEdgesOfAutomaton.clear();
}
+ // produce the combination
if (productiveCombination) {
+ AutomataEdgeSets automataEdgeSets;
+ automataEdgeSets.reserve(outputAndEdges.second.size());
+ STORM_LOG_ASSERT(edgeSetsMemory.size() == outputAndEdges.second.size(), "Unexpected number of edge sets stored.");
+ STORM_LOG_ASSERT(edgeIteratorMemory.size() == outputAndEdges.second.size(), "Unexpected number of edge iterators stored.");
+ auto edgeSetIt = edgeSetsMemory.begin();
+ auto edgeIteratorIt = edgeIteratorMemory.begin();
+ for (auto const& automatonAndEdges : outputAndEdges.second) {
+ EdgeSetWithIndices enabledEdgesOfAutomaton;
+ uint64_t automatonIndex = automatonAndEdges.first;
+ EdgeSetWithIndices const& edgeSetWithIndices = **edgeSetIt;
+ auto indexAndEdgeIt = *edgeIteratorIt;
+ // The first edge where the edgeIterator points to is always enabled.
+ enabledEdgesOfAutomaton.emplace_back(*indexAndEdgeIt);
+ auto indexAndEdgeIte = edgeSetWithIndices.end();
+ for (++indexAndEdgeIt; indexAndEdgeIt != indexAndEdgeIte; ++indexAndEdgeIt) {
+ // check whether we do not consider this edge
+ if (edgeFilter != EdgeFilter::All) {
+ STORM_LOG_ASSERT(edgeFilter == EdgeFilter::WithRate || edgeFilter == EdgeFilter::WithoutRate, "Unexpected edge filter.");
+ if ((edgeFilter == EdgeFilter::WithRate) != indexAndEdgeIt->second->hasRate()) {
+ continue;
+ }
+ }
+
+ if (!this->evaluator->asBool(indexAndEdgeIt->second->getGuard())) {
+ continue;
+ }
+ // If we reach this point, the edge is considered enabled.
+ enabledEdgesOfAutomaton.emplace_back(*indexAndEdgeIt);
+ }
+ automataEdgeSets.emplace_back(std::move(automatonIndex), std::move(enabledEdgesOfAutomaton));
+ ++edgeSetIt;
+ ++edgeIteratorIt;
+ }
// insert choices in the result vector.
expandSynchronizingEdgeCombination(automataEdgeSets, outputActionIndex, state, stateToIdCallback, result);
}
diff --git a/src/storm/storage/Distribution.cpp b/src/storm/storage/Distribution.cpp
index 9d0d89d19..f40afb402 100644
--- a/src/storm/storage/Distribution.cpp
+++ b/src/storm/storage/Distribution.cpp
@@ -19,6 +19,11 @@ namespace storm {
// Intentionally left empty.
}
+ template<typename ValueType, typename StateType>
+ void Distribution<ValueType, StateType>::reserve(uint64_t size) {
+ this->distribution.reserve(size);
+ }
+
template<typename ValueType, typename StateType>
void Distribution<ValueType, StateType>::add(Distribution const& other) {
container_type newDistribution;
@@ -51,12 +56,7 @@ namespace storm {
template<typename ValueType, typename StateType>
void Distribution<ValueType, StateType>::addProbability(StateType const& state, ValueType const& probability) {
- auto it = this->distribution.find(state);
- if (it == this->distribution.end()) {
- this->distribution.emplace_hint(it, state, probability);
- } else {
- it->second += probability;
- }
+ this->distribution[state] += probability;
}
template<typename ValueType, typename StateType>
diff --git a/src/storm/storage/Distribution.h b/src/storm/storage/Distribution.h
index 1d0fbbd5f..d7e0bd2fb 100644
--- a/src/storm/storage/Distribution.h
+++ b/src/storm/storage/Distribution.h
@@ -32,6 +32,11 @@ namespace storm {
Distribution(Distribution&& other) = default;
Distribution& operator=(Distribution&& other) = default;
+ /*
+ * If the size of this distribution is known before adding probabilities,, this method can be used to reserve enough space.
+ */
+ void reserve(uint64_t size);
+
/*!
* Adds the given distribution to the current one.
*/