diff --git a/src/models/AtomicPropositionsLabeling.h b/src/models/AtomicPropositionsLabeling.h index a88f285aa..30900f0c3 100644 --- a/src/models/AtomicPropositionsLabeling.h +++ b/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: diff --git a/src/models/Dtmc.h b/src/models/Dtmc.h index 01157489e..d993ab23d 100644 --- a/src/models/Dtmc.h +++ b/src/models/Dtmc.h @@ -11,7 +11,7 @@ #include #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* 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 backward_transitions; + mrmc::models::GraphTransitions backward_transitions; }; } // namespace models diff --git a/src/models/GraphTransitions.h b/src/models/GraphTransitions.h index 97ea77e35..c06701782 100644 --- a/src/models/GraphTransitions.h +++ b/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 #include "src/storage/SquareSparseMatrix.h" +#include + namespace mrmc { namespace models { @@ -20,7 +21,7 @@ namespace models { * given size. */ template -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* 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* 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* transitionMatrix) - : numberOfStates(transitionMatrix->getRowCount()), numberOfNonZeroTransitions(transitionMatrix->getNonZeroEntryCount()) { + void initializeBackward(mrmc::storage::SquareSparseMatrix* 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_ */ diff --git a/src/storage/BitVector.h b/src/storage/BitVector.h index ca1c7ec09..b8f21a916 100644 --- a/src/storage/BitVector.h +++ b/src/storage/BitVector.h @@ -16,6 +16,8 @@ extern log4cplus::Logger logger; +#include + 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: