From 86c183a342efe4e76b8456af5927caa801e1830d Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Wed, 10 Apr 2019 16:46:36 +0200
Subject: [PATCH] Fixed seqfault when no property was given

---
 src/storm-dft-cli/storm-dft.cpp               | 33 +++++++++++--------
 .../modelchecker/dft/DFTModelChecker.cpp      |  1 +
 2 files changed, 21 insertions(+), 13 deletions(-)

diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp
index a804a798d..19dec5f9d 100644
--- a/src/storm-dft-cli/storm-dft.cpp
+++ b/src/storm-dft-cli/storm-dft.cpp
@@ -115,15 +115,17 @@ void processOptions() {
     }
 
     // Build properties
-    STORM_LOG_WARN_COND(!properties.empty(), "No property given.");
-    std::string propString;
-    for (size_t i = 0; i < properties.size(); ++i) {
-        if (i + 1 < properties.size()) {
-            propString += ";";
+    std::vector<std::shared_ptr<storm::logic::Formula const>> props;
+    if (!properties.empty()) {
+        std::string propString;
+        for (size_t i = 0; i < properties.size(); ++i) {
+            if (i + 1 < properties.size()) {
+                propString += ";";
+            }
+            propString += properties[i];
         }
-        propString += properties[i];
+        props = storm::api::extractFormulasFromProperties(storm::api::parseProperties(propString));
     }
-    std::vector<std::shared_ptr<storm::logic::Formula const>> props = storm::api::extractFormulasFromProperties(storm::api::parseProperties(propString));
 
     // Set relevant elements
     // TODO: also incorporate events from properties
@@ -149,13 +151,18 @@ void processOptions() {
         relevantEvents = dft->getAllIds();
     }
 
-    // Carry out the actual analysis
-    double approximationError = 0.0;
-    if (faultTreeSettings.isApproximationErrorSet()) {
-        approximationError = faultTreeSettings.getApproximationError();
+    // Analyze DFT
+    // TODO allow building of state space even without properties
+    if (props.empty()) {
+        STORM_LOG_WARN("No property given. No analysis will be performed.");
+    } else {
+        double approximationError = 0.0;
+        if (faultTreeSettings.isApproximationErrorSet()) {
+            approximationError = faultTreeSettings.getApproximationError();
+        }
+        storm::api::analyzeDFT<ValueType>(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), relevantEvents, approximationError,
+                                          faultTreeSettings.getApproximationHeuristic(), true);
     }
-    storm::api::analyzeDFT<ValueType>(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), relevantEvents, approximationError,
-                                      faultTreeSettings.getApproximationHeuristic(), true);
 }
 
 /*!
diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
index 5d6806f58..19a091a50 100644
--- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
+++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
@@ -27,6 +27,7 @@ namespace storm {
             // TODO: check that all paths reach the target state for approximation
 
             // Checking DFT
+            // TODO: distinguish for all properties, not only for first one
             if (properties[0]->isTimeOperatorFormula() && allowModularisation) {
                 // Use parallel composition as modularisation approach for expected time
                 std::shared_ptr<storm::models::sparse::Model<ValueType>> model = buildModelViaComposition(dft, properties, symred, true, relevantEvents);