From 936985f5360ea31865600c5c1dd0802406804252 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 12 May 2020 17:37:17 +0200 Subject: [PATCH] Add labels for claiming in Markov chain with flag --labels-claiming --- .../builder/ExplicitDFTModelBuilder.cpp | 21 +++++++++++++++++++ .../settings/modules/FaultTreeSettings.cpp | 7 +++++++ .../settings/modules/FaultTreeSettings.h | 8 +++++++ src/storm-dft/storage/dft/DFT.cpp | 8 +------ src/storm-dft/storage/dft/DFT.h | 20 +++++++++++++++++- src/storm-dft/storage/dft/DFTState.cpp | 5 +++++ src/storm-dft/storage/dft/DFTState.h | 11 ++++++++++ 7 files changed, 72 insertions(+), 8 deletions(-) diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp index 7b601032e..d1c46cbed 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp +++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp @@ -495,6 +495,8 @@ namespace storm { template void ExplicitDFTModelBuilder::buildLabeling() { + bool isAddLabelsClaiming = storm::settings::getModule().isAddLabelsClaiming(); + // Build state labeling modelComponents.stateLabeling = storm::models::sparse::StateLabeling(modelComponents.transitionMatrix.getRowGroupCount()); // Initial state @@ -513,6 +515,17 @@ namespace storm { modelComponents.stateLabeling.addLabel(element->name() + "_dc"); } } + std::vector const>> spares; // Only filled if needed + if (isAddLabelsClaiming) { + // Collect labels for claiming + for (size_t spareId : dft.getSpareIndices()) { + auto const& spare = dft.getGate(spareId); + spares.push_back(spare); + for (auto const& child : spare->children()) { + modelComponents.stateLabeling.addLabel(spare->name() + "_claimed_" + child->name()); + } + } + } // Set labels to states if (this->uniqueFailedState) { @@ -546,6 +559,14 @@ namespace storm { } } } + if (isAddLabelsClaiming) { + for (auto const& spare : spares) { + size_t claimedChildId = dft.uses(state, *stateGenerationInfo, spare->id()); + if (claimedChildId != spare->id()) { + modelComponents.stateLabeling.addLabelToState(spare->name() + "_claimed_" + dft.getElement(claimedChildId)->name(), stateId); + } + } + } } STORM_LOG_TRACE(modelComponents.stateLabeling); diff --git a/src/storm-dft/settings/modules/FaultTreeSettings.cpp b/src/storm-dft/settings/modules/FaultTreeSettings.cpp index 5a6cc7243..a10ebc854 100644 --- a/src/storm-dft/settings/modules/FaultTreeSettings.cpp +++ b/src/storm-dft/settings/modules/FaultTreeSettings.cpp @@ -21,6 +21,7 @@ namespace storm { const std::string FaultTreeSettings::disableDCOptionName = "disabledc"; const std::string FaultTreeSettings::allowDCRelevantOptionName = "allowdcrelevant"; const std::string FaultTreeSettings::relevantEventsOptionName = "relevantevents"; + const std::string FaultTreeSettings::addLabelsClaimingOptionName = "labels-claiming"; const std::string FaultTreeSettings::approximationErrorOptionName = "approximation"; const std::string FaultTreeSettings::approximationErrorOptionShortName = "approx"; const std::string FaultTreeSettings::approximationHeuristicOptionName = "approximationheuristic"; @@ -43,6 +44,8 @@ namespace storm { "A comma separated list of names of relevant events. 'all' marks all events as relevant, The default '' or 'none' marks only the top level event as relevant.").setDefaultValueString( "").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, allowDCRelevantOptionName, false, "Allow Don't Care propagation for relevant events.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, addLabelsClaimingOptionName, false, + "Add labels representing claiming operations.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, approximationErrorOptionName, false, "Approximation error allowed.").setShortName( approximationErrorOptionShortName).addArgument( storm::settings::ArgumentBuilder::createDoubleArgument("error", "The relative approximation error to use.").addValidatorDouble( @@ -86,6 +89,10 @@ namespace storm { return storm::parser::parseCommaSeperatedValues(this->getOption(relevantEventsOptionName).getArgumentByName("values").getValueAsString()); } + bool FaultTreeSettings::isAddLabelsClaiming() const { + return this->getOption(addLabelsClaimingOptionName).getHasOptionBeenSet(); + } + bool FaultTreeSettings::isApproximationErrorSet() const { return this->getOption(approximationErrorOptionName).getHasOptionBeenSet(); } diff --git a/src/storm-dft/settings/modules/FaultTreeSettings.h b/src/storm-dft/settings/modules/FaultTreeSettings.h index 3099f4b8b..91fd452c8 100644 --- a/src/storm-dft/settings/modules/FaultTreeSettings.h +++ b/src/storm-dft/settings/modules/FaultTreeSettings.h @@ -61,6 +61,13 @@ namespace storm { */ std::vector getRelevantEvents() const; + /*! + * Retrieves whether the labels for claimings should be added in the Markov chain. + * + * @return True iff the option was set. + */ + bool isAddLabelsClaiming() const; + /*! * Retrieves whether the option to compute an approximation is set. * @@ -136,6 +143,7 @@ namespace storm { static const std::string disableDCOptionName; static const std::string allowDCRelevantOptionName; static const std::string relevantEventsOptionName; + static const std::string addLabelsClaimingOptionName; static const std::string approximationErrorOptionName; static const std::string approximationErrorOptionShortName; static const std::string approximationHeuristicOptionName; diff --git a/src/storm-dft/storage/dft/DFT.cpp b/src/storm-dft/storage/dft/DFT.cpp index 94e33cbaa..0e00c4423 100644 --- a/src/storm-dft/storage/dft/DFT.cpp +++ b/src/storm-dft/storage/dft/DFT.cpp @@ -696,13 +696,7 @@ namespace storm { stream << storm::storage::toChar(DFTState::getElementState(status, stateGenerationInfo, elem->id())); if (elem->isSpareGate()) { stream << "["; - size_t nrUsedChild = status.getAsInt(stateGenerationInfo.getSpareUsageIndex(elem->id()), stateGenerationInfo.usageInfoBits()); - size_t useId; - if (nrUsedChild == getMaxSpareChildCount()) { - useId = elem->id(); - } else { - useId = getChild(elem->id(), nrUsedChild); - } + size_t useId = this->uses(status, stateGenerationInfo, elem->id()); if (useId == elem->id() || status[stateGenerationInfo.getSpareActivationIndex(useId)]) { stream << "actively "; } diff --git a/src/storm-dft/storage/dft/DFT.h b/src/storm-dft/storage/dft/DFT.h index a95b06937..9f5ecdea4 100644 --- a/src/storm-dft/storage/dft/DFT.h +++ b/src/storm-dft/storage/dft/DFT.h @@ -287,7 +287,25 @@ namespace storm { bool isFailsafe(storm::storage::BitVector const& state, DFTStateGenerationInfo const& stateGenerationInfo) const { return storm::storage::DFTState::isFailsafe(state, stateGenerationInfo.getStateIndex(mTopLevelIndex)); } - + + /*! + * Return id of used child for a given spare gate. + * If no child is used the id of the spare gate is returned. + * + * @param state DFT state. + * @param stateGenerationInfo State generation information. + * @param id Id of spare gate. + * @return Id of used child. Id of spare gate if no child is used. + */ + size_t uses(storm::storage::BitVector const& state, DFTStateGenerationInfo const& stateGenerationInfo, size_t id) const { + size_t nrUsedChild = storm::storage::DFTState::usesIndex(state, stateGenerationInfo, id); + if (nrUsedChild == getMaxSpareChildCount()) { + return id; + } else { + return getChild(id, nrUsedChild); + } + } + size_t getChild(size_t spareId, size_t nrUsedChild) const; size_t getNrChild(size_t spareId, size_t childId) const; diff --git a/src/storm-dft/storage/dft/DFTState.cpp b/src/storm-dft/storage/dft/DFTState.cpp index 65e0b3fb8..4be919435 100644 --- a/src/storm-dft/storage/dft/DFTState.cpp +++ b/src/storm-dft/storage/dft/DFTState.cpp @@ -412,6 +412,11 @@ namespace storm { } } + template + uint_fast64_t DFTState::usesIndex(storm::storage::BitVector const& state, DFTStateGenerationInfo const& stateGenerationInfo, size_t id) { + return state.getAsInt(stateGenerationInfo.getSpareUsageIndex(id), stateGenerationInfo.usageInfoBits()); + } + template uint_fast64_t DFTState::extractUses(size_t from) const { STORM_LOG_ASSERT(mStateGenerationInfo.usageInfoBits() < 64, "UsageInfoBit size too large."); diff --git a/src/storm-dft/storage/dft/DFTState.h b/src/storm-dft/storage/dft/DFTState.h index 9eb425d7e..9ebe12dba 100644 --- a/src/storm-dft/storage/dft/DFTState.h +++ b/src/storm-dft/storage/dft/DFTState.h @@ -259,6 +259,17 @@ namespace storm { * the spare. */ uint_fast64_t uses(size_t id) const; + + /** + * Returns the index of the used child for a spare gate. + * If no element is used, the maximal spare count is returned. + * + * @param state DFT state. + * @param stateGenerationInfo State generation info. + * @param id Id of spare gate. + * @return Index of used child. Maximal spare count if no child is usde. + */ + static uint_fast64_t usesIndex(storm::storage::BitVector const& state, DFTStateGenerationInfo const& stateGenerationInfo, size_t id); /** * This method is commonly used to get the usage information for spares.