Added iterator functionality to bit vector. Minor cosmetics here and there.

src/models/backward_transitions.h

@@ -100,7 +100,6 @@ public:
 		return this->predecessor_list + this->state_indices_list[state];
 	}
 
-
 	/*!
 	 * Returns an iterator referring to the element after the predecessors of
 	 * the given state.

src/models/dtmc.h

@@ -38,9 +38,8 @@ public:
 	 * @param state_labeling The labeling that assigns a set of atomic
 	 * propositions to each state.
 	 */
-	Dtmc(mrmc::sparse::StaticSparseMatrix<T>* probability_matrix,
-			mrmc::models::AtomicPropositionsLabeling* state_labeling) :
-				backward_transitions(probability_matrix) {
+	Dtmc(mrmc::sparse::StaticSparseMatrix<T>* probability_matrix, mrmc::models::AtomicPropositionsLabeling* state_labeling)
+			: backward_transitions(probability_matrix) {
 		this->probability_matrix = probability_matrix;
 		this->state_labeling = state_labeling;
 	}
@@ -58,7 +57,6 @@ public:
 	//! Destructor
 	/*!
 	 * Destructor. Frees the matrix and labeling associated with this DTMC.
-	 *
 	 */
 	~Dtmc() {
 		if (this->probability_matrix != nullptr) {

src/mrmc-cpp.cpp

@@ -66,6 +66,8 @@ int main(const int argc, const char* argv[]) {
 	mrmc::models::AtomicPropositionsLabeling* labeling = mrmc::parser::read_lab_file(probMatrix->getRowCount(), s->getString("labfile").c_str());
 	mrmc::models::Dtmc<double> dtmc(probMatrix, labeling);
 
+	dtmc.printModelInformationToStream(std::cout);
+
 	if (s != nullptr) {
 		delete s;
 	}

src/parser/read_lab_file.cpp

@@ -19,6 +19,8 @@
 #include <pantheios/pantheios.hpp>
 #include <pantheios/inserters/integer.hpp>
 
+#include <iostream>
+
 #ifdef WIN32
 #	define STRTOK_FUNC strtok_s
 #else
@@ -172,7 +174,6 @@ mrmc::models::AtomicPropositionsLabeling * read_lab_file(int node_count, const c
          }
          result->addAtomicPropositionToState(token, static_cast<uint_fast64_t>(node));
       } while (token != NULL);
-
    }
 
    fclose(P);

src/vector/bitvector.h

@@ -13,6 +13,8 @@
 #include "src/exceptions/invalid_argument.h"
 #include "src/exceptions/out_of_range.h"
 
+#include <iostream>
+
 namespace mrmc {
 
 namespace vector {
@@ -23,14 +25,39 @@ namespace vector {
  Does NOT perform index bound checks!
  */
 class BitVector {
- public:
+
+	class constIndexIterator {
+		constIndexIterator(uint_fast64_t* bucketPtr, uint_fast64_t* endBucketPtr) : bucketPtr(bucketPtr), endBucketPtr(endBucketPtr), offset(0), currentBitInByte(0) { }
+		constIndexIterator& operator++() {
+			do {
+				uint_fast64_t remainingInBucket = *bucketPtr >> ++currentBitInByte;
+				if (remainingInBucket != 0) {
+					while ((remainingInBucket & 1) == 0) {
+						remainingInBucket >>= 1;
+						++currentBitInByte;
+					}
+				}
+				offset <<= 6; ++bucketPtr; currentBitInByte = 0;
+			} while (bucketPtr != endBucketPtr);
+			return *this;
+		}
+		uint_fast64_t operator*() { return offset + currentBitInByte; }
+		bool operator!=(constIndexIterator& rhs) { return bucketPtr != rhs.bucketPtr; }
+	private:
+		uint_fast64_t* bucketPtr;
+		uint_fast64_t* endBucketPtr;
+		uint_fast64_t offset;
+		uint_fast8_t currentBitInByte;
+	};
+
+public:
 	//! Constructor
 	/*!
 	 \param initial_length The initial size of the boolean Array. Can be changed later on via BitVector::resize()
 	 */
 	BitVector(uint_fast64_t initial_length) {
-		bucket_count = initial_length / 64;
-		if (initial_length % 64 != 0) {
+		bucket_count = initial_length >> 6;
+		if ((initial_length & mod64mask) != 0) {
 			++bucket_count;
 		}
 		bucket_array = new uint_fast64_t[bucket_count]();
@@ -46,11 +73,12 @@ class BitVector {
 	 Copy Constructor. Creates an exact copy of the source bit vector bv. Modification of either bit vector does not affect the other.
 	 @param bv A reference to the bit vector that should be copied from
 	 */
-	BitVector(const BitVector &bv) : bucket_count(bv.bucket_count)
-	{
+	BitVector(const BitVector &bv) :
+			bucket_count(bv.bucket_count) {
 		pantheios::log_DEBUG("BitVector::CopyCTor: Using Copy() Ctor.");
 		bucket_array = new uint_fast64_t[bucket_count]();
-		memcpy(bucket_array, bv.bucket_array, sizeof(uint_fast64_t) * bucket_count);
+		memcpy(bucket_array, bv.bucket_array,
+				sizeof(uint_fast64_t) * bucket_count);
 	}
 
 	~BitVector() {
@@ -63,11 +91,13 @@ class BitVector {
 		uint_fast64_t* tempArray = new uint_fast64_t[new_length]();
 
 		// 64 bit/entries per uint_fast64_t
-		uint_fast64_t copySize = (new_length <= (bucket_count * 64)) ? (new_length/64) : (bucket_count);
+		uint_fast64_t copySize =
+				(new_length <= (bucket_count << 6)) ?
+						(new_length >> 6) : (bucket_count);
 		memcpy(tempArray, bucket_array, sizeof(uint_fast64_t) * copySize);
 
-		bucket_count = new_length / 64;
-		if (new_length % 64 != 0) {
+		bucket_count = new_length >> 6;
+		if ((new_length & mod64mask) != 0) {
 			++bucket_count;
 		}
 
@@ -76,12 +106,12 @@ class BitVector {
 	}
 
 	void set(const uint_fast64_t index, const bool value) {
-		uint_fast64_t bucket = index / 64;
+		uint_fast64_t bucket = index >> 6;
 		// Taking the step with mask is crucial as we NEED a 64bit shift, not a 32bit one.
 		// MSVC: C4334, use 1i64 or cast to __int64.
 		// result of 32-bit shift implicitly converted to 64 bits (was 64-bit shift intended?)
 		uint_fast64_t mask = 1;
-		mask = mask << (index % 64);
+		mask = mask << (index & mod64mask);
 		if (value) {
 			bucket_array[bucket] |= mask;
 		} else {
@@ -90,19 +120,21 @@ class BitVector {
 	}
 
 	bool get(const uint_fast64_t index) {
-		uint_fast64_t bucket = index / 64;
+		uint_fast64_t bucket = index >> 6;
 		// Taking the step with mask is crucial as we NEED a 64bit shift, not a 32bit one.
 		// MSVC: C4334, use 1i64 or cast to __int64.
 		// result of 32-bit shift implicitly converted to 64 bits (was 64-bit shift intended?)
 		uint_fast64_t mask = 1;
-		mask = mask << (index % 64);
+		mask = mask << (index & mod64mask);
 		return ((bucket_array[bucket] & mask) == mask);
 	}
 
 	// Operators
 	BitVector operator &(BitVector const &bv) {
-		uint_fast64_t minSize = (bv.bucket_count < this->bucket_count) ? bv.bucket_count : this->bucket_count;
-		BitVector result(minSize * 64);
+		uint_fast64_t minSize =
+				(bv.bucket_count < this->bucket_count) ?
+						bv.bucket_count : this->bucket_count;
+		BitVector result(minSize << 6);
 		for (uint_fast64_t i = 0; i < minSize; ++i) {
 			result.bucket_array[i] = this->bucket_array[i] & bv.bucket_array[i];
 		}
@@ -110,8 +142,10 @@ class BitVector {
 		return result;
 	}
 	BitVector operator |(BitVector const &bv) {
-		uint_fast64_t minSize = (bv.bucket_count < this->bucket_count) ? bv.bucket_count : this->bucket_count;
-		BitVector result(minSize * 64);
+		uint_fast64_t minSize =
+				(bv.bucket_count < this->bucket_count) ?
+						bv.bucket_count : this->bucket_count;
+		BitVector result(minSize << 6);
 		for (uint_fast64_t i = 0; i < minSize; ++i) {
 			result.bucket_array[i] = this->bucket_array[i] | bv.bucket_array[i];
 		}
@@ -120,8 +154,10 @@ class BitVector {
 	}
 
 	BitVector operator ^(BitVector const &bv) {
-		uint_fast64_t minSize = (bv.bucket_count < this->bucket_count) ? bv.bucket_count : this->bucket_count;
-		BitVector result(minSize * 64);
+		uint_fast64_t minSize =
+				(bv.bucket_count < this->bucket_count) ?
+						bv.bucket_count : this->bucket_count;
+		BitVector result(minSize << 6);
 		for (uint_fast64_t i = 0; i < minSize; ++i) {
 			result.bucket_array[i] = this->bucket_array[i] ^ bv.bucket_array[i];
 		}
@@ -130,7 +166,7 @@ class BitVector {
 	}
 
 	BitVector operator ~() {
-		BitVector result(this->bucket_count * 64);
+		BitVector result(this->bucket_count << 6);
 		for (uint_fast64_t i = 0; i < this->bucket_count; ++i) {
 			result.bucket_array[i] = ~this->bucket_array[i];
 		}
@@ -138,15 +174,30 @@ class BitVector {
 		return result;
 	}
 
+	BitVector implies(BitVector& other) {
+		if (other.getSize() != this->getSize()) {
+			pantheios::log_ERROR(
+					"BitVector::implies: Throwing invalid argument exception for connecting bit vectors of different size.");
+			throw mrmc::exceptions::invalid_argument();
+		}
+		BitVector result(this->bucket_count << 6);
+		for (uint_fast64_t i = 0; i < this->bucket_count; ++i) {
+			result.bucket_array[i] = ~this->bucket_array[i]
+					| other.bucket_array[i];
+		}
+
+		return result;
+	}
+
 	/*!
 	 * Returns the number of bits that are set (to one) in this bit vector.
 	 * @return The number of bits that are set (to one) in this bit vector.
 	 */
 	uint_fast64_t getNumberOfSetBits() {
 		uint_fast64_t set_bits = 0;
-		for (uint_fast64_t i = 0; i < bucket_count; i++) {
+		for (uint_fast64_t i = 0; i < bucket_count; ++i) {
 #ifdef __GNUG__ // check if we are using g++ and use built-in function if available
-			set_bits += __builtin_popcount (this->bucket_array[i]);
+			set_bits += __builtin_popcountll(this->bucket_array[i]);
 #else
 			uint_fast32_t cnt;
 			uint_fast64_t bitset = this->bucket_array[i];
@@ -159,6 +210,10 @@ class BitVector {
 		return set_bits;
 	}
 
+	uint_fast64_t getSize() {
+		return bucket_count;
+	}
+
 	/*!
 	 * Returns the size of the bit vector in memory measured in bytes.
 	 * @return The size of the bit vector in memory measured in bytes.
@@ -167,12 +222,14 @@ class BitVector {
 		return sizeof(*this) + sizeof(uint_fast64_t) * bucket_count;
 	}
 
- private:
+private:
 	uint_fast64_t bucket_count;
 
 	/*! Array containing the boolean bits for each node, 64bits/64nodes per element */
 	uint_fast64_t* bucket_array;
 
+	static const uint_fast64_t mod64mask = (1 << 6) - 1;
+
 };
 
 } // namespace vector