sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Refactored names according to guidelines.

tempestpy_adaptions
dehnert 12 years ago
parent
464fe97578
commit
8857655b56
2 changed files with 49 additions and 50 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 45
      src/models/Dtmc.h
  2. 54
      src/models/GraphTransitions.h

45
src/models/Dtmc.h
View File

@ -30,15 +30,15 @@ public:
/*! /*!
* Constructs a DTMC object from the given transition probability matrix and * Constructs a DTMC object from the given transition probability matrix and
* the given labeling of the states. * 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. * 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. * propositions to each state.
*/ */
Dtmc(mrmc::storage::SquareSparseMatrix<T>* 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<T>* probabilityMatrix, mrmc::models::AtomicPropositionsLabeling* stateLabeling)
: backwardTransitions(probabilityMatrix, false) {
this->probabilityMatrix = probabilityMatrix;
this->stateLabeling = stateLabeling;
} }
//! Copy Constructor //! Copy Constructor
@ -46,19 +46,19 @@ public:
* Copy Constructor. Performs a deep copy of the given DTMC. * Copy Constructor. Performs a deep copy of the given DTMC.
* @param dtmc A reference to the DTMC that is to be copied. * @param dtmc A reference to the DTMC that is to be copied.
*/ */
Dtmc(const Dtmc<T> &dtmc) : probability_matrix(dtmc.probability_matrix),
state_labeling(dtmc.state_labeling) { }
Dtmc(const Dtmc<T> &dtmc) : probabilityMatrix(dtmc.probabilityMatrix),
stateLabeling(dtmc.stateLabeling) { }
//! Destructor //! Destructor
/*! /*!
* Destructor. Frees the matrix and labeling associated with this DTMC. * Destructor. Frees the matrix and labeling associated with this DTMC.
*/ */
~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. * @return The size of the state space of the DTMC.
*/ */
uint_fast64_t getStateSpaceSize() { 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. * @return The number of (non-zero) transitions of the DTMC.
*/ */
uint_fast64_t getNumberOfTransitions() { uint_fast64_t getNumberOfTransitions() {
return this->probability_matrix->getNonZeroEntryCount();
return this->probabilityMatrix->getNonZeroEntryCount();
} }
/*! /*!
@ -85,7 +85,7 @@ public:
* function. * function.
*/ */
mrmc::storage::SquareSparseMatrix<T>* getTransitionProbabilityMatrix() { mrmc::storage::SquareSparseMatrix<T>* getTransitionProbabilityMatrix() {
return this->probability_matrix;
return this->probabilityMatrix;
} }
/*! /*!
@ -97,12 +97,11 @@ public:
<< std::endl; << std::endl;
out << "Model type: \t\tDTMC" << std::endl; out << "Model type: \t\tDTMC" << std::endl;
out << "States: \t\t" << this->getStateSpaceSize() << 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" 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; sizeof(*this))/1024 << " kbytes" << std::endl;
out << "-------------------------------------------------------------- " out << "-------------------------------------------------------------- "
<< std::endl; << std::endl;
@ -111,16 +110,16 @@ public:
private: private:
/*! A matrix representing the transition probability function of the DTMC. */ /*! A matrix representing the transition probability function of the DTMC. */
mrmc::storage::SquareSparseMatrix<T>* probability_matrix;
mrmc::storage::SquareSparseMatrix<T>* probabilityMatrix;
/*! The labeling of the states of the DTMC. */ /*! 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 * A data structure that stores the predecessors for all states. This is
* needed for backwards directed searches. * needed for backwards directed searches.
*/ */
mrmc::models::GraphTransitions<T> backward_transitions;
mrmc::models::GraphTransitions<T> backwardTransitions;
}; };
} // namespace models } // namespace models

54
src/models/GraphTransitions.h
View File

@ -27,7 +27,7 @@ public:
/*! /*!
* Just typedef the iterator as a pointer to the index type. * 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 //! Constructor
/*! /*!
@ -39,7 +39,7 @@ public:
* of the backwards transition relation. * of the backwards transition relation.
*/ */
GraphTransitions(mrmc::storage::SquareSparseMatrix<T>* transitionMatrix, bool forward) GraphTransitions(mrmc::storage::SquareSparseMatrix<T>* 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) { if (forward) {
this->initializeForward(transitionMatrix); this->initializeForward(transitionMatrix);
} else { } else {
@ -52,11 +52,11 @@ public:
* Destructor. Frees the internal storage. * Destructor. Frees the internal storage.
*/ */
~GraphTransitions() { ~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. * @param state The state for which to get the predecessor iterator.
* @return An iterator to the predecessors of the given states. * @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 * @return An iterator referring to the element after the predecessors of
* the given state. * 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: private:
@ -87,18 +87,18 @@ private:
* relation given by means of a sparse matrix. * relation given by means of a sparse matrix.
*/ */
void initializeForward(mrmc::storage::SquareSparseMatrix<T>* transitionMatrix) { 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];
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 // First, we copy the index list from the sparse matrix as this will
// stay the same. // 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 // Now we can iterate over all rows of the transition matrix and record
// the target state. // the target state.
for (uint_fast64_t i = 0, currentNonZeroElement = 0; i < numberOfStates; i++) { for (uint_fast64_t i = 0, currentNonZeroElement = 0; i < numberOfStates; i++) {
for (auto rowIt = transitionMatrix->beginConstColumnNoDiagIterator(i); rowIt != transitionMatrix->endConstColumnNoDiagIterator(i); ++rowIt) { 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. * matrix.
*/ */
void initializeBackward(mrmc::storage::SquareSparseMatrix<T>* transitionMatrix) { 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];
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. // First, we need to count how many backward transitions each state has.
// NOTE: We disregard the diagonal here, as we only consider "true" // NOTE: We disregard the diagonal here, as we only consider "true"
// predecessors. // predecessors.
for (uint_fast64_t i = 0; i < numberOfStates; i++) { for (uint_fast64_t i = 0; i < numberOfStates; i++) {
for (auto rowIt = transitionMatrix->beginConstColumnNoDiagIterator(i); rowIt != transitionMatrix->endConstColumnNoDiagIterator(i); ++rowIt) { 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. // Now compute the accumulated offsets.
for (uint_fast64_t i = 1; i < numberOfStates; i++) { 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, // 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 // for each state i the range of indices can be read off between
// state_indices_list[i] and state_indices_list[i + 1]. // 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 // Create an array that stores the next index for each state. Initially
// this corresponds to the previously computed accumulated offsets. // 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 // 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. // every state. Again, we start by considering all but the last row.
for (uint_fast64_t i = 0; i < numberOfStates; i++) { for (uint_fast64_t i = 0; i < numberOfStates; i++) {
for (auto rowIt = transitionMatrix->beginConstColumnNoDiagIterator(i); rowIt != transitionMatrix->endConstColumnNoDiagIterator(i); ++rowIt) { 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. // 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 * 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 * Store the number of states to determine the highest index at which the

Write Preview
Loading…
Cancel
Save