diff --git a/src/models/Dtmc.h b/src/models/Dtmc.h index d993ab23d..4376c9559 100644 --- a/src/models/Dtmc.h +++ b/src/models/Dtmc.h @@ -30,15 +30,15 @@ public: /*! * Constructs a DTMC object from the given transition probability matrix and * the given labeling of the states. - * @param probability_matrix The transition probability function of the + * @param probabilityMatrix The transition probability function of the * DTMC given by a matrix. - * @param state_labeling The labeling that assigns a set of atomic + * @param stateLabeling The labeling that assigns a set of atomic * propositions to each state. */ - Dtmc(mrmc::storage::SquareSparseMatrix* probability_matrix, mrmc::models::AtomicPropositionsLabeling* state_labeling) - : backward_transitions(probability_matrix, false) { - this->probability_matrix = probability_matrix; - this->state_labeling = state_labeling; + Dtmc(mrmc::storage::SquareSparseMatrix* probabilityMatrix, mrmc::models::AtomicPropositionsLabeling* stateLabeling) + : backwardTransitions(probabilityMatrix, false) { + this->probabilityMatrix = probabilityMatrix; + this->stateLabeling = stateLabeling; } //! Copy Constructor @@ -46,19 +46,19 @@ public: * Copy Constructor. Performs a deep copy of the given DTMC. * @param dtmc A reference to the DTMC that is to be copied. */ - Dtmc(const Dtmc &dtmc) : probability_matrix(dtmc.probability_matrix), - state_labeling(dtmc.state_labeling) { } + Dtmc(const Dtmc &dtmc) : probabilityMatrix(dtmc.probabilityMatrix), + stateLabeling(dtmc.stateLabeling) { } //! Destructor /*! * Destructor. Frees the matrix and labeling associated with this DTMC. */ ~Dtmc() { - if (this->probability_matrix != nullptr) { - delete this->probability_matrix; + if (this->probabilityMatrix != nullptr) { + delete this->probabilityMatrix; } - if (this->state_labeling != nullptr) { - delete this->state_labeling; + if (this->stateLabeling != nullptr) { + delete this->stateLabeling; } } @@ -67,7 +67,7 @@ public: * @return The size of the state space of the DTMC. */ uint_fast64_t getStateSpaceSize() { - return this->probability_matrix->getRowCount(); + return this->probabilityMatrix->getRowCount(); } /*! @@ -75,7 +75,7 @@ public: * @return The number of (non-zero) transitions of the DTMC. */ uint_fast64_t getNumberOfTransitions() { - return this->probability_matrix->getNonZeroEntryCount(); + return this->probabilityMatrix->getNonZeroEntryCount(); } /*! @@ -85,7 +85,7 @@ public: * function. */ mrmc::storage::SquareSparseMatrix* getTransitionProbabilityMatrix() { - return this->probability_matrix; + return this->probabilityMatrix; } /*! @@ -97,12 +97,11 @@ public: << std::endl; out << "Model type: \t\tDTMC" << std::endl; out << "States: \t\t" << this->getStateSpaceSize() << std::endl; - out << "Transitions: \t\t" << this->getNumberOfTransitions() - << std::endl; - this->state_labeling->printAtomicPropositionsInformationToStream(out); + out << "Transitions: \t\t" << this->getNumberOfTransitions() << std::endl; + this->stateLabeling->printAtomicPropositionsInformationToStream(out); out << "Size in memory: \t" - << (this->probability_matrix->getSizeInMemory() + - this->state_labeling->getSizeInMemory() + + << (this->probabilityMatrix->getSizeInMemory() + + this->stateLabeling->getSizeInMemory() + sizeof(*this))/1024 << " kbytes" << std::endl; out << "-------------------------------------------------------------- " << std::endl; @@ -111,16 +110,16 @@ public: private: /*! A matrix representing the transition probability function of the DTMC. */ - mrmc::storage::SquareSparseMatrix* probability_matrix; + mrmc::storage::SquareSparseMatrix* probabilityMatrix; /*! The labeling of the states of the DTMC. */ - mrmc::models::AtomicPropositionsLabeling* state_labeling; + mrmc::models::AtomicPropositionsLabeling* stateLabeling; /*! * A data structure that stores the predecessors for all states. This is * needed for backwards directed searches. */ - mrmc::models::GraphTransitions backward_transitions; + mrmc::models::GraphTransitions backwardTransitions; }; } // namespace models diff --git a/src/models/GraphTransitions.h b/src/models/GraphTransitions.h index 50b950359..88ef44f7f 100644 --- a/src/models/GraphTransitions.h +++ b/src/models/GraphTransitions.h @@ -27,7 +27,7 @@ public: /*! * Just typedef the iterator as a pointer to the index type. */ - typedef const uint_fast64_t * const state_predecessor_iterator; + typedef const uint_fast64_t * const statePredecessorIterator; //! Constructor /*! @@ -39,7 +39,7 @@ public: * of the backwards transition relation. */ GraphTransitions(mrmc::storage::SquareSparseMatrix* transitionMatrix, bool forward) - : predecessor_list(nullptr), state_indices_list(nullptr), numberOfStates(transitionMatrix->getRowCount()), numberOfNonZeroTransitions(transitionMatrix->getNonZeroEntryCount()) { + : successorList(nullptr), stateIndications(nullptr), numberOfStates(transitionMatrix->getRowCount()), numberOfNonZeroTransitions(transitionMatrix->getNonZeroEntryCount()) { if (forward) { this->initializeForward(transitionMatrix); } else { @@ -52,11 +52,11 @@ public: * Destructor. Frees the internal storage. */ ~GraphTransitions() { - if (this->predecessor_list != nullptr) { - delete[] this->predecessor_list; + if (this->successorList != nullptr) { + delete[] this->successorList; } - if (this->state_indices_list != nullptr) { - delete[] this->state_indices_list; + if (this->stateIndications != nullptr) { + delete[] this->stateIndications; } } @@ -65,8 +65,8 @@ public: * @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]; + statePredecessorIterator beginStatePredecessorIterator(uint_fast64_t state) const { + return this->successorList + this->stateIndications[state]; } /*! @@ -76,8 +76,8 @@ public: * @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]; + statePredecessorIterator endStatePredecessorIterator(uint_fast64_t state) const { + return this->successorList + this->stateIndications[state + 1]; } private: @@ -87,18 +87,18 @@ private: * 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]; + this->successorList = new uint_fast64_t[numberOfNonZeroTransitions]; + this->stateIndications = 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); + memcpy(this->stateIndications, 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; + this->stateIndications[currentNonZeroElement++] = *rowIt; } } } @@ -109,53 +109,53 @@ private: * matrix. */ void initializeBackward(mrmc::storage::SquareSparseMatrix* transitionMatrix) { - this->predecessor_list = new uint_fast64_t[numberOfNonZeroTransitions]; - this->state_indices_list = new uint_fast64_t[numberOfStates + 1]; + this->successorList = new uint_fast64_t[numberOfNonZeroTransitions]; + 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 (auto rowIt = transitionMatrix->beginConstColumnNoDiagIterator(i); rowIt != transitionMatrix->endConstColumnNoDiagIterator(i); ++rowIt) { - this->state_indices_list[*rowIt + 1]++; + this->stateIndications[*rowIt + 1]++; } } // Now compute the accumulated offsets. for (uint_fast64_t i = 1; i < numberOfStates; i++) { - this->state_indices_list[i] = this->state_indices_list[i - 1] + this->state_indices_list[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->state_indices_list[numberOfStates] = numberOfNonZeroTransitions; + this->stateIndications[numberOfStates] = numberOfNonZeroTransitions; // Create an array that stores the next index for each state. Initially // this corresponds to the previously computed accumulated offsets. - uint_fast64_t* next_state_index_list = new uint_fast64_t[numberOfStates]; - memcpy(next_state_index_list, state_indices_list, numberOfStates * sizeof(uint_fast64_t)); + uint_fast64_t* nextIndicesList = new uint_fast64_t[numberOfStates]; + memcpy(nextIndicesList, stateIndications, numberOfStates * sizeof(uint_fast64_t)); // 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->beginConstColumnNoDiagIterator(i); rowIt != transitionMatrix->endConstColumnNoDiagIterator(i); ++rowIt) { - this->predecessor_list[next_state_index_list[*rowIt]++] = i; + this->successorList[nextIndicesList[*rowIt]++] = i; } } // Now we can dispose of the auxiliary array. - delete[] next_state_index_list; + delete[] nextIndicesList; } - /*! A list of predecessors for *all* states. */ - uint_fast64_t* predecessor_list; + /*! A list of successors for *all* states. */ + uint_fast64_t* successorList; /*! * A list of indices indicating at which position in the global array the - * predecessors of a state can be found. + * successors of a state can be found. */ - uint_fast64_t* state_indices_list; + uint_fast64_t* stateIndications; /*! * Store the number of states to determine the highest index at which the