diff --git a/src/models/AtomicPropositionsLabeling.h b/src/models/AtomicPropositionsLabeling.h index 66b5c879f..2689ad6ea 100644 --- a/src/models/AtomicPropositionsLabeling.h +++ b/src/models/AtomicPropositionsLabeling.h @@ -15,6 +15,11 @@ #include #include +#include "log4cplus/logger.h" +#include "log4cplus/loggingmacros.h" + +extern log4cplus::Logger logger; + namespace storm { namespace models { @@ -82,9 +87,11 @@ public: */ uint_fast64_t addAtomicProposition(std::string ap) { if (nameToLabelingMap.count(ap) != 0) { + LOG4CPLUS_ERROR(logger, "Atomic Proposition already exists."); throw storm::exceptions::OutOfRangeException("Atomic Proposition already exists."); } if (apsCurrent >= apCountMax) { + LOG4CPLUS_ERROR(logger, "Added more atomic propositions than previously declared."); throw storm::exceptions::OutOfRangeException("Added more atomic propositions than" "previously declared."); } @@ -110,9 +117,11 @@ public: */ void addAtomicPropositionToState(std::string ap, const uint_fast64_t state) { if (nameToLabelingMap.count(ap) == 0) { + LOG4CPLUS_ERROR(logger, "Atomic Proposition '" << ap << "' unknown."); throw storm::exceptions::OutOfRangeException() << "Atomic Proposition '" << ap << "' unknown."; } if (state >= stateCount) { + LOG4CPLUS_ERROR(logger, "State index out of range."); throw storm::exceptions::OutOfRangeException("State index out of range."); } this->singleLabelings[nameToLabelingMap[ap]]->set(state, true); @@ -125,6 +134,7 @@ public: */ std::set getPropositionsForState(uint_fast64_t state) { if (state >= stateCount) { + LOG4CPLUS_ERROR(logger, "State index out of range."); throw storm::exceptions::OutOfRangeException("State index out of range."); } std::set result; @@ -165,6 +175,11 @@ public: * represents the labeling of the states with the given atomic proposition. */ storm::storage::BitVector* getAtomicProposition(std::string ap) { + if (!this->containsAtomicProposition(ap)) { + LOG4CPLUS_ERROR(logger, "The atomic proposition " << ap << " is invalid for the labeling of the model."); + throw storm::exceptions::InvalidArgumentException() << "The atomic proposition " << ap + << " is invalid for the labeling of the model."; + } return (this->singleLabelings[nameToLabelingMap[ap]]); } diff --git a/src/storm.cpp b/src/storm.cpp index a8e839595..77e58fd52 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -205,8 +205,21 @@ void testCheckingSynchronousLeader(storm::models::Dtmc& dtmc, uint_fast6 delete mc; } -void testCheckingDice(storm::models::Mdp mdp) { +void testCheckingDice(storm::models::Mdp& mdp) { + storm::storage::BitVector* targetStates = mdp.getLabeledStates(std::string("two")); + *targetStates |= *mdp.getLabeledStates(std::string("three")); + storm::storage::BitVector* trueStates = new storm::storage::BitVector(mdp.getNumberOfStates(), true); + storm::storage::BitVector* statesWithProbability0 = new storm::storage::BitVector(mdp.getNumberOfStates()); + storm::storage::BitVector* statesWithProbability1 = new storm::storage::BitVector(mdp.getNumberOfStates()); + + storm::utility::GraphAnalyzer::performProb01Max(mdp, *trueStates, *targetStates, statesWithProbability0, statesWithProbability1); + + std::cout << statesWithProbability0->toString() << std::endl << statesWithProbability1->toString() << std::endl; + + delete statesWithProbability0; + delete statesWithProbability1; + delete trueStates; } /*! diff --git a/src/utility/GraphAnalyzer.h b/src/utility/GraphAnalyzer.h index a05e3705d..9806077a2 100644 --- a/src/utility/GraphAnalyzer.h +++ b/src/utility/GraphAnalyzer.h @@ -257,7 +257,7 @@ public: bool addToStatesWithProbability0 = true; for (auto rowIt = nondeterministicChoiceIndices->begin() + *it; rowIt != nondeterministicChoiceIndices->begin() + *it + 1; ++rowIt) { bool hasAtLeastOneSuccessorWithProbabilityGreater0 = false; - for (auto colIt = transitionMatrix->beginConstColumnIterator(*rowIt); colIt != transitionMatrix->endConstColumnIterator(); ++colIt) { + for (auto colIt = transitionMatrix->beginConstColumnIterator(*rowIt); colIt != transitionMatrix->endConstColumnIterator(*rowIt); ++colIt) { if (statesWithProbability0->get(*colIt)) { hasAtLeastOneSuccessorWithProbabilityGreater0 = true; break;