Fixed seqfault when no property was given

src/storm-dft-cli/storm-dft.cpp

@@ -115,7 +115,8 @@ void processOptions() {
     }
 
     // Build properties
-    STORM_LOG_WARN_COND(!properties.empty(), "No property given.");
+    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()) {
@@ -123,7 +124,8 @@ void processOptions() {
             }
             propString += properties[i];
         }
-    std::vector<std::shared_ptr<storm::logic::Formula const>> props = storm::api::extractFormulasFromProperties(storm::api::parseProperties(propString));
+        props = storm::api::extractFormulasFromProperties(storm::api::parseProperties(propString));
+    }
 
     // Set relevant elements
     // TODO: also incorporate events from properties
@@ -149,7 +151,11 @@ void processOptions() {
         relevantEvents = dft->getAllIds();
     }
 
-    // Carry out the actual analysis
+    // 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();
@@ -157,6 +163,7 @@ void processOptions() {
         storm::api::analyzeDFT<ValueType>(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), relevantEvents, approximationError,
                                           faultTreeSettings.getApproximationHeuristic(), true);
     }
+}
 
 /*!
  * Entry point for Storm-DFT.

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