From 5a8c2a8d0e55b4175b2058262611ffeaa7f58164 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 23 Nov 2012 13:05:09 +0100 Subject: [PATCH] Added iterator functionality to bit vector. Minor cosmetics here and there. --- src/models/backward_transitions.h | 1 - src/models/dtmc.h | 6 +- src/mrmc-cpp.cpp | 2 + src/parser/read_lab_file.cpp | 3 +- src/vector/bitvector.h | 125 ++++++++++++++++++++++-------- 5 files changed, 97 insertions(+), 40 deletions(-) diff --git a/src/models/backward_transitions.h b/src/models/backward_transitions.h index 2f6d3d49a..52311d3f5 100644 --- a/src/models/backward_transitions.h +++ b/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. diff --git a/src/models/dtmc.h b/src/models/dtmc.h index c01e341b1..5a2bb8fd0 100644 --- a/src/models/dtmc.h +++ b/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* probability_matrix, - mrmc::models::AtomicPropositionsLabeling* state_labeling) : - backward_transitions(probability_matrix) { + Dtmc(mrmc::sparse::StaticSparseMatrix* 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) { diff --git a/src/mrmc-cpp.cpp b/src/mrmc-cpp.cpp index 2dbee8c29..670920765 100644 --- a/src/mrmc-cpp.cpp +++ b/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 dtmc(probMatrix, labeling); + dtmc.printModelInformationToStream(std::cout); + if (s != nullptr) { delete s; } diff --git a/src/parser/read_lab_file.cpp b/src/parser/read_lab_file.cpp index 35210d5a6..99dfc6fa5 100644 --- a/src/parser/read_lab_file.cpp +++ b/src/parser/read_lab_file.cpp @@ -19,6 +19,8 @@ #include #include +#include + #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(node)); } while (token != NULL); - } fclose(P); diff --git a/src/vector/bitvector.h b/src/vector/bitvector.h index 74fd0abf1..334b5ba78 100644 --- a/src/vector/bitvector.h +++ b/src/vector/bitvector.h @@ -13,24 +13,51 @@ #include "src/exceptions/invalid_argument.h" #include "src/exceptions/out_of_range.h" +#include + namespace mrmc { namespace vector { //! A Boolean Array /*! - A bit vector for boolean fields or quick selection schemas on Matrix entries. - Does NOT perform index bound checks! + A bit vector for boolean fields or quick selection schemas on Matrix entries. + 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() + /*! + \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](); @@ -43,14 +70,15 @@ class BitVector { //! Copy Constructor /*! - 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 + 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,47 +120,53 @@ 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]; } - + 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]; } - + 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]; } - + return result; } 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