Browse Source

Adding check "transitionRewards submatrix of transitions"

main
gereon 13 years ago
parent
commit
b13f1ff37f
  1. 11
      src/models/Dtmc.h
  2. 21
      src/storage/SparseMatrix.h

11
src/models/Dtmc.h

@ -53,6 +53,12 @@ public:
LOG4CPLUS_ERROR(logger, "Probability matrix is invalid."); LOG4CPLUS_ERROR(logger, "Probability matrix is invalid.");
throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid."; throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid.";
} }
if (this->transitionRewardMatrix != nullptr) {
if (!this->transitionRewardMatrix->isSubmatrixOf(*(this->probabilityMatrix))) {
LOG4CPLUS_ERROR(logger, "Transition reward matrix is not a submatrix of the transition matrix, i.e. there are rewards for transitions that do not exist.");
throw storm::exceptions::InvalidArgumentException() << "There are transition rewards for nonexistent transitions.";
}
}
} }
//! Copy Constructor //! Copy Constructor
@ -66,10 +72,7 @@ public:
if (dtmc.backwardTransitions != nullptr) { if (dtmc.backwardTransitions != nullptr) {
this->backwardTransitions = new storm::models::GraphTransitions<T>(*dtmc.backwardTransitions); this->backwardTransitions = new storm::models::GraphTransitions<T>(*dtmc.backwardTransitions);
} }
if (!this->checkValidityOfProbabilityMatrix()) {
LOG4CPLUS_ERROR(logger, "Probability matrix is invalid.");
throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid.";
}
// no checks here, as they have already been performed for dtmc.
} }
//! Destructor //! Destructor

21
src/storage/SparseMatrix.h

@ -953,6 +953,27 @@ public:
} }
return sum; return sum;
} }
/*!
* @brief Checks if it is a submatrix of the given matrix.
*
* A matrix A is a submatrix of B if a value in A is only nonzero, if
* the value in B at the same position is also nonzero. Furthermore, A
* and B have to have the same size.
* @param matrix Matrix to check against.
* @return True iff this is a submatrix of matrix.
*/
bool isSubmatrixOf(SparseMatrix<T> const & matrix) const {
if (this->getRowCount() != matrix.getRowCount()) return false;
if (this->getColumnCount() != matrix.getColumnCount()) return false;
for (uint_fast64_t row = 0; row < this->getRowCount(); ++row) {
for (uint_fast64_t elem = rowIndications[row], elem2 = matrix.rowIndications[row]; elem < rowIndications[row + 1] && elem < matrix.rowIndications[row + 1]; ++elem, ++elem2) {
if (columnIndications[elem] < matrix.columnIndications[elem2]) return false;
}
}
return true;
}
void print() const { void print() const {
std::cout << "entries: ----------------------------" << std::endl; std::cout << "entries: ----------------------------" << std::endl;

Loading…
Cancel
Save