From 0d1923524c319f75db7507b65acad2f244c88bf8 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Tue, 7 Feb 2017 13:58:40 +0100
Subject: [PATCH] Json file can be used as dft input from now on as well

---
 src/storm-dft-cli/storm-dyftee.cpp | 24 ++++++++++++++++--------
 1 file changed, 16 insertions(+), 8 deletions(-)

diff --git a/src/storm-dft-cli/storm-dyftee.cpp b/src/storm-dft-cli/storm-dyftee.cpp
index 3ec3b0ac0..9a8cd033b 100644
--- a/src/storm-dft-cli/storm-dyftee.cpp
+++ b/src/storm-dft-cli/storm-dyftee.cpp
@@ -36,23 +36,31 @@
 /*!
  * Load DFT from filename, build corresponding Model and check against given property.
  *
- * @param filename Path to DFT file in Galileo format.
  * @param property PCTC formula capturing the property to check.
  * @param symred Flag whether symmetry reduction should be used.
  * @param allowModularisation Flag whether modularisation should be applied if possible.
  * @param enableDC Flag whether Don't Care propagation should be used.
  */
 template <typename ValueType>
-void analyzeDFT(std::string filename, std::string property, bool symred, bool allowModularisation, bool enableDC, double approximationError) {
-    std::cout << "Running DFT analysis on file " << filename << " with property " << property << std::endl;
+void analyzeDFT(std::string property, bool symred, bool allowModularisation, bool enableDC, double approximationError) {
+    storm::settings::modules::DFTSettings const& dftSettings = storm::settings::getModule<storm::settings::modules::DFTSettings>();
+
+    std::shared_ptr<storm::storage::DFT<ValueType>> dft;
+    if (dftSettings.isDftJsonFileSet()) {
+        storm::parser::DFTJsonParser<ValueType> parser;
+        std::cout << "Running DFT analysis on file " << dftSettings.getDftJsonFilename() << " with property " << property << std::endl;
+        dft = std::make_shared<storm::storage::DFT<ValueType>>(parser.parseJson(dftSettings.getDftJsonFilename()));
+    } else {
+        storm::parser::DFTGalileoParser<ValueType> parser;
+        std::cout << "Running DFT analysis on file " << dftSettings.getDftFilename() << " with property " << property << std::endl;
+        dft = std::make_shared<storm::storage::DFT<ValueType>>(parser.parseDFT(dftSettings.getDftFilename()));
+    }
 
-    storm::parser::DFTGalileoParser<ValueType> parser;
-    storm::storage::DFT<ValueType> dft = parser.parseDFT(filename);
     std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForExplicit(property));
     STORM_LOG_ASSERT(formulas.size() == 1, "Wrong number of formulas.");
 
     storm::modelchecker::DFTModelChecker<ValueType> modelChecker;
-    modelChecker.check(dft, formulas[0], symred, allowModularisation, enableDC, approximationError);
+    modelChecker.check(*dft, formulas[0], symred, allowModularisation, enableDC, approximationError);
     modelChecker.printTimings();
     modelChecker.printResult();
 }
@@ -247,12 +255,12 @@ int main(const int argc, const char** argv) {
         // From this point on we are ready to carry out the actual computations.
         if (parametric) {
 #ifdef STORM_HAVE_CARL
-            analyzeDFT<storm::RationalFunction>(dftSettings.getDftFilename(), pctlFormula, dftSettings.useSymmetryReduction(), dftSettings.useModularisation(), !dftSettings.isDisableDC(), approximationError);
+            analyzeDFT<storm::RationalFunction>(pctlFormula, dftSettings.useSymmetryReduction(), dftSettings.useModularisation(), !dftSettings.isDisableDC(), approximationError);
 #else
             STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameters are not supported in this build.");
 #endif
         } else {
-            analyzeDFT<double>(dftSettings.getDftFilename(), pctlFormula, dftSettings.useSymmetryReduction(), dftSettings.useModularisation(), !dftSettings.isDisableDC(), approximationError);
+            analyzeDFT<double>(pctlFormula, dftSettings.useSymmetryReduction(), dftSettings.useModularisation(), !dftSettings.isDisableDC(), approximationError);
         }
         
         // All operations have now been performed, so we clean up everything and terminate.