From 73ab4a78a973dc1a0eafc20fd3a579adb2d50de4 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 11 Feb 2013 20:12:28 +0100 Subject: [PATCH] Renamed methods get*Pointer in sparse matrix class, because they do not return a pointer. Added initial versions of forward/backward graph transition creation for nondeterministic models. --- src/models/GraphTransitions.h | 94 ++++++++++++++++++++++++++++++----- src/storage/SparseMatrix.h | 6 +-- 2 files changed, 84 insertions(+), 16 deletions(-) diff --git a/src/models/GraphTransitions.h b/src/models/GraphTransitions.h index 64d5c65cd..6f4da36f1 100644 --- a/src/models/GraphTransitions.h +++ b/src/models/GraphTransitions.h @@ -40,7 +40,7 @@ public: * of the backwards transition relation. */ GraphTransitions(std::shared_ptr> transitionMatrix, bool forward) - : successorList(nullptr), stateIndications(nullptr), numberOfStates(transitionMatrix->getColumnCount()), numberOfNonZeroTransitions(transitionMatrix->getNonZeroEntryCount()) { + : successorList(nullptr), stateIndications(nullptr), numberOfStates(transitionMatrix->getColumnCount()), numberOfTransitions(transitionMatrix->getNonZeroEntryCount()) { if (forward) { this->initializeForward(transitionMatrix); } else { @@ -48,6 +48,15 @@ public: } } + GraphTransitions(std::shared_ptr> transitionMatrix, std::shared_ptr> choiceIndices, bool forward) + : successorList(nullptr), stateIndications(nullptr), numberOfStates(transitionMatrix->getColumnCount()), numberOfTransitions(transitionMatrix->getNonZeroEntryCount()) { + if (forward) { + this->initializeForward(transitionMatrix, choiceIndices); + } else { + this->initializeBackward(transitionMatrix, choiceIndices); + } + } + //! Destructor /*! * Destructor. Frees the internal storage. @@ -67,7 +76,7 @@ public: * measured in bytes. */ virtual uint_fast64_t getSizeInMemory() const { - uint_fast64_t result = sizeof(this) + (numberOfStates + numberOfNonZeroTransitions + 1) * sizeof(uint_fast64_t); + uint_fast64_t result = sizeof(this) + (numberOfStates + numberOfTransitions + 1) * sizeof(uint_fast64_t); return result; } @@ -98,18 +107,37 @@ private: * relation given by means of a sparse matrix. */ void initializeForward(std::shared_ptr> transitionMatrix) { - this->successorList = new uint_fast64_t[numberOfNonZeroTransitions]; + this->successorList = new uint_fast64_t[numberOfTransitions]; this->stateIndications = new uint_fast64_t[numberOfStates + 1]; // First, we copy the index list from the sparse matrix as this will // stay the same. - std::copy(transitionMatrix->getRowIndicationsPointer().begin(), transitionMatrix->getRowIndicationsPointer().end(), this->stateIndications); + std::copy(transitionMatrix->getRowIndications().begin(), transitionMatrix->getRowIndications().end(), this->stateIndications); // Now we can iterate over all rows of the transition matrix and record // the target state. for (uint_fast64_t i = 0, currentNonZeroElement = 0; i < numberOfStates; i++) { for (auto rowIt = transitionMatrix->beginConstColumnIterator(i); rowIt != transitionMatrix->endConstColumnIterator(i); ++rowIt) { - this->stateIndications[currentNonZeroElement++] = *rowIt; + this->successorList[currentNonZeroElement++] = *rowIt; + } + } + } + + void initializeForward(std::shared_ptr> transitionMatrix, std::shared_ptr> choiceIndices) { + this->successorList = new uint_fast64_t[numberOfTransitions]; + this->stateIndications = new uint_fast64_t[numberOfStates + 1]; + + for (uint_fast64_t i = 0; i < numberOfStates; ++i) { + this->stateIndications[i] = transitionMatrix->getRowIndications().at(choiceIndices->at(i)); + } + + // Now we can iterate over all rows of the transition matrix and record + // the target state. + for (uint_fast64_t i = 0, currentNonZeroElement = 0; i < numberOfStates; i++) { + for (uint_fast64_t j = choiceIndices->at(i); j < choiceIndices->at(i + 1); ++j) { + for (auto rowIt = transitionMatrix->beginConstColumnIterator(j); rowIt != transitionMatrix->endConstColumnIterator(j); ++rowIt) { + this->successorList[currentNonZeroElement++] = *rowIt; + } } } } @@ -120,27 +148,25 @@ private: * matrix. */ void initializeBackward(std::shared_ptr> transitionMatrix) { - this->successorList = new uint_fast64_t[numberOfNonZeroTransitions]; + this->successorList = new uint_fast64_t[numberOfTransitions]; this->stateIndications = new uint_fast64_t[numberOfStates + 1](); // First, we need to count how many backward transitions each state has. - // NOTE: We disregard the diagonal here, as we only consider "true" - // predecessors. - for (uint_fast64_t i = 0; i < numberOfStates; i++) { + for (uint_fast64_t i = 0; i < numberOfStates; ++i) { for (auto rowIt = transitionMatrix->beginConstColumnIterator(i); rowIt != transitionMatrix->endConstColumnIterator(i); ++rowIt) { this->stateIndications[*rowIt + 1]++; } } // Now compute the accumulated offsets. - for (uint_fast64_t i = 1; i < numberOfStates; i++) { + for (uint_fast64_t i = 1; i < numberOfStates; ++i) { this->stateIndications[i] = this->stateIndications[i - 1] + this->stateIndications[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]. - this->stateIndications[numberOfStates] = numberOfNonZeroTransitions; + this->stateIndications[numberOfStates] = numberOfTransitions; // Create an array that stores the next index for each state. Initially // this corresponds to the previously computed accumulated offsets. @@ -149,7 +175,7 @@ private: // 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++) { + for (uint_fast64_t i = 0; i < numberOfStates; ++i) { for (auto rowIt = transitionMatrix->beginConstColumnIterator(i); rowIt != transitionMatrix->endConstColumnIterator(i); ++rowIt) { this->successorList[nextIndicesList[*rowIt]++] = i; } @@ -159,6 +185,48 @@ private: delete[] nextIndicesList; } + void initializeBackward(std::shared_ptr> transitionMatrix, std::shared_ptr> choiceIndices) { + this->successorList = new uint_fast64_t[numberOfTransitions]; + this->stateIndications = new uint_fast64_t[numberOfStates + 1](); + + // First, we need to count how many backward transitions each state has. + for (uint_fast64_t i = 0; i < numberOfStates; ++i) { + for (uint_fast64_t j = choiceIndices->at(i); j < choiceIndices->at(i + 1); ++j) { + for (auto rowIt = transitionMatrix->beginConstColumnIterator(j); rowIt != transitionMatrix->endConstColumnIterator(j); ++rowIt) { + this->stateIndications[*rowIt + 1]++; + } + } + } + + // Now compute the accumulated offsets. + for (uint_fast64_t i = 1; i < numberOfStates; i++) { + this->stateIndications[i] = this->stateIndications[i - 1] + this->stateIndications[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]. + this->stateIndications[numberOfStates] = numberOfTransitions; + + // Create an array that stores the next index for each state. Initially + // this corresponds to the previously computed accumulated offsets. + uint_fast64_t* nextIndicesList = new uint_fast64_t[numberOfStates]; + std::copy(stateIndications, stateIndications + numberOfStates, nextIndicesList); + + // 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++) { + for (uint_fast64_t j = choiceIndices->at(i); j < choiceIndices->at(i + 1); ++j) { + for (auto rowIt = transitionMatrix->beginConstColumnIterator(j); rowIt != transitionMatrix->endConstColumnIterator(j); ++rowIt) { + this->successorList[nextIndicesList[*rowIt]++] = i; + } + } + } + + // Now we can dispose of the auxiliary array. + delete[] nextIndicesList; + } + /*! A list of successors for *all* states. */ uint_fast64_t* successorList; @@ -178,7 +246,7 @@ private: * Store the number of non-zero transition entries to determine the highest * index at which the predecessor_list may be accessed. */ - uint_fast64_t numberOfNonZeroTransitions; + uint_fast64_t numberOfTransitions; }; } // namespace models diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index 94d663d3b..a35df8b47 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -476,7 +476,7 @@ public: * Returns a pointer to the value storage of the matrix. * @return A pointer to the value storage of the matrix. */ - std::vector const & getStoragePointer() const { + std::vector const& getStorage() const { return valueStorage; } @@ -486,7 +486,7 @@ public: * @return A pointer to the array that stores the start indices of non-zero * entries in the value storage for each row. */ - std::vector const & getRowIndicationsPointer() const { + std::vector const& getRowIndications() const { return rowIndications; } @@ -496,7 +496,7 @@ public: * @return A pointer to an array that stores the column of each non-zero * element. */ - std::vector const & getColumnIndicationsPointer() const { + std::vector const& getColumnIndications() const { return columnIndications; }