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.

12 years ago · 73ab4a78a9
2 changed files with 84 additions and 16 deletions
--- a/src/models/GraphTransitions.h
+++ b/src/models/GraphTransitions.h
@ -40,7 +40,7 @@ public:
 	 * of the backwards transition relation.
 	 */
 	GraphTransitions(std::shared_ptr<storm::storage::SparseMatrix<T>> 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<storm::storage::SparseMatrix<T>> transitionMatrix, std::shared_ptr<std::vector<uint_fast64_t>> 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<storm::storage::SparseMatrix<T>> 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<storm::storage::SparseMatrix<T>> transitionMatrix, std::shared_ptr<std::vector<uint_fast64_t>> 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,17 +148,55 @@ private:
 	 * matrix.
 	 */
 	void initializeBackward(std::shared_ptr<storm::storage::SparseMatrix<T>> 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) {
+			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 (auto rowIt = transitionMatrix->beginConstColumnIterator(i); rowIt != transitionMatrix->endConstColumnIterator(i); ++rowIt) {
+				this->successorList[nextIndicesList[*rowIt]++] = i;
+			}
+		}
+
+		// Now we can dispose of the auxiliary array.
+		delete[] nextIndicesList;
+	}
+
+	void initializeBackward(std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix, std::shared_ptr<std::vector<uint_fast64_t>> 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++) {
@ -140,7 +206,7 @@ private:
 		// 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.
@ -150,10 +216,12 @@ 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 (auto rowIt = transitionMatrix->beginConstColumnIterator(i); rowIt != transitionMatrix->endConstColumnIterator(i); ++rowIt) {
+			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;
@ -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
--- 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<T> const & getStoragePointer() const {
+	std::vector<T> 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<uint_fast64_t> const & getRowIndicationsPointer() const {
+	std::vector<uint_fast64_t> 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<uint_fast64_t> const & getColumnIndicationsPointer() const {
+	std::vector<uint_fast64_t> const& getColumnIndications() const {
 		return columnIndications;
 	}