Build all labels when exporting DFT

src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp

@@ -28,7 +28,7 @@ namespace storm {
         }
 
         template<typename ValueType, typename StateType>
-        ExplicitDFTModelBuilderApprox<ValueType, StateType>::LabelOptions::LabelOptions(std::vector<std::shared_ptr<const storm::logic::Formula>> properties) : buildFailLabel(true), buildFailSafeLabel(false) {
+        ExplicitDFTModelBuilderApprox<ValueType, StateType>::LabelOptions::LabelOptions(std::vector<std::shared_ptr<const storm::logic::Formula>> properties, bool buildAllLabels) : buildFailLabel(true), buildFailSafeLabel(false), buildAllLabels(buildAllLabels) {
             // Get necessary labels from properties
             std::vector<std::shared_ptr<storm::logic::AtomicLabelFormula const>> atomicLabels;
             for (auto property : properties) {
@@ -441,7 +441,7 @@ namespace storm {
             // 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) {
+                if (labelOpts.buildAllLabels || labelOpts.elementLabels.count(element->name()) > 0) {
                     modelComponents.stateLabeling.addLabel(element->name() + "_fail");
                 }
             }
@@ -462,7 +462,7 @@ namespace storm {
                 // 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()))) {
+                    if ((labelOpts.buildAllLabels || labelOpts.elementLabels.count(element->name()) > 0) && storm::storage::DFTState<ValueType>::hasFailed(state, stateGenerationInfo->getStateIndex(element->id()))) {
                         modelComponents.stateLabeling.addLabelToState(element->name() + "_fail", stateId);
                     }
                 }

src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h

@@ -154,7 +154,7 @@ namespace storm {
             // A structure holding the labeling options.
             struct LabelOptions {
                 // Constructor
-                LabelOptions(std::vector<std::shared_ptr<storm::logic::Formula const>> properties);
+                LabelOptions(std::vector<std::shared_ptr<storm::logic::Formula const>> properties, bool buildAllLabels = false);
 
                 // Flag indicating if the general fail label should be included.
                 bool buildFailLabel;
@@ -162,6 +162,9 @@ namespace storm {
                 // Flag indicating if the general failsafe label should be included.
                 bool buildFailSafeLabel;
 
+                // Flag indicating if all possible labels should be included.
+                bool buildAllLabels;
+
                 // Set of element names whose fail label to include.
                 std::set<std::string> elementLabels;
             };

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

@@ -344,7 +344,7 @@ 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(properties);
+                    typename storm::builder::ExplicitDFTModelBuilderApprox<ValueType>::LabelOptions labeloptions(properties, storm::settings::getModule<storm::settings::modules::IOSettings>().isExportExplicitSet());
                     builder.buildModel(labeloptions, 0, 0.0);
                     model = builder.getModel();
                 } else {