From ea00abc35eba8f83b5bc41e6d0ed07592fdf2528 Mon Sep 17 00:00:00 2001 From: Mavo Date: Thu, 13 Oct 2016 13:12:16 +0200 Subject: [PATCH] Fixed problems with approximation while using symred Former-commit-id: df12c037e731f08e7072e2d74abf64a5ce5c11f7 --- src/builder/ExplicitDFTModelBuilderApprox.cpp | 30 ++++++++++++------- src/storage/dft/DFTState.cpp | 2 +- src/utility/vector.cpp | 14 +++++---- 3 files changed, 29 insertions(+), 17 deletions(-) diff --git a/src/builder/ExplicitDFTModelBuilderApprox.cpp b/src/builder/ExplicitDFTModelBuilderApprox.cpp index 1f702d270..ac26129df 100644 --- a/src/builder/ExplicitDFTModelBuilderApprox.cpp +++ b/src/builder/ExplicitDFTModelBuilderApprox.cpp @@ -82,18 +82,23 @@ namespace storm { modelComponents.deterministicModel = generator.isDeterministicModel(); // Replace pseudo states in matrix - // TODO Matthias: avoid hack with fixed int type - std::vector pseudoStatesVector; - for (auto const& pseudoStatePair : mPseudoStatesMapping) { - pseudoStatesVector.push_back(pseudoStatePair.first); + if (!mPseudoStatesMapping.empty()) { + // TODO Matthias: avoid hack with fixed int type + std::vector pseudoStatesVector; + for (auto const& pseudoStatePair : mPseudoStatesMapping) { + pseudoStatesVector.push_back(matrixBuilder.mappingOffset + pseudoStatePair.first); + } + STORM_LOG_ASSERT(std::find(pseudoStatesVector.begin(), pseudoStatesVector.end(), 0) == pseudoStatesVector.end(), "Unexplored pseudo state still contained."); + STORM_LOG_TRACE("Replace pseudo states: " << pseudoStatesVector << ", offset: " << OFFSET_PSEUDO_STATE); + // TODO Matthias: combine replacement with later one + matrixBuilder.builder.replaceColumns(pseudoStatesVector, OFFSET_PSEUDO_STATE); + mPseudoStatesMapping.clear(); } - STORM_LOG_ASSERT(std::find(pseudoStatesVector.begin(), pseudoStatesVector.end(), 0) == pseudoStatesVector.end(), "Unexplored pseudo state still contained."); - matrixBuilder.builder.replaceColumns(pseudoStatesVector, OFFSET_PSEUDO_STATE); - mPseudoStatesMapping.clear(); // Fix the entries in the transition matrix according to the mapping of ids to row group indices STORM_LOG_ASSERT(matrixBuilder.stateRemapping[initialStateIndex] == initialStateIndex, "Initial state should not be remapped."); // TODO Matthias: do not consider all rows? + STORM_LOG_TRACE("Remap matrix: " << matrixBuilder.stateRemapping << ", offset: " << matrixBuilder.mappingOffset); matrixBuilder.remap(); STORM_LOG_TRACE("State remapping: " << matrixBuilder.stateRemapping); @@ -251,10 +256,9 @@ namespace storm { for (auto const& choice : behavior) { // Add the probabilistic behavior to the matrix. for (auto const& stateProbabilityPair : choice) { - - // Check that pseudo state and its instantiation do not appear together - // TODO Matthias: prove that this is not possible and remove if (stateProbabilityPair.first >= OFFSET_PSEUDO_STATE) { + // Check that pseudo state and its instantiation do not appear together + // TODO Matthias: prove that this is not possible and remove StateType newId = stateProbabilityPair.first - OFFSET_PSEUDO_STATE; STORM_LOG_ASSERT(newId < mPseudoStatesMapping.size(), "Id is not valid."); if (mPseudoStatesMapping[newId].first > 0) { @@ -264,8 +268,12 @@ namespace storm { STORM_LOG_ASSERT(itFind->first != newId, "Pseudo state and instantiation occur together in a distribution."); } } + // Set transtion to pseudo state + matrixBuilder.addTransition(stateProbabilityPair.first, stateProbabilityPair.second); + } else { + // Set transition to state id + offset. This helps in only remapping all previously skipped states. + matrixBuilder.addTransition(matrixBuilder.mappingOffset + stateProbabilityPair.first, stateProbabilityPair.second); } - matrixBuilder.addTransition(matrixBuilder.mappingOffset + stateProbabilityPair.first, stateProbabilityPair.second); } matrixBuilder.finishRow(); } diff --git a/src/storage/dft/DFTState.cpp b/src/storage/dft/DFTState.cpp index b292e322d..208dd6bf0 100644 --- a/src/storage/dft/DFTState.cpp +++ b/src/storage/dft/DFTState.cpp @@ -36,7 +36,7 @@ namespace storm { } 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) { + DFTState::DFTState(storm::storage::BitVector const& status, DFT const& dft, DFTStateGenerationInfo const& stateGenerationInfo, size_t id) : mStatus(status), mId(id), mDft(dft), mStateGenerationInfo(stateGenerationInfo), exploreHeuristic() { for(size_t index = 0; index < mDft.nrElements(); ++index) { // Initialize currently failable BE diff --git a/src/utility/vector.cpp b/src/utility/vector.cpp index 44e480029..595af193e 100644 --- a/src/utility/vector.cpp +++ b/src/utility/vector.cpp @@ -20,20 +20,24 @@ template std::ostream& operator<<(std::ostream& out, std::vector std::ostream& operator<<(std::ostream& out, std::vector const& vector) { out << "vector (" << vector.size() << ") [ "; - for (uint_fast64_t i = 0; i < vector.size() - 1; ++i) { + for (size_t i = 0; i + 1 < vector.size(); ++i) { out << vector[i] << ", "; } - out << vector.back(); + if (!vector.empty()) { + out << vector.back(); + } out << " ]"; return out; } std::ostream& operator<<(std::ostream& out, std::vector const& vector) { out << "vector (" << vector.size() << ") [ "; - for (uint_fast64_t i = 0; i < vector.size() - 1; ++i) { + for (size_t i = 0; i + 1 < vector.size(); ++i) { out << vector[i] << ", "; } - out << vector.back(); + if (!vector.empty()) { + out << vector.back(); + } out << " ]"; return out; -} \ No newline at end of file +}