diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp index 7b364204e..da2100537 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp +++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp @@ -58,11 +58,17 @@ namespace storm { dft(dft), stateGenerationInfo(std::make_shared(dft.buildStateGenerationInfo(symmetries))), relevantEvents(relevantEvents), - generator(dft, *stateGenerationInfo, relevantEvents, mergeFailedStates), + generator(dft, *stateGenerationInfo, mergeFailedStates), matrixBuilder(!generator.isDeterministicModel()), stateStorage(dft.stateBitVectorSize()), explorationQueue(1, 0, 0.9, false) { + // Set relevant events + this->dft.setRelevantEvents(this->relevantEvents); + // Mark top level element as relevant + this->dft.getElement(this->dft.getTopLevelIndex())->setRelevance(true); + + // Compute independent subtrees if (dft.topLevelType() == storm::storage::DFTElementType::OR) { // We only support this for approximation with top level element OR diff --git a/src/storm-dft/generator/DftNextStateGenerator.cpp b/src/storm-dft/generator/DftNextStateGenerator.cpp index 253e0e0a2..eb1795448 100644 --- a/src/storm-dft/generator/DftNextStateGenerator.cpp +++ b/src/storm-dft/generator/DftNextStateGenerator.cpp @@ -8,17 +8,17 @@ namespace storm { namespace generator { - + template - DftNextStateGenerator::DftNextStateGenerator(storm::storage::DFT const& dft, storm::storage::DFTStateGenerationInfo const& stateGenerationInfo, std::set const& relevantEvents, bool mergeFailedStates) : mDft(dft), mStateGenerationInfo(stateGenerationInfo), state(nullptr), relevantEvents(relevantEvents), mergeFailedStates(mergeFailedStates) { + DftNextStateGenerator::DftNextStateGenerator(storm::storage::DFT const& dft, storm::storage::DFTStateGenerationInfo const& stateGenerationInfo, bool mergeFailedStates) : mDft(dft), mStateGenerationInfo(stateGenerationInfo), state(nullptr), mergeFailedStates(mergeFailedStates) { deterministicModel = !mDft.canHaveNondeterminism(); } - + template bool DftNextStateGenerator::isDeterministicModel() const { return deterministicModel; } - + template std::vector DftNextStateGenerator::getInitialStates(StateToIdCallback const& stateToIdCallback) { DFTStatePointer initialState = std::make_shared>(mDft, mStateGenerationInfo, 0); @@ -42,7 +42,7 @@ namespace storm { // Store a pointer to the state itself, because we need to be able to access it when expanding it. this->state = state; } - + template StateBehavior DftNextStateGenerator::expand(StateToIdCallback const& stateToIdCallback) { STORM_LOG_DEBUG("Explore state: " << mDft.getStateString(state)); @@ -146,8 +146,8 @@ namespace storm { } // Propagate dont cares - // TODO: do not set DC for relevant events - while (relevantEvents.empty() && !queues.dontCarePropagationDone()) { + // Relevance is considered for each element independently + while (!queues.dontCarePropagationDone()) { DFTElementPointer next = queues.nextDontCarePropagation(); next->checkDontCareAnymore(*newState, queues); } diff --git a/src/storm-dft/generator/DftNextStateGenerator.h b/src/storm-dft/generator/DftNextStateGenerator.h index 0574d0266..b77751521 100644 --- a/src/storm-dft/generator/DftNextStateGenerator.h +++ b/src/storm-dft/generator/DftNextStateGenerator.h @@ -24,7 +24,7 @@ namespace storm { public: typedef std::function StateToIdCallback; - DftNextStateGenerator(storm::storage::DFT const& dft, storm::storage::DFTStateGenerationInfo const& stateGenerationInfo, std::set const& relevantEvents, bool mergeFailedStates); + DftNextStateGenerator(storm::storage::DFT const& dft, storm::storage::DFTStateGenerationInfo const& stateGenerationInfo, bool mergeFailedStates); bool isDeterministicModel() const; std::vector getInitialStates(StateToIdCallback const& stateToIdCallback); @@ -55,9 +55,6 @@ namespace storm { // Current state DFTStatePointer state; - // List with ids of relevant events which should be observed. - std::set const& relevantEvents; - // Flag indication if all failed states should be merged into one. bool mergeFailedStates = true; diff --git a/src/storm-dft/storage/dft/DFT.cpp b/src/storm-dft/storage/dft/DFT.cpp index 1aa04eaa6..4a3a5eb30 100644 --- a/src/storm-dft/storage/dft/DFT.cpp +++ b/src/storm-dft/storage/dft/DFT.cpp @@ -863,6 +863,17 @@ namespace storm { return (*iter)->id(); } + template + void DFT::setRelevantEvents(std::set const& relevantEvents) const { + for (auto const& elem : mElements) { + if (relevantEvents.find(elem->id()) != relevantEvents.end()) { + elem->setRelevance(true); + } else { + elem->setRelevance(false); + } + } + } + template void DFT::writeStatsToStream(std::ostream& stream) const { // Count individual types of elements diff --git a/src/storm-dft/storage/dft/DFT.h b/src/storm-dft/storage/dft/DFT.h index dfb7c583d..2b8795a82 100644 --- a/src/storm-dft/storage/dft/DFT.h +++ b/src/storm-dft/storage/dft/DFT.h @@ -318,6 +318,12 @@ namespace storm { */ size_t getIndex(std::string const& name) const; + /*! + * Set the relevance flag for all elements according to the given relevant events. + * @param relevantEvents All elements which should be to relevant. All elements not occuring are set to irrelevant. + */ + void setRelevantEvents(std::set const& relevantEvents) const; + private: std::tuple, std::vector, std::vector> getSortedParentAndDependencyIds(size_t index) const; diff --git a/src/storm-dft/storage/dft/elements/DFTElement.cpp b/src/storm-dft/storage/dft/elements/DFTElement.cpp index 5f04b9d65..d9bba261a 100644 --- a/src/storm-dft/storage/dft/elements/DFTElement.cpp +++ b/src/storm-dft/storage/dft/elements/DFTElement.cpp @@ -9,6 +9,11 @@ namespace storm { template bool DFTElement::checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const { + if (this->isRelevant()) { + // Relevant events are ignored for Don't Care propagation + return false; + } + if (state.dontCare(mId)) { return false; } diff --git a/src/storm-dft/storage/dft/elements/DFTElement.h b/src/storm-dft/storage/dft/elements/DFTElement.h index 80fff512c..f89f69c7a 100644 --- a/src/storm-dft/storage/dft/elements/DFTElement.h +++ b/src/storm-dft/storage/dft/elements/DFTElement.h @@ -51,7 +51,7 @@ namespace storm { * @param id Id. * @param name Name. */ - DFTElement(size_t id, std::string const& name) : mId(id), mName(name) { + DFTElement(size_t id, std::string const& name) : mId(id), mName(name), mRank(-1), mRelevant(false) { // Intentionally left empty. } @@ -117,6 +117,23 @@ namespace storm { this->mRank = rank; } + /*! + * Get whether the element is relevant. + * Relevant elements are for example not set to Don't Care and their status is stored as a label in the generated Markov Chain. + * @return True iff the element is relevant. + */ + virtual bool isRelevant() const { + return mRelevant; + } + + /*! + * Set the relevancy of the element. + * @param relevant If true, the element is relevant. + */ + virtual void setRelevance(bool relevant) const { + this->mRelevant = relevant; + } + /*! * Checks whether the element is a basic element. * @return True iff element is a BE. @@ -416,10 +433,11 @@ namespace storm { protected: std::size_t mId; std::string mName; - std::size_t mRank = -1; + std::size_t mRank; DFTGateVector mParents; DFTDependencyVector mOutgoingDependencies; DFTRestrictionVector mRestrictions; + mutable bool mRelevant; // Must be mutable to allow changes later on. TODO: avoid mutable };