Browse Source

Added assertions

Former-commit-id: c84ad69729
main
Mavo 9 years ago
parent
commit
4ece7e45a9
  1. 4
      src/builder/ExplicitDFTModelBuilder.cpp
  2. 5
      src/storage/dft/DFT.cpp

4
src/builder/ExplicitDFTModelBuilder.cpp

@ -1,6 +1,7 @@
#include "src/builder/ExplicitDFTModelBuilder.h" #include "src/builder/ExplicitDFTModelBuilder.h"
#include <src/models/sparse/Ctmc.h> #include <src/models/sparse/Ctmc.h>
#include <src/utility/constants.h> #include <src/utility/constants.h>
#include <src/exceptions/UnexpectedException.h>
#include <map> #include <map>
namespace storm { namespace storm {
@ -32,6 +33,7 @@ namespace storm {
// Build transition matrix // Build transition matrix
modelComponents.transitionMatrix = transitionMatrixBuilder.build(); modelComponents.transitionMatrix = transitionMatrixBuilder.build();
STORM_LOG_DEBUG("TransitionMatrix: " << std::endl << modelComponents.transitionMatrix); STORM_LOG_DEBUG("TransitionMatrix: " << std::endl << modelComponents.transitionMatrix);
assert(modelComponents.transitionMatrix.getRowCount() == modelComponents.transitionMatrix.getColumnCount());
// Build state labeling // Build state labeling
modelComponents.stateLabeling = storm::models::sparse::StateLabeling(mStates.size()); modelComponents.stateLabeling = storm::models::sparse::StateLabeling(mStates.size());
@ -90,6 +92,8 @@ namespace storm {
STORM_LOG_TRACE("Added self loop for " << state->getId()); STORM_LOG_TRACE("Added self loop for " << state->getId());
// No further exploration required // No further exploration required
continue; continue;
} else {
STORM_LOG_THROW(state->nrFailableBEs() > 0, storm::exceptions::UnexpectedException, "State " << state->getId() << " is no target state but behaves like one");
} }
// Let BE fail // Let BE fail

5
src/storage/dft/DFT.cpp

@ -133,10 +133,11 @@ namespace storm {
for (auto const& elem : mElements) { for (auto const& elem : mElements) {
stream << state->getElementStateInt(elem->id()); stream << state->getElementStateInt(elem->id());
if(elem->isSpareGate()) { if(elem->isSpareGate()) {
stream << "[";
if(state->isActiveSpare(elem->id())) { if(state->isActiveSpare(elem->id())) {
stream << " actively";
stream << "actively ";
} }
stream << " using " << state->uses(elem->id());
stream << "using " << state->uses(elem->id()) << "]";
} }
} }
return stream.str(); return stream.str();

Loading…
Cancel
Save