Add labels for claiming in Markov chain with flag --labels-claiming

src/storm-dft/builder/ExplicitDFTModelBuilder.cpp

@@ -495,6 +495,8 @@ namespace storm {
 
         template<typename ValueType, typename StateType>
         void ExplicitDFTModelBuilder<ValueType, StateType>::buildLabeling() {
+            bool isAddLabelsClaiming = storm::settings::getModule<storm::settings::modules::FaultTreeSettings>().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<std::shared_ptr<storm::storage::DFTGate<ValueType> 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);

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();
             }

src/storm-dft/settings/modules/FaultTreeSettings.h

@@ -61,6 +61,13 @@ namespace storm {
                  */
                 std::vector<std::string> 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;

src/storm-dft/storage/dft/DFT.cpp

@@ -696,13 +696,7 @@ namespace storm {
                     stream << storm::storage::toChar(DFTState<ValueType>::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 ";
                         }

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<ValueType>::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<ValueType>::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;

src/storm-dft/storage/dft/DFTState.cpp

@@ -412,6 +412,11 @@ namespace storm {
             }
         }
 
+        template<typename ValueType>
+        uint_fast64_t DFTState<ValueType>::usesIndex(storm::storage::BitVector const& state, DFTStateGenerationInfo const& stateGenerationInfo, size_t id) {
+            return state.getAsInt(stateGenerationInfo.getSpareUsageIndex(id), stateGenerationInfo.usageInfoBits());
+        }
+
         template<typename ValueType>
         uint_fast64_t DFTState<ValueType>::extractUses(size_t from) const {
             STORM_LOG_ASSERT(mStateGenerationInfo.usageInfoBits() < 64, "UsageInfoBit size too large.");

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.