Use fail labels according to given properties

src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp

@@ -9,7 +9,7 @@
 #include "storm/utility/bitoperations.h"
 #include "storm/exceptions/UnexpectedException.h"
 #include "storm/settings/SettingsManager.h"
-
+#include "storm/logic/AtomicLabelFormula.h"
 #include "storm-dft/settings/modules/DFTSettings.h"
 
 
@@ -27,6 +27,29 @@ namespace storm {
             builder = storm::storage::SparseMatrixBuilder<ValueType>(0, 0, 0, false, canHaveNondeterminism, 0);
         }
 
+        template<typename ValueType, typename StateType>
+        ExplicitDFTModelBuilderApprox<ValueType, StateType>::LabelOptions::LabelOptions(std::vector<std::shared_ptr<const storm::logic::Formula>> properties) : buildFailLabel(true), buildFailSafeLabel(false) {
+            // Get necessary labels from properties
+            std::vector<std::shared_ptr<storm::logic::AtomicLabelFormula const>> atomicLabels;
+            for (auto property : properties) {
+                property->gatherAtomicLabelFormulas(atomicLabels);
+            }
+            // Set usage of necessary labels
+            for (auto atomic : atomicLabels) {
+                std::string label = atomic->getLabel();
+                std::size_t foundIndex = label.find("_fail");
+                if (foundIndex != std::string::npos) {
+                    elementLabels.insert(label.substr(0, foundIndex));
+                } else if (label.compare("failed") == 0) {
+                    buildFailLabel = true;
+                } else if (label.compare("failsafe") == 0) {
+                    buildFailSafeLabel = true;
+                } else {
+                    STORM_LOG_WARN("Label '" << label << "' not known.");
+                }
+            }
+        }
+
         template<typename ValueType, typename StateType>
         ExplicitDFTModelBuilderApprox<ValueType, StateType>::ExplicitDFTModelBuilderApprox(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC) :
                 dft(dft),
@@ -415,16 +438,16 @@ namespace storm {
                 modelComponents.stateLabeling.addLabel("failsafe");
             }
 
