diff --git a/src/counterexamples/MILPMinimalLabelSetGenerator.h b/src/counterexamples/MILPMinimalLabelSetGenerator.h
index 8e9e23503..ea02db662 100644
--- a/src/counterexamples/MILPMinimalLabelSetGenerator.h
+++ b/src/counterexamples/MILPMinimalLabelSetGenerator.h
@@ -99,7 +99,7 @@ namespace storm {
*/
static struct StateInformation determineRelevantAndProblematicStates(storm::models::Mdp<T> const& labeledMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
StateInformation result;
- storm::storage::SparseMatrix<bool> backwardTransitions = labeledMdp.getBackwardTransitions();
+ storm::storage::SparseMatrix<T> backwardTransitions = labeledMdp.getBackwardTransitions();
result.relevantStates = storm::utility::graph::performProbGreater0E(labeledMdp, backwardTransitions, phiStates, psiStates);
result.relevantStates &= ~psiStates;
result.problematicStates = storm::utility::graph::performProbGreater0E(labeledMdp, backwardTransitions, phiStates, psiStates);
@@ -912,7 +912,7 @@ namespace storm {
* @return The total number of constraints that were created.
*/
static uint_fast64_t assertSchedulerCuts(GRBenv* env, GRBmodel* model, storm::models::Mdp<T> const& labeledMdp, storm::storage::BitVector const& psiStates, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) {
- storm::storage::SparseMatrix<bool> backwardTransitions = labeledMdp.getBackwardTransitions();
+ storm::storage::SparseMatrix<T> backwardTransitions = labeledMdp.getBackwardTransitions();
uint_fast64_t numberOfConstraintsCreated = 0;
int error = 0;
std::vector<int> variables;
diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h
index e3fa9e394..8bd56c2dc 100644
--- a/src/counterexamples/SMTMinimalCommandSetGenerator.h
+++ b/src/counterexamples/SMTMinimalCommandSetGenerator.h
@@ -84,7 +84,7 @@ namespace storm {
// Compute all relevant states, i.e. states for which there exists a scheduler that has a non-zero
// probabilitiy of satisfying phi until psi.
- storm::storage::SparseMatrix<bool> backwardTransitions = labeledMdp.getBackwardTransitions();
+ storm::storage::SparseMatrix<T> backwardTransitions = labeledMdp.getBackwardTransitions();
relevancyInformation.relevantStates = storm::utility::graph::performProbGreater0E(labeledMdp, backwardTransitions, phiStates, psiStates);
relevancyInformation.relevantStates &= ~psiStates;
@@ -214,7 +214,7 @@ namespace storm {
std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = labeledMdp.getNondeterministicChoiceIndices();
storm::storage::BitVector const& initialStates = labeledMdp.getInitialStates();
std::vector<storm::storage::VectorSet<uint_fast64_t>> const& choiceLabeling = labeledMdp.getChoiceLabeling();
- storm::storage::SparseMatrix<bool> backwardTransitions = labeledMdp.getBackwardTransitions();
+ storm::storage::SparseMatrix<T> backwardTransitions = labeledMdp.getBackwardTransitions();
for (auto currentState : relevancyInformation.relevantStates) {
for (auto currentChoice : relevancyInformation.relevantChoicesForRelevantStates.at(currentState)) {
@@ -484,7 +484,7 @@ namespace storm {
// Get some data from the MDP for convenient access.
storm::storage::SparseMatrix<T> const& transitionMatrix = labeledMdp.getTransitionMatrix();
std::vector<storm::storage::VectorSet<uint_fast64_t>> const& choiceLabeling = labeledMdp.getChoiceLabeling();
- storm::storage::SparseMatrix<bool> backwardTransitions = labeledMdp.getBackwardTransitions();
+ storm::storage::SparseMatrix<T> backwardTransitions = labeledMdp.getBackwardTransitions();
// Compute the set of labels that may precede a given action.
for (auto currentState : relevancyInformation.relevantStates) {
diff --git a/src/modelchecker/prctl/TopologicalValueIterationMdpPrctlModelChecker.h b/src/modelchecker/prctl/TopologicalValueIterationMdpPrctlModelChecker.h
index 69f62c15c..77fa27543 100644
--- a/src/modelchecker/prctl/TopologicalValueIterationMdpPrctlModelChecker.h
+++ b/src/modelchecker/prctl/TopologicalValueIterationMdpPrctlModelChecker.h
@@ -69,7 +69,7 @@ private:
// Now, we need to determine the SCCs of the MDP and a topological sort.
std::vector<std::vector<uint_fast64_t>> stronglyConnectedComponents = storm::utility::graph::performSccDecomposition(this->getModel(), stronglyConnectedComponents, stronglyConnectedComponentsDependencyGraph);
- storm::storage::SparseMatrix<bool> stronglyConnectedComponentsDependencyGraph = this->getModel().extractSccDependencyGraph(stronglyConnectedComponents);
+ storm::storage::SparseMatrix<T> stronglyConnectedComponentsDependencyGraph = this->getModel().extractSccDependencyGraph(stronglyConnectedComponents);
std::vector<uint_fast64_t> topologicalSort = storm::utility::graph::getTopologicalSort(stronglyConnectedComponentsDependencyGraph);
// Set up the environment for the power method.
diff --git a/src/models/AbstractModel.h b/src/models/AbstractModel.h
index 84663dbc0..0a02028d3 100644
--- a/src/models/AbstractModel.h
+++ b/src/models/AbstractModel.h
@@ -145,10 +145,10 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
/*!
* Extracts the dependency graph from the model according to the given partition.
*
- * @param partition A vector containing the blocks of the partition of the system.
+ * @param decomposition A decomposition containing the blocks of the partition of the system.
* @return A sparse matrix with bool entries that represents the dependency graph of the blocks of the partition.
*/
- storm::storage::SparseMatrix<bool> extractPartitionDependencyGraph(storm::storage::Decomposition const& decomposition) const {
+ storm::storage::SparseMatrix<T> extractPartitionDependencyGraph(storm::storage::Decomposition const& decomposition) const {
uint_fast64_t numberOfStates = decomposition.size();
// First, we need to create a mapping of states to their SCC index, to ease the computation of dependency transitions later.
@@ -160,7 +160,7 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
}
// The resulting sparse matrix will have as many rows/columns as there are blocks in the partition.
- storm::storage::SparseMatrix<bool> dependencyGraph(numberOfStates);
+ storm::storage::SparseMatrix<T> dependencyGraph(numberOfStates);
dependencyGraph.initialize();
for (uint_fast64_t currentBlockIndex = 0; currentBlockIndex < decomposition.size(); ++currentBlockIndex) {
@@ -191,76 +191,15 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
dependencyGraph.finalize(true);
return dependencyGraph;
}
-
- /*!
- * Retrieves the backward transition relation of the model, i.e. a set of transitions
- * between states that correspond to the reversed transition relation of this model.
- *
- * @return A sparse matrix that represents the backward transitions of this model.
- */
- storm::storage::SparseMatrix<bool> getBackwardTransitions() const {
- return getBackwardTransitions<bool>([](T const& value) -> bool { return value != 0; });
- }
-
+
/*!
* Retrieves the backward transition relation of the model, i.e. a set of transitions
* between states that correspond to the reversed transition relation of this model.
*
* @return A sparse matrix that represents the backward transitions of this model.
*/
- template <typename TransitionType>
- storm::storage::SparseMatrix<TransitionType> getBackwardTransitions(std::function<TransitionType(T const&)> const& selectionFunction) const {
- uint_fast64_t numberOfStates = this->getNumberOfStates();
- uint_fast64_t numberOfTransitions = this->getNumberOfTransitions();
-
- std::vector<uint_fast64_t> rowIndications(numberOfStates + 1);
- std::vector<uint_fast64_t> columnIndications(numberOfTransitions);
- std::vector<TransitionType> values(numberOfTransitions, TransitionType());
-
- // First, we need to count how many backward transitions each state has.
- for (uint_fast64_t i = 0; i < numberOfStates; ++i) {
- typename storm::storage::SparseMatrix<T>::Rows rows = this->getRows(i);
- for (auto const& transition : rows) {
- if (transition.value() > 0) {
- ++rowIndications[transition.column() + 1];
- }
- }
- }
-
- // Now compute the accumulated offsets.
- for (uint_fast64_t i = 1; i < numberOfStates; ++i) {
- rowIndications[i] = rowIndications[i - 1] + rowIndications[i];
- }
-
- // Put a sentinel element at the end of the indices list. This way,
- // for each state i the range of indices can be read off between
- // state_indices_list[i] and state_indices_list[i + 1].
- // FIXME: This should not be necessary and already be implied by the first steps.
- rowIndications[numberOfStates] = numberOfTransitions;
-
- // Create an array that stores the next index for each state. Initially
- // this corresponds to the previously computed accumulated offsets.
- std::vector<uint_fast64_t> nextIndices = rowIndications;
-
- // Now we are ready to actually fill in the list of predecessors for
- // every state. Again, we start by considering all but the last row.
- for (uint_fast64_t i = 0; i < numberOfStates; ++i) {
- typename storm::storage::SparseMatrix<T>::Rows rows = this->getRows(i);
- for (auto& transition : rows) {
- if (transition.value() > 0) {
- values[nextIndices[transition.column()]] = selectionFunction(transition.value());
- columnIndications[nextIndices[transition.column()]++] = i;
- }
- }
- }
-
- storm::storage::SparseMatrix<TransitionType> backwardTransitionMatrix(numberOfStates, numberOfStates,
- numberOfTransitions,
- std::move(rowIndications),
- std::move(columnIndications),
- std::move(values));
-
- return backwardTransitionMatrix;
+ storm::storage::SparseMatrix<T> getBackwardTransitions() const {
+ return this->transitionMatrix.transpose();
}
/*!
diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp
index 6cc37eca9..50c73d96e 100644
--- a/src/storage/SparseMatrix.cpp
+++ b/src/storage/SparseMatrix.cpp
@@ -662,6 +662,57 @@ namespace storage {
negateAllNonDiagonalElements();
}
+ template <typename T>
+ SparseMatrix<T> SparseMatrix<T>::transpose() const {
+
+ uint_fast64_t rowCount = this->colCount;
+ uint_fast64_t colCount = this->rowCount;
+ uint_fast64_t nonZeroEntryCount = this->nonZeroEntryCount;
+
+ std::vector<uint_fast64_t> rowIndications(rowCount + 1);
+ std::vector<uint_fast64_t> columnIndications(nonZeroEntryCount);
+ std::vector<T> values(nonZeroEntryCount, T());
+
+ // First, we need to count how many entries each column has.
+ for (uint_fast64_t i = 0; i < this->rowCount; ++i) {
+ typename storm::storage::SparseMatrix<T>::Rows rows = this->getRow(i);
+ for (auto const& transition : rows) {
+ if (transition.value() > 0) {
+ ++rowIndications[transition.column() + 1];
+ }
+ }
+ }
+
+ // Now compute the accumulated offsets.
+ for (uint_fast64_t i = 1; i < rowCount + 1; ++i) {
+ rowIndications[i] = rowIndications[i - 1] + rowIndications[i];
+ }
+
+ // Create an array that stores the index for the next value to be added for
+ // each row in the transposed matrix. Initially this corresponds to the previously
+ // computed accumulated offsets.
+ std::vector<uint_fast64_t> nextIndices = rowIndications;
+
+ // Now we are ready to actually fill in the values of the transposed matrix.
+ for (uint_fast64_t i = 0; i < this->rowCount; ++i) {
+ typename storm::storage::SparseMatrix<T>::Rows rows = this->getRow(i);
+ for (auto& transition : rows) {
+ if (transition.value() > 0) {
+ values[nextIndices[transition.column()]] = transition.value();
+ columnIndications[nextIndices[transition.column()]++] = i;
+ }
+ }
+ }
+
+ storm::storage::SparseMatrix<T> transposedMatrix(rowCount, colCount,
+ nonZeroEntryCount,
+ std::move(rowIndications),
+ std::move(columnIndications),
+ std::move(values));
+
+ return transposedMatrix;
+ }
+
template<typename T>
void SparseMatrix<T>::invertDiagonal() {
// Check if the matrix is square, because only then it makes sense to perform this
@@ -1000,7 +1051,7 @@ namespace storage {
// Explicit instantiations of specializations of this template here.
template class SparseMatrix<double>;
- template class SparseMatrix<bool>;
+ template class SparseMatrix<int>;
// Functions of the tbbHelper_MatrixRowVectorScalarProduct friend class.
diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h
index 0bd275e73..669b8b692 100644
--- a/src/storage/SparseMatrix.h
+++ b/src/storage/SparseMatrix.h
@@ -538,6 +538,13 @@ public:
*/
void convertToEquationSystem();
+ /*!
+ * Transposes the matrix.
+ *
+ * @return A sparse matrix that represents the transpose of this matrix.
+ */
+ storm::storage::SparseMatrix<T> transpose() const;
+
/*!
* Inverts all elements on the diagonal, i.e. sets the diagonal values to 1 minus their previous
* value. Requires the matrix to contain each diagonal element and to be square.
@@ -791,7 +798,7 @@ private:
// Extern template declaration to tell the compiler that there already is an instanciation of this template somewhere.
// The extern instance will be found by the linker. Prevents multiple instantiations of the same template specialisation.
extern template class SparseMatrix<double>;
-extern template class SparseMatrix<bool>;
+extern template class SparseMatrix<int>;
#ifdef STORM_HAVE_INTELTBB
/*!
diff --git a/src/utility/counterexamples.h b/src/utility/counterexamples.h
index 0ac816236..bd441a048 100644
--- a/src/utility/counterexamples.h
+++ b/src/utility/counterexamples.h
@@ -25,7 +25,7 @@ namespace storm {
storm::storage::SparseMatrix<T> const& transitionMatrix = labeledMdp.getTransitionMatrix();
std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = labeledMdp.getNondeterministicChoiceIndices();
std::vector<storm::storage::VectorSet<uint_fast64_t>> const& choiceLabeling = labeledMdp.getChoiceLabeling();
- storm::storage::SparseMatrix<bool> backwardTransitions = labeledMdp.getBackwardTransitions();
+ storm::storage::SparseMatrix<T> backwardTransitions = labeledMdp.getBackwardTransitions();
// Now we compute the set of labels that is present on all paths from the initial to the target states.
std::vector<storm::storage::VectorSet<uint_fast64_t>> analysisInformation(labeledMdp.getNumberOfStates(), relevantLabels);
diff --git a/src/utility/graph.h b/src/utility/graph.h
index e0e68402b..c9c58a86a 100644
--- a/src/utility/graph.h
+++ b/src/utility/graph.h
@@ -50,7 +50,7 @@ namespace storm {
storm::storage::BitVector statesWithProbabilityGreater0(model.getNumberOfStates());
// Get the backwards transition relation from the model to ease the search.
- storm::storage::SparseMatrix<bool> backwardTransitions = model.getBackwardTransitions();
+ storm::storage::SparseMatrix<T> backwardTransitions = model.getBackwardTransitions();
// Add all psi states as the already satisfy the condition.
statesWithProbabilityGreater0 |= psiStates;
@@ -177,7 +177,7 @@ namespace storm {
* @return A bit vector that represents all states with probability 0.
*/
template <typename T>
- storm::storage::BitVector performProbGreater0E(storm::models::AbstractNondeterministicModel<T> const& model, storm::storage::SparseMatrix<bool> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) {
+ storm::storage::BitVector performProbGreater0E(storm::models::AbstractNondeterministicModel<T> const& model, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) {
// Prepare resulting bit vector.
storm::storage::BitVector statesWithProbabilityGreater0(model.getNumberOfStates());
@@ -245,7 +245,7 @@ namespace storm {
* @return A bit vector that represents all states with probability 0.
*/
template <typename T>
- storm::storage::BitVector performProb0A(storm::models::AbstractNondeterministicModel<T> const& model, storm::storage::SparseMatrix<bool> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
+ storm::storage::BitVector performProb0A(storm::models::AbstractNondeterministicModel<T> const& model, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
storm::storage::BitVector statesWithProbability0 = performProbGreater0E(model, backwardTransitions, phiStates, psiStates);
statesWithProbability0.complement();
return statesWithProbability0;
@@ -264,7 +264,7 @@ namespace storm {
* @return A bit vector that represents all states with probability 1.
*/
template <typename T>
- storm::storage::BitVector performProb1E(storm::models::AbstractNondeterministicModel<T> const& model, storm::storage::SparseMatrix<bool> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
+ storm::storage::BitVector performProb1E(storm::models::AbstractNondeterministicModel<T> const& model, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
// Get some temporaries for convenience.
storm::storage::SparseMatrix<T> const& transitionMatrix = model.getTransitionMatrix();
std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices();
@@ -338,7 +338,7 @@ namespace storm {
std::pair<storm::storage::BitVector, storm::storage::BitVector> result;
// Get the backwards transition relation from the model to ease the search.
- storm::storage::SparseMatrix<bool> backwardTransitions = model.getBackwardTransitions();
+ storm::storage::SparseMatrix<T> backwardTransitions = model.getBackwardTransitions();
result.first = performProb0A(model, backwardTransitions, phiStates, psiStates);
result.second = performProb1E(model, backwardTransitions, phiStates, psiStates);
@@ -360,7 +360,7 @@ namespace storm {
* @return A bit vector that represents all states with probability 0.
*/
template <typename T>
- storm::storage::BitVector performProbGreater0A(storm::models::AbstractNondeterministicModel<T> const& model, storm::storage::SparseMatrix<bool> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) {
+ storm::storage::BitVector performProbGreater0A(storm::models::AbstractNondeterministicModel<T> const& model, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) {
// Prepare resulting bit vector.
storm::storage::BitVector statesWithProbabilityGreater0(model.getNumberOfStates());
@@ -451,7 +451,7 @@ namespace storm {
* @return A bit vector that represents all states with probability 0.
*/
template <typename T>
- storm::storage::BitVector performProb0E(storm::models::AbstractNondeterministicModel<T> const& model, storm::storage::SparseMatrix<bool> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
+ storm::storage::BitVector performProb0E(storm::models::AbstractNondeterministicModel<T> const& model, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
storm::storage::BitVector statesWithProbability0 = performProbGreater0A(model, backwardTransitions, phiStates, psiStates);
statesWithProbability0.complement();
return statesWithProbability0;
@@ -470,7 +470,7 @@ namespace storm {
* @return A bit vector that represents all states with probability 0.
*/
template <typename T>
- storm::storage::BitVector performProb1A(storm::models::AbstractNondeterministicModel<T> const& model, storm::storage::SparseMatrix<bool> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
+ storm::storage::BitVector performProb1A(storm::models::AbstractNondeterministicModel<T> const& model, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
// Get some temporaries for convenience.
storm::storage::SparseMatrix<T> const& transitionMatrix = model.getTransitionMatrix();
std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices();
@@ -543,7 +543,7 @@ namespace storm {
std::pair<storm::storage::BitVector, storm::storage::BitVector> result;
// Get the backwards transition relation from the model to ease the search.
- storm::storage::SparseMatrix<bool> backwardTransitions = model.getBackwardTransitions();
+ storm::storage::SparseMatrix<T> backwardTransitions = model.getBackwardTransitions();
result.first = performProb0E(model, backwardTransitions, phiStates, psiStates);
result.second = performProb1A(model, backwardTransitions, phiStates, psiStates);
diff --git a/test/performance/graph/GraphTest.cpp b/test/performance/graph/GraphTest.cpp
index a050be516..0f1459e52 100644
--- a/test/performance/graph/GraphTest.cpp
+++ b/test/performance/graph/GraphTest.cpp
@@ -98,7 +98,7 @@ TEST(GraphTest, PerformSCCDecompositionAndGetDependencyGraph) {
ASSERT_EQ(sccDecomposition.size(), 1290297ull);
LOG4CPLUS_WARN(logger, "Extracting SCC dependency graph of crowds/crowds20_5...");
- storm::storage::SparseMatrix<bool> sccDependencyGraph(std::move(dtmc->extractPartitionDependencyGraph(sccDecomposition)));
+ storm::storage::SparseMatrix<double> sccDependencyGraph(std::move(dtmc->extractPartitionDependencyGraph(sccDecomposition)));
LOG4CPLUS_WARN(logger, "Done.");
ASSERT_EQ(sccDependencyGraph.getNonZeroEntryCount(), 1371253ull);
@@ -155,4 +155,4 @@ TEST(GraphTest, PerformSCCDecompositionAndGetDependencyGraph) {
ASSERT_EQ(sccDependencyGraph.getNonZeroEntryCount(), 7888ull);
mdp2 = nullptr;
-}
\ No newline at end of file
+}