From 7e8b790451b01f0fd0c1dc27272eda8695bee65b Mon Sep 17 00:00:00 2001 From: Mavo Date: Fri, 11 Mar 2016 11:49:53 +0100 Subject: [PATCH] Preparation for pseudo state generation from bit vector Former-commit-id: a273f13a676bb7b1a9f5ae2b1ced896c40808e81 --- src/builder/ExplicitDFTModelBuilder.cpp | 39 ++++++++++++++++++++----- src/builder/ExplicitDFTModelBuilder.h | 2 +- src/storage/dft/DFTState.cpp | 7 +++++ src/storage/dft/DFTState.h | 5 ++++ 4 files changed, 45 insertions(+), 8 deletions(-) diff --git a/src/builder/ExplicitDFTModelBuilder.cpp b/src/builder/ExplicitDFTModelBuilder.cpp index 3c5a39702..d57dec2e7 100644 --- a/src/builder/ExplicitDFTModelBuilder.cpp +++ b/src/builder/ExplicitDFTModelBuilder.cpp @@ -246,10 +246,11 @@ namespace storm { if (!changed && newStateId >= OFFSET_PSEUDO_STATE) { newStateId = newStateId - OFFSET_PSEUDO_STATE; assert(newStateId < mPseudoStatesMapping.size()); - if (mPseudoStatesMapping[newStateId] == 0) { + if (mPseudoStatesMapping[newStateId].first == 0) { // Create pseudo state now + assert(mPseudoStatesMapping[newStateId].second == newState->status()); newState->setId(newIndex++); - mPseudoStatesMapping[newStateId] = newState->getId(); + mPseudoStatesMapping[newStateId].first = newState->getId(); newStateId = newState->getId(); mStates.setOrAdd(newState->status(), newStateId); stateQueue.push(newState); @@ -261,7 +262,7 @@ namespace storm { if (changed) { // Remember to create state later on newState->setId(mPseudoStatesMapping.size() + OFFSET_PSEUDO_STATE); - mPseudoStatesMapping.push_back(0); + mPseudoStatesMapping.push_back(std::make_pair(0, newState->status())); newStateId = mStates.findOrAdd(newState->status(), newState->getId()); STORM_LOG_TRACE("New state for later creation: " << mDft.getStateString(newState)); } else { @@ -345,9 +346,9 @@ namespace storm { if (it->first >= OFFSET_PSEUDO_STATE) { uint_fast64_t newId = it->first - OFFSET_PSEUDO_STATE; assert(newId < mPseudoStatesMapping.size()); - if (mPseudoStatesMapping[newId] > 0) { + if (mPseudoStatesMapping[newId].first > 0) { // State exists already - newId = mPseudoStatesMapping[newId]; + newId = mPseudoStatesMapping[newId].first; auto itFind = outgoingTransitions.find(newId); if (itFind != outgoingTransitions.end()) { // Add probability from pseudo state to instantiation @@ -382,11 +383,35 @@ namespace storm { exitRates.push_back(exitRate); assert(exitRates.size()-1 == state->getId()); + if (stateQueue.empty()) { + // Before ending the exploration check for pseudo states which are no be initialized yet + for (auto & pseudoStatePair : mPseudoStatesMapping) { + if (pseudoStatePair.first == 0) { + // Create state from pseudo state and explore + assert(mStates.contains(pseudoStatePair.second)); + assert(mStates.getValue(pseudoStatePair.second) >= OFFSET_PSEUDO_STATE); + STORM_LOG_TRACE("Create pseudo state from bit vector " << pseudoStatePair.second); + DFTStatePointer pseudoState = std::make_shared>(pseudoStatePair.second, mDft, *mStateGenerationInfo, newIndex++); + assert(pseudoStatePair.second == pseudoState->status()); + pseudoStatePair.first = pseudoState->getId(); + mStates.setOrAdd(pseudoState->status(), pseudoState->getId()); + stateQueue.push(pseudoState); + STORM_LOG_TRACE("Explore pseudo state " << mDft.getStateString(pseudoState) << " with id " << pseudoState->getId()); + break; + } + } + } + } // end while queue - assert(std::find(mPseudoStatesMapping.begin(), mPseudoStatesMapping.end(), 0) == mPseudoStatesMapping.end()); + + std::vector pseudoStatesVector; + for (auto const& pseudoStatePair : mPseudoStatesMapping) { + pseudoStatesVector.push_back(pseudoStatePair.first); + } + assert(std::find(pseudoStatesVector.begin(), pseudoStatesVector.end(), 0) == pseudoStatesVector.end()); // Replace pseudo states in matrix - transitionMatrixBuilder.replaceColumns(mPseudoStatesMapping, OFFSET_PSEUDO_STATE); + transitionMatrixBuilder.replaceColumns(pseudoStatesVector, OFFSET_PSEUDO_STATE); assert(!deterministic || rowOffset == 0); return deterministic; diff --git a/src/builder/ExplicitDFTModelBuilder.h b/src/builder/ExplicitDFTModelBuilder.h index 13b3eaf0d..7fc343be2 100644 --- a/src/builder/ExplicitDFTModelBuilder.h +++ b/src/builder/ExplicitDFTModelBuilder.h @@ -52,7 +52,7 @@ namespace storm { storm::storage::DFT const& mDft; std::shared_ptr mStateGenerationInfo; storm::storage::BitVectorHashMap mStates; - std::vector mPseudoStatesMapping; + std::vector> mPseudoStatesMapping; // vector of (id to concrete state, bitvector) size_t newIndex = 0; bool mergeFailedStates = true; size_t failedIndex = 0; diff --git a/src/storage/dft/DFTState.cpp b/src/storage/dft/DFTState.cpp index 1d34362f9..b7061b9b2 100644 --- a/src/storage/dft/DFTState.cpp +++ b/src/storage/dft/DFTState.cpp @@ -22,6 +22,13 @@ namespace storm { std::vector alwaysActiveBEs = dft.nonColdBEs(); mIsCurrentlyFailableBE.insert(mIsCurrentlyFailableBE.end(), alwaysActiveBEs.begin(), alwaysActiveBEs.end()); } + + template + DFTState::DFTState(storm::storage::BitVector const& status, DFT const& dft, DFTStateGenerationInfo const& stateGenerationInfo, size_t id) : mStatus(status), mId(id), mDft(dft), mStateGenerationInfo(stateGenerationInfo) { + // TODO implement + assert(false); + } + template DFTElementState DFTState::getElementState(size_t id) const { diff --git a/src/storage/dft/DFTState.h b/src/storage/dft/DFTState.h index 826e510d5..faf183411 100644 --- a/src/storage/dft/DFTState.h +++ b/src/storage/dft/DFTState.h @@ -36,6 +36,11 @@ namespace storm { public: DFTState(DFT const& dft, DFTStateGenerationInfo const& stateGenerationInfo, size_t id); + /** + * Construct state from underlying bitvector. + */ + DFTState(storm::storage::BitVector const& status, DFT const& dft, DFTStateGenerationInfo const& stateGenerationInfo, size_t id); + DFTElementState getElementState(size_t id) const; DFTDependencyState getDependencyState(size_t id) const;