-            // Collect labels for all BE
-            std::vector<std::shared_ptr<storage::DFTBE<ValueType>>> basicElements = dft.getBasicElements();
-            for (std::shared_ptr<storage::DFTBE<ValueType>> elem : basicElements) {
-                if(labelOpts.beLabels.count(elem->name()) > 0) {
-                    modelComponents.stateLabeling.addLabel(elem->name() + "_fail");
+            // Collect labels for all necessary elements
+            for (size_t id = 0; id < dft.nrElements(); ++id) {
+                std::shared_ptr<storage::DFTElement<ValueType> const> element = dft.getElement(id);
+                if (labelOpts.elementLabels.count(element->name()) > 0) {
+                    modelComponents.stateLabeling.addLabel(element->name() + "_fail");
                 }
             }
 
             // Set labels to states
-            if(mergeFailedStates) {
+            if (mergeFailedStates) {
                 modelComponents.stateLabeling.addLabelToState("failed", failedStateId);
             }
             for (auto const& stateIdPair : stateStorage.stateToId) {
@@ -435,14 +458,17 @@ namespace storm {
                 }
                 if (labelOpts.buildFailSafeLabel && dft.isFailsafe(state, *stateGenerationInfo)) {
                     modelComponents.stateLabeling.addLabelToState("failsafe", stateId);
-                };
-                // Set fail status for each BE
-                for (std::shared_ptr<storage::DFTBE<ValueType>> elem : basicElements) {
-                    if (labelOpts.beLabels.count(elem->name()) > 0 && storm::storage::DFTState<ValueType>::hasFailed(state, stateGenerationInfo->getStateIndex(elem->id())) ) {
-                        modelComponents.stateLabeling.addLabelToState(elem->name() + "_fail", stateId);
+                }
+                // Set fail status for each necessary element
+                for (size_t id = 0; id < dft.nrElements(); ++id) {
+                    std::shared_ptr<storage::DFTElement<ValueType> const> element = dft.getElement(id);
+                    if (labelOpts.elementLabels.count(element->name()) > 0 && storm::storage::DFTState<ValueType>::hasFailed(state, stateGenerationInfo->getStateIndex(element->id()))) {
+                        modelComponents.stateLabeling.addLabelToState(element->name() + "_fail", stateId);
                     }
                 }
             }
+
+            STORM_LOG_TRACE(modelComponents.stateLabeling);
         }
 
         template<typename ValueType, typename StateType>

src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h

@@ -153,9 +153,17 @@ namespace storm {
         public:
             // A structure holding the labeling options.
             struct LabelOptions {
-                bool buildFailLabel = true;
-                bool buildFailSafeLabel = false;
-                std::set<std::string> beLabels = {};
+                // Constructor
+                LabelOptions(std::vector<std::shared_ptr<storm::logic::Formula const>> properties);
+
+                // Flag indicating if the general fail label should be included.
+                bool buildFailLabel;
+
+                // Flag indicating if the general failsafe label should be included.
+                bool buildFailSafeLabel;
+
+                // Set of element names whose fail label to include.
+                std::set<std::string> elementLabels;
             };
 
             /*!

src/storm-dft/modelchecker/dft/DFTModelChecker.cpp

@@ -191,7 +191,7 @@ namespace storm {
                     // Build a single CTMC
                     STORM_LOG_INFO("Building Model...");
                     storm::builder::ExplicitDFTModelBuilderApprox<ValueType> builder(ft, symmetries, enableDC);
-                    typename storm::builder::ExplicitDFTModelBuilderApprox<ValueType>::LabelOptions labeloptions; // TODO initialize this with the formula
+                    typename storm::builder::ExplicitDFTModelBuilderApprox<ValueType>::LabelOptions labeloptions(properties);
                     builder.buildModel(labeloptions, 0, 0.0);
                     std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.getModel();
                     //model->printModelInformationToStream(std::cout);
@@ -246,7 +246,7 @@ namespace storm {
 
 
                 storm::builder::ExplicitDFTModelBuilderApprox<ValueType> builder(dft, symmetries, enableDC);
-                typename storm::builder::ExplicitDFTModelBuilderApprox<ValueType>::LabelOptions labeloptions; // TODO initialize this with the formula
+                typename storm::builder::ExplicitDFTModelBuilderApprox<ValueType>::LabelOptions labeloptions(properties);
                 builder.buildModel(labeloptions, 0, 0.0);
                 std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.getModel();
                 //model->printModelInformationToStream(std::cout);
@@ -280,7 +280,7 @@ namespace storm {
                 std::shared_ptr<storm::models::sparse::Model<ValueType>> model;
                 std::vector<ValueType> newResult;
                 storm::builder::ExplicitDFTModelBuilderApprox<ValueType> builder(dft, symmetries, enableDC);
-                typename storm::builder::ExplicitDFTModelBuilderApprox<ValueType>::LabelOptions labeloptions; // TODO initialize this with the formula
+                typename storm::builder::ExplicitDFTModelBuilderApprox<ValueType>::LabelOptions labeloptions(properties);
 
                 // TODO Matthias: compute approximation for all properties simultaneously?
                 std::shared_ptr<const storm::logic::Formula> property = properties[0];
@@ -348,12 +348,12 @@ namespace storm {
                 // TODO Matthias: use only one builder if everything works again
                 if (storm::settings::getModule<storm::settings::modules::DFTSettings>().isApproximationErrorSet()) {
                     storm::builder::ExplicitDFTModelBuilderApprox<ValueType> builder(dft, symmetries, enableDC);
-                    typename storm::builder::ExplicitDFTModelBuilderApprox<ValueType>::LabelOptions labeloptions; // TODO initialize this with the formula
+                    typename storm::builder::ExplicitDFTModelBuilderApprox<ValueType>::LabelOptions labeloptions(properties);
                     builder.buildModel(labeloptions, 0, 0.0);
                     model = builder.getModel();
                 } else {
                     storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries, enableDC);
-                    typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions; // TODO initialize this with the formula
+                    typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions;
                     model = builder.buildModel(labeloptions);
                 }
                 //model->printModelInformationToStream(std::cout);

src/storm-dft/modelchecker/dft/DFTModelChecker.h

@@ -19,7 +19,7 @@ namespace storm {
 
             typedef std::pair<ValueType, ValueType> approximation_result;
             typedef std::vector<boost::variant<ValueType, approximation_result>> dft_results;
-            typedef std::vector<std::shared_ptr<const storm::logic::Formula>> property_vector;
+            typedef std::vector<std::shared_ptr<storm::logic::Formula const>> property_vector;
 
         public:
 

src/storm/models/sparse/StateLabeling.cpp

@@ -115,6 +115,23 @@ namespace storm {
                     out << "   * " << labelIndexPair.first << " -> " << this->labelings[labelIndexPair.second].getNumberOfSetBits() << " state(s)" << std::endl;
                 }
             }
+
+            void StateLabeling::printCompleteLabelingInformationToStream(std::ostream& out) const {
+                out << "Labels: \t" << this->getNumberOfLabels() << std::endl;
+                for (auto label : nameToLabelingIndexMap) {
+                    out << "Label '" << label.first << "': ";
+                    for (auto index : this->labelings[label.second]) {
+                        out << index << " ";
+                    }
+                    out << std::endl;
+                }
+            }
+
+            std::ostream& operator<<(std::ostream& out, StateLabeling const& labeling) {
+                labeling.printLabelingInformationToStream(out);
+                return out;
+            }
+
         }
     }
 }

src/storm/models/sparse/StateLabeling.h

@@ -152,7 +152,16 @@ namespace storm {
                  * @param out The stream the information is to be printed to.
                  */
                 void printLabelingInformationToStream(std::ostream& out) const;
-                
+
+                /*!
+                 * Prints the complete labeling to the specified stream.
+                 *
+                 * @param out The stream the information is to be printed to.
+                 */
+                void printCompleteLabelingInformationToStream(std::ostream& out) const;
+
+                friend std::ostream& operator<<(std::ostream& out, StateLabeling const& labeling);
+
             private:
                 // The number of states for which this object can hold the labeling.
                 uint_fast64_t stateCount;