From 5c0e515adeb8105742b5ba5db24c9dd1fc3fd321 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Thu, 2 Mar 2017 18:05:36 +0100
Subject: [PATCH] Build all labels when exporting DFT

---
 src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp | 6 +++---
 src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h   | 5 ++++-
 src/storm-dft/modelchecker/dft/DFTModelChecker.cpp      | 2 +-
 3 files changed, 8 insertions(+), 5 deletions(-)

diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp
index febccc0e6..65d9f838b 100644
--- a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp
+++ b/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);
                     }
                 }
diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h
index 6facce687..d7ee37de5 100644
--- a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h
+++ b/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;
             };
diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
index 8d655764e..73c107de6 100644
--- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
+++ b/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 {