diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h index 0f5a5c074..23e18f4fc 100644 --- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h @@ -430,9 +430,7 @@ public: storm::utility::vector::setVectorValues(*result, maybeStates, storm::utility::constGetOne()); } else { // In this case we have to compute the reward values for the remaining states. - uint_fast64_t maybeStatesSetBitCount = maybeStates.getNumberOfSetBits(); - - // Now we can eliminate the rows and columns from the original transition probability matrix. + // We can eliminate the rows and columns from the original transition probability matrix. storm::storage::SparseMatrix submatrix = this->getModel().getTransitionMatrix().getSubmatrix(maybeStates); // Converting the matrix from the fixpoint notation to the form needed for the equation // system. That is, we go from x = A*x + b to (I-A)x = b. diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h index 530e9df18..5256fda66 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h @@ -318,7 +318,7 @@ namespace storm { // Create vector for results for maybe states. std::vector x = this->getInitialValueIterationValues(submatrix, subNondeterministicChoiceIndices, b); - + // Solve the corresponding system of equations. if (linearEquationSolver != nullptr) { this->linearEquationSolver->solveEquationSystem(minimize, submatrix, x, b, subNondeterministicChoiceIndices); diff --git a/src/models/AbstractDeterministicModel.h b/src/models/AbstractDeterministicModel.h index aa34218ce..61bb58f3d 100644 --- a/src/models/AbstractDeterministicModel.h +++ b/src/models/AbstractDeterministicModel.h @@ -100,10 +100,12 @@ class AbstractDeterministicModel: public AbstractModel { AbstractModel::writeDotToStream(outStream, includeLabeling, subsystem, firstValue, secondValue, stateColoring, colors, scheduler, false); // Simply iterate over all transitions and draw the arrows with probability information attached. - for (auto const& transition : this->transitionMatrix) { - if (transition.value() != storm::utility::constGetZero()) { - if (subsystem == nullptr || subsystem->get(transition.column())) { - outStream << "\t" << transition.row() << " -> " << transition.column() << " [ label= \"" << transition.value() << "\" ];" << std::endl; + for (uint_fast64_t i = 0; i < this->transitionMatrix.getRowCount(); ++i) { + for (auto transitionIt = this->transitionMatrix.begin(i), transitionIte = this->transitionMatrix.end(i); transitionIt != transitionIte; ++transitionIt) { + if (*transitionIt != storm::utility::constGetZero()) { + if (subsystem == nullptr || subsystem->get(transitionIt.column())) { + outStream << "\t" << i << " -> " << transitionIt.column() << " [ label= \"" << *transitionIt << "\" ];" << std::endl; + } } } } diff --git a/src/models/AbstractNondeterministicModel.h b/src/models/AbstractNondeterministicModel.h index 10ab8bfdd..ca8a95308 100644 --- a/src/models/AbstractNondeterministicModel.h +++ b/src/models/AbstractNondeterministicModel.h @@ -144,10 +144,6 @@ class AbstractNondeterministicModel: public AbstractModel { virtual void writeDotToStream(std::ostream& outStream, bool includeLabeling = true, storm::storage::BitVector const* subsystem = nullptr, std::vector const* firstValue = nullptr, std::vector const* secondValue = nullptr, std::vector const* stateColoring = nullptr, std::vector const* colors = nullptr, std::vector* scheduler = nullptr, bool finalizeOutput = true) const override { AbstractModel::writeDotToStream(outStream, includeLabeling, subsystem, firstValue, secondValue, stateColoring, colors, scheduler, false); - - // Initialize the two iterators that we are going to use. - typename storm::storage::SparseMatrix::ConstRowsIterator transitionIt = this->getTransitionMatrix().begin(); - typename storm::storage::SparseMatrix::ConstRowsIterator transitionIte = this->getTransitionMatrix().begin(); // Write the probability distributions for all the states. for (uint_fast64_t state = 0, highestStateIndex = this->getNumberOfStates() - 1; state <= highestStateIndex; ++state) { @@ -190,10 +186,9 @@ class AbstractNondeterministicModel: public AbstractModel { outStream << ";" << std::endl; // Now draw all probabilitic arcs that belong to this nondeterminstic choice. - transitionIte.moveToNextRow(); - for (; transitionIt != transitionIte; ++transitionIt) { + for (auto transitionIt = this->getTransitionMatrix().begin(nondeterministicChoiceIndices[state] + rowCount), transitionIte = this->getTransitionMatrix().begin(nondeterministicChoiceIndices[state + 1]); transitionIt != transitionIte; ++transitionIt) { if (subsystem == nullptr || subsystem->get(transitionIt.column())) { - outStream << "\t\"" << state << "c" << row << "\" -> " << transitionIt.column() << " [ label= \"" << transitionIt.value() << "\" ]"; + outStream << "\t\"" << state << "c" << row << "\" -> " << transitionIt.column() << " [ label= \"" << *transitionIt << "\" ]"; // If we were given a scheduler to highlight, we do so now. if (scheduler != nullptr) { diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index eec7410c0..c841fa27d 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -75,14 +75,14 @@ public: * (row, column) in addition to the value itself. This is a const iterator in the sense that it is not possible to * modify the matrix with it. */ - class ConstRowsIterator { + class Iterator { public: /*! * Constructs an iterator over the elements of the given matrix. * * @param matrix The matrix on which this iterator operates. */ - ConstRowsIterator(SparseMatrix const& matrix, uint_fast64_t row = 0) : matrix(&matrix), posIndex(matrix.rowIndications[row]), rowIndex(row) { + Iterator(T* valuePtr, uint_fast64_t* columnPtr) : valuePtr(valuePtr), columnPtr(columnPtr) { // Intentionally left empty. } @@ -91,11 +91,9 @@ public: * * @returns A reference to itself. */ - ConstRowsIterator& operator++() { - ++posIndex; - if (posIndex >= matrix->rowIndications[rowIndex + 1]) { - ++rowIndex; - } + Iterator& operator++() { + ++valuePtr; + ++columnPtr; return *this; } @@ -105,8 +103,8 @@ public: * * @returns A reference to itself. */ - ConstRowsIterator& operator*() { - return *this; + T& operator*() { + return *valuePtr; } /*! @@ -116,8 +114,8 @@ public: * * @return True iff the given iterator points to the same index as the current iterator. */ - bool operator==(ConstRowsIterator const& other) const { - return this->posIndex == other.posIndex; + bool operator==(Iterator const& other) const { + return this->valuePtr == other.valuePtr; } /*! @@ -127,31 +125,19 @@ public: * * @return True iff the given iterator points to a differnent index as the current iterator. */ - bool operator!=(ConstRowsIterator const& other) const { - return this->posIndex != other.posIndex; + bool operator!=(Iterator const& other) const { + return this->valuePtr != other.valuePtr; } /*! * Assignment operator */ - ConstRowsIterator& operator=( const ConstRowsIterator& rhs) { - this->matrix = rhs.matrix; - this->posIndex = rhs.posIndex; - this->rowIndex = rhs.rowIndex; - + Iterator& operator=(Iterator const& rhs) { + this->valuePtr = rhs.valuePtr; + this->columnPtr = rhs.columnPtr; return *this; } - /*! - * Retrieves the row that is associated with the current non-zero element this iterator - * points to. - * - * @returns The row of the current non-zero element this iterator points to. - */ - uint_fast64_t row() const { - return this->rowIndex; - } - /*! * Retrieves the column that is associated with the current non-zero element this iterator * points to. @@ -159,15 +145,7 @@ public: * @returns The column of the current non-zero element this iterator points to. */ uint_fast64_t column() const { - return matrix->columnIndications[posIndex]; - } - - /*! - * Retrieves the internal index of this iterator. This index corresponds to the position of - * the current element in the vector of non-zero values of the matrix. - */ - uint_fast64_t index() const { - return this->posIndex; + return *columnPtr; } /*! @@ -175,54 +153,105 @@ public: * * @returns The value of the current non-zero element this iterator points to. */ - T const& value() const { - return matrix->valueStorage[posIndex]; + T& value() { + return *valuePtr; } - - /*! - * Moves the iterator to the beginning of the given row. - * - * @param row The row this iterator is to be moved to. - */ - void moveToRow(uint_fast64_t row) { - this->rowIndex = row; - this->posIndex = matrix->rowIndications[row]; +private: + T* valuePtr; + uint_fast64_t* columnPtr; + }; + + /*! + * Iterator class that is able to iterate over the non-zero elements of a matrix and return the position + * (row, column) in addition to the value itself. This is a const iterator in the sense that it is not possible to + * modify the matrix with it. + */ + class ConstIterator { + public: + /*! + * Constructs an iterator over the elements of the given matrix. + * + * @param matrix The matrix on which this iterator operates. + */ + ConstIterator(T const* valuePtr, uint_fast64_t const* columnPtr) : valuePtr(valuePtr), columnPtr(columnPtr) { + // Intentionally left empty. } - - /*! - * Moves the iterator to the beginning of the next row. - */ - void moveToNextRow() { - moveToRow(rowIndex + 1); + + /*! + * Moves the iterator the next non-zero element of the matrix. + * + * @returns A reference to itself. + */ + ConstIterator& operator++() { + ++valuePtr; + ++columnPtr; + return *this; } - + /*! - * Calculates the size of the current row + * Dereferencing operator for this iterator. Actually returns a reference to itself. This is + * needed, because the range-based for-loop in C++11 dereferences the iterator automatically. + * + * @returns A reference to itself. */ - uint_fast64_t rowSize() { - return (matrix->rowIndications[this->rowIndex + 1] - matrix->rowIndications[this->rowIndex]); + T const& operator*() { + return *valuePtr; } - + /*! - * Moves the column-pointer forward + * Comparison operator that compares the current iterator with the given one in terms of + * the indices they point to. Note that this does not check whether the iterators are + * interpreted over the same matrix. + * + * @return True iff the given iterator points to the same index as the current iterator. */ - void advance(uint_fast64_t count) { - this->posIndex += count; + bool operator==(ConstIterator const& other) const { + return this->valuePtr == other.valuePtr; + } + + /*! + * Comparison operator that compares the current iterator with the given one in terms of + * the indices they point to. Note that this does not check whether the iterators are + * interpreted over the same matrix. + * + * @return True iff the given iterator points to a differnent index as the current iterator. + */ + bool operator!=(ConstIterator const& other) const { + return this->valuePtr != other.valuePtr; } - private: - // A constant reference to the matrix this iterator is associated with. - SparseMatrix const* matrix; - // The current index in the list of all non-zero elements of the matrix this iterator points to. - uint_fast64_t posIndex; + /*! + * Assignment operator + */ + ConstIterator& operator=(ConstIterator const& rhs) { + this->valuePtr = rhs.valuePtr; + this->columnPtr = rhs.columnPtr; + return *this; + } - // The row of the element this iterator currently points to. - uint_fast64_t rowIndex; + /*! + * Retrieves the column that is associated with the current non-zero element this iterator + * points to. + * + * @returns The column of the current non-zero element this iterator points to. + */ + uint_fast64_t column() const { + return *columnPtr; + } + + /*! + * Retrieves the value of the current non-zero element this iterator points to. + * + * @returns The value of the current non-zero element this iterator points to. + */ + T const& value() { + return *valuePtr; + } + private: + T const* valuePtr; + uint_fast64_t const* columnPtr; }; - // Declare the iterator as a friend class to grant access to private data members of the matrix. - friend class ConstRowsIterator; - /*! * An enum representing the internal state of the Matrix * After creating the Matrix using the Constructor, the Object is in state UnInitialized. After @@ -1102,25 +1131,13 @@ public: #ifdef STORM_USE_TBB tbb::parallel_for(tbb::blocked_range(0, result.size()), tbbHelper_MatrixRowVectorScalarProduct, std::vector, T>(this, &vector, &result)); #else - // Initialize two iterators that - ConstRowsIterator matrixElementIt(*this); - ConstRowsIterator matrixElementIte(*this); - - // Iterate over all positions of the result vector and compute its value as the scalar - // product of the corresponding row with the input vector. - // Note that only the end iterator has to be moved by one row, because the other iterator - // is automatically moved forward one row by the inner loop. - for (auto& element : result) { - // Put the past-the-end iterator to the correct position. - matrixElementIte.moveToNextRow(); - - // Initialize the result to be 0. - element = storm::utility::constGetZero(); - - // Perform the scalar product. - for (; matrixElementIt != matrixElementIte; ++matrixElementIt) { - element += matrixElementIt.value() * vector[matrixElementIt.column()]; - } + auto elementIt = this->begin(); + for (uint_fast64_t i = 0; i < this->rowCount; ++i) { + result[i] = storm::utility::constGetZero(); + + for (auto elementIte = this->end(i); elementIt != elementIte; ++elementIt) { + result[i] += *elementIt * vector[elementIt.column()]; + } } #endif } @@ -1148,8 +1165,12 @@ public: * @returns An iterator to the elements of the matrix that cannot be used for modifying the * contents. */ - ConstRowsIterator begin(uint_fast64_t row = 0) const { - return ConstRowsIterator(*this, row); + Iterator begin(uint_fast64_t row = 0) { + return Iterator(this->valueStorage.data() + this->rowIndications[row], this->columnIndications.data() + this->rowIndications[row]); + } + + ConstIterator begin(uint_fast64_t row = 0) const { + return ConstIterator(this->valueStorage.data() + this->rowIndications[row], this->columnIndications.data() + this->rowIndications[row]); } /*! @@ -1157,8 +1178,12 @@ public: * * @returns A const iterator that points past the last element of the matrix. */ - ConstRowsIterator end() const { - return ConstRowsIterator(*this, this->rowCount); + Iterator end() { + return Iterator(this->valueStorage.data() + nonZeroEntryCount, nullptr); + } + + ConstIterator end() const { + return ConstIterator(this->valueStorage.data() + nonZeroEntryCount, nullptr); } /*! @@ -1167,8 +1192,12 @@ public: * @returns row The row past which this iterator has to point. * @returns A const iterator that points to the first element after the given row. */ - ConstRowsIterator end(uint_fast64_t row) const { - return ConstRowsIterator(*this, row + 1); + Iterator end(uint_fast64_t row) { + return Iterator(&this->valueStorage[0] + this->rowIndications[row + 1], nullptr); + } + + ConstIterator end(uint_fast64_t row) const { + return ConstIterator(&this->valueStorage[0] + this->rowIndications[row + 1], nullptr); } /*! diff --git a/src/utility/vector.h b/src/utility/vector.h index e11ab0583..0ee5033d2 100644 --- a/src/utility/vector.h +++ b/src/utility/vector.h @@ -143,7 +143,7 @@ void selectVectorValuesRepeatedly(std::vector& vector, storm::storage::BitVec */ template void subtractFromConstantOneVector(std::vector& vector) { - for (auto element : vector) { + for (auto& element : vector) { element = storm::utility::constGetOne() - element; } }