Fixed includes for graph transitions class. Added index iteration functionality to the bit vector class.

src/models/AtomicPropositionsLabeling.h

@@ -188,6 +188,12 @@ public:
 				<< this->singleLabelings[ap.second]->getNumberOfSetBits();
 			out << " state(s)" << std::endl;
 		}
+		for(int i = 0; i < apCountMax; ++i) {
+			std::cout << "iterator " << i << std::endl;
+			for(auto it = this->singleLabelings[i]->begin(); it != this->singleLabelings[i]->end(); ++it) {
+				out << "next value: " << *it << std::endl;
+			}
+		}
 	}
 
 private:

src/models/Dtmc.h

@@ -11,7 +11,7 @@
 #include <ostream>
 
 #include "AtomicPropositionsLabeling.h"
-#include "BackwardTransitions.h"
+#include "GraphTransitions.h"
 #include "src/storage/SquareSparseMatrix.h"
 
 namespace mrmc {
@@ -36,7 +36,7 @@ public:
 	 * propositions to each state.
 	 */
 	Dtmc(mrmc::storage::SquareSparseMatrix<T>* probability_matrix, mrmc::models::AtomicPropositionsLabeling* state_labeling)
-			: backward_transitions(probability_matrix) {
+			: backward_transitions(probability_matrix, false) {
 		this->probability_matrix = probability_matrix;
 		this->state_labeling = state_labeling;
 	}
@@ -118,9 +118,9 @@ private:
 
 	/*!
 	 * A data structure that stores the predecessors for all states. This is
-	 * needed for a backwards search.
+	 * needed for backwards directed searches.
 	 */
-	mrmc::models::BackwardTransitions<T> backward_transitions;
+	mrmc::models::GraphTransitions<T> backward_transitions;
 };
 
 } // namespace models

src/models/GraphTransitions.h

@@ -5,12 +5,13 @@
  *      Author: Christian Dehnert
  */
 
-#ifndef BACKWARD_TRANSITIONS_H_
-#define BACKWARD_TRANSITIONS_H_
+#ifndef GRAPHTRANSITIONS_H_
+#define BACKWARDTRANSITIONS_H_
 
-#include <iostream>
 #include "src/storage/SquareSparseMatrix.h"
 
+#include <string.h>
+
 namespace mrmc {
 
 namespace models {
@@ -20,7 +21,7 @@ namespace models {
  * given size.
  */
 template <class T>
-class BackwardTransitions {
+class GraphTransitions {
 
 public:
 	/*!
@@ -30,13 +31,84 @@ public:
 
 	//! Constructor
 	/*!
-	 * Constructs a backward transitions object from the given sparse matrix
-	 * representing the (forward) transition relation.
-	 * @param transition_matrix The (0-based) matrix representing the transition
+	 * Constructs an object representing the graph structure of the given
+	 * transition relation, which is given by a sparse matrix.
+	 * @param transitionMatrix The (0-based) matrix representing the transition
 	 * relation.
+	 * @param forward If set to true, this objects will store the graph structure
+	 * of the backwards transition relation.
+	 */
+	GraphTransitions(mrmc::storage::SquareSparseMatrix<T>* transitionMatrix, bool forward)
+			: numberOfStates(transitionMatrix->getRowCount()), numberOfNonZeroTransitions(transitionMatrix->getNonZeroEntryCount()), predecessor_list(nullptr), state_indices_list(nullptr) {
+		if (forward) {
+			this->initializeForward(transitionMatrix);
+		} else {
+			this->initializeBackward(transitionMatrix);
+		}
+	}
+
+	//! Destructor
+	/*!
+	 * Destructor. Frees the internal storage.
+	 */
+	~GraphTransitions() {
+		if (this->predecessor_list != nullptr) {
+			delete[] this->predecessor_list;
+		}
+		if (this->state_indices_list != nullptr) {
+			delete[] this->state_indices_list;
+		}
+	}
+
+	/*!
+	 * Returns an iterator to the predecessors of the given states.
+	 * @param state The state for which to get the predecessor iterator.
+	 * @return An iterator to the predecessors of the given states.
+	 */
+	state_predecessor_iterator beginStatePredecessorIterator(uint_fast64_t state) const {
+		return this->predecessor_list + this->state_indices_list[state];
+	}
+
+	/*!
+	 * Returns an iterator referring to the element after the predecessors of
+	 * the given state.
+	 * @param row The state for which to get the iterator.
+	 * @return An iterator referring to the element after the predecessors of
+	 * the given state.
+	 */
+	state_predecessor_iterator endStatePredecessorIterator(uint_fast64_t state) const {
+		return this->predecessor_list + this->state_indices_list[state + 1];
+	}
+
+private:
+
+	/*!
+	 * Initializes this graph transitions object using the forward transition
+	 * relation given by means of a sparse matrix.
+	 */
+	void initializeForward(mrmc::storage::SquareSparseMatrix<T>* transitionMatrix) {
+		this->predecessor_list = new uint_fast64_t[numberOfNonZeroTransitions];
+		this->state_indices_list = new uint_fast64_t[numberOfStates + 1];
+
+		// First, we copy the index list from the sparse matrix as this will
+		// stay the same.
+		memcpy(this->state_indices_list, transitionMatrix->getRowIndicationsPointer(), numberOfStates + 1);
+
+		// 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->beginConstColumnNoDiagIterator(i); rowIt != transitionMatrix->endConstColumnNoDiagIterator(i); ++rowIt) {
+				this->state_indices_list[currentNonZeroElement++] = *rowIt;
+			}
+		}
+	}
+
+	/*!
+	 * Initializes this graph transitions object using the backwards transition
+	 * relation, whose forward transition relation is given by means of a sparse
+	 * matrix.
 	 */
-	BackwardTransitions(mrmc::storage::SquareSparseMatrix<T>* transitionMatrix)
-			: numberOfStates(transitionMatrix->getRowCount()), numberOfNonZeroTransitions(transitionMatrix->getNonZeroEntryCount()) {
+	void initializeBackward(mrmc::storage::SquareSparseMatrix<T>* transitionMatrix) {
 		this->predecessor_list = new uint_fast64_t[numberOfNonZeroTransitions];
 		this->state_indices_list = new uint_fast64_t[numberOfStates + 1];
 
@@ -76,40 +148,6 @@ public:
 		delete[] next_state_index_list;
 	}
 
-	//! Destructor
-	/*!
-	 * Destructor. Frees the internal storage.
-	 */
-	~BackwardTransitions() {
-		if (this->predecessor_list != nullptr) {
-			delete[] this->predecessor_list;
-		}
-		if (this->state_indices_list != nullptr) {
-			delete[] this->state_indices_list;
-		}
-	}
-
-	/*!
-	 * Returns an iterator to the predecessors of the given states.
-	 * @param state The state for which to get the predecessor iterator.
-	 * @return An iterator to the predecessors of the given states.
-	 */
-	state_predecessor_iterator beginStatePredecessorIterator(uint_fast64_t state) const {
-		return this->predecessor_list + this->state_indices_list[state];
-	}
-
-	/*!
-	 * Returns an iterator referring to the element after the predecessors of
-	 * the given state.
-	 * @param row The state for which to get the iterator.
-	 * @return An iterator referring to the element after the predecessors of
-	 * the given state.
-	 */
-	state_predecessor_iterator endStatePredecessorIterator(uint_fast64_t state) const {
-		return this->predecessor_list + this->state_indices_list[state + 1];
-	}
-
-private:
 	/*! A list of predecessors for *all* states. */
 	uint_fast64_t* predecessor_list;
 
@@ -136,4 +174,4 @@ private:
 
 } // namespace mrmc
 
-#endif /* BACKWARD_TRANSITIONS_H_ */
+#endif /* GRAPHTRANSITIONS_H_ */

src/storage/BitVector.h

@@ -16,6 +16,8 @@
 
 extern log4cplus::Logger logger;
 
+#include <iostream>
+
 namespace mrmc {
 
 namespace storage {
@@ -26,28 +28,85 @@ namespace storage {
 class BitVector {
 
 public:
+	/*!
+	 * A class that enables iterating over the indices of the bit vector whose
+	 * bits are set to true. Note that this is a const iterator, which cannot
+	 * alter the bit vector.
+	 */
 	class constIndexIterator {
 	public:
-		constIndexIterator(uint_fast64_t* bucketPtr, uint_fast64_t* endBucketPtr) : bucketPtr(bucketPtr), endBucketPtr(endBucketPtr), offset(0), currentBitInByte(0) { }
+		/*!
+		 * Constructs a const iterator using the given pointer to the first bucket
+		 * as well as the given pointer to the element past the bucket array.
+		 * @param bucketPtr A pointer to the first bucket of the bucket array.
+		 * @param endBucketPtr A pointer to the element past the bucket array.
+		 * This is needed to ensure iteration is stopped properly.
+		 */
+		constIndexIterator(uint64_t* bucketPtr, uint64_t* endBucketPtr) : bucketPtr(bucketPtr), endBucketPtr(endBucketPtr), offset(0), currentBitInByte(0) {
+			// If the first bit is not set, then we actually need to find the
+			// position of the first bit that is set.
+			if ((*bucketPtr & 1) == 0) {
+				++(*this);
+			}
+		}
+
+		/*!
+		 * Constructs a const iterator from the given bucketPtr. As the other members
+		 * are initialized to zero, this should only be used for constructing iterators
+		 * that are to be compared with a fully initialized iterator, not for creating
+		 * a iterator to be used for actually iterating.
+		 */
+		constIndexIterator(uint64_t* bucketPtr) : bucketPtr(bucketPtr), endBucketPtr(nullptr), offset(0), currentBitInByte(0) { }
+
+		/*!
+		 * Increases the position of the iterator to the position of the next bit that
+		 * is set to true.
+		 * @return A reference to this iterator.
+		 */
 		constIndexIterator& operator++() {
 			do {
-				uint_fast64_t remainingInBucket = *bucketPtr >> ++currentBitInByte;
+				// Compute the remaining bucket content by a right shift
+				// to the current bit.
+				uint_fast64_t remainingInBucket = *bucketPtr >> currentBitInByte++;
+				// Check if there is at least one bit in the remainder of the bucket
+				// that is set to true.
 				if (remainingInBucket != 0) {
+					// Find that bit.
 					while ((remainingInBucket & 1) == 0) {
 						remainingInBucket >>= 1;
 						++currentBitInByte;
 					}
+					return *this;
 				}
-				offset <<= 6; ++bucketPtr; currentBitInByte = 0;
+
+				// Advance to the next bucket.
+				offset += 64; ++bucketPtr; currentBitInByte = 0;
 			} while (bucketPtr != endBucketPtr);
 			return *this;
 		}
-		uint_fast64_t operator*() { return offset + currentBitInByte; }
-		bool operator!=(constIndexIterator& rhs) { return bucketPtr != rhs.bucketPtr; }
+
+		/*!
+		 * Returns the index of the current bit that is set to true.
+		 * @return The index of the current bit that is set to true.
+		 */
+		uint_fast64_t operator*() const { return offset + currentBitInByte; }
+
+		/*!
+		 * Compares the iterator with another iterator to determine whether
+		 * the iteration process has reached the end.
+		 */
+		bool operator!=(const constIndexIterator& rhs) const { return bucketPtr != rhs.bucketPtr; }
 	private:
-		uint_fast64_t* bucketPtr;
-		uint_fast64_t* endBucketPtr;
+		/*! A pointer to the current bucket. */
+		uint64_t* bucketPtr;
+
+		/*! A pointer to the element after the last bucket. */
+		uint64_t* endBucketPtr;
+
+		/*! The number of bits in this bit vector before the current bucket. */
 		uint_fast64_t offset;
+
+		/*! The index of the current bit in the current bucket. */
 		uint_fast8_t currentBitInByte;
 	};
 
@@ -286,7 +345,7 @@ public:
 	 * Returns an iterator pointing at the element past the bit vector.
 	 */
 	constIndexIterator end() const {
-		return constIndexIterator(this->bucketArray + bucketCount, 0);
+		return constIndexIterator(this->bucketArray + bucketCount);
 	}
 
 private: