From c8d2cf17242d36e81ebe493d264b5ff93cba009b Mon Sep 17 00:00:00 2001
From: Mavo <matthias.volk@rwth-aachen.de>
Date: Sat, 9 Jan 2016 11:23:36 +0100
Subject: [PATCH] Better distinction between parametric and non-parametric DFTs

Former-commit-id: 57ac698a3876d3f6fe1828469d4c7c6d2426aa41
---
 src/storm-dyftee.cpp | 82 +++++++++++++++++++++++++++++---------------
 1 file changed, 54 insertions(+), 28 deletions(-)

diff --git a/src/storm-dyftee.cpp b/src/storm-dyftee.cpp
index 906e9df21..2e9e88bbf 100644
--- a/src/storm-dyftee.cpp
+++ b/src/storm-dyftee.cpp
@@ -5,24 +5,62 @@
 #include "modelchecker/results/CheckResult.h"
 #include "utility/storm.h"
 
-#define VALUE_TYPE storm::RationalFunction
+/*!
+ * Load DFT from filename, build corresponding CTMC and check against given property.
+ *
+ * @param filename Path to DFT file in Galileo format.
+ * @param property PCTC formula capturing the property to check.
+ */
+template <typename ValueType>
+void analyzeDFT(std::string filename, std::string property) {
+    // Parsing DFT
+    std::cout << "Parsing DFT file..." << std::endl;
+    storm::parser::DFTGalileoParser<ValueType> parser;
+    storm::storage::DFT<ValueType> dft = parser.parseDFT(filename);
+    std::cout << "Built data structure" << std::endl;
+
+    // Building CTMC
+    std::cout << "Building CTMC..." << std::endl;
+    storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft);
+    std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.buildCTMC();
+    std::cout << "Built CTMC" << std::endl;
+
+    // Model checking
+    std::cout << "Model checking..." << std::endl;
+    std::vector<std::shared_ptr<storm::logic::Formula>> formulas = storm::parseFormulasForExplicit(property);
+    assert(formulas.size() == 1);
+    std::unique_ptr<storm::modelchecker::CheckResult> resultCtmc(storm::verifySparseModel(model, formulas[0]));
+    assert(resultCtmc);
+    std::cout << "Result (initial states): ";
+    resultCtmc->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates()));
+    std::cout << *resultCtmc << std::endl;
+    std::cout << "Checked CTMC" << std::endl;
+}
 
-/*
+/*!
  * Entry point for the DyFTeE backend.
+ *
+ * @param argc The argc argument of main().
+ * @param argv The argv argument of main().
+ * @return Return code, 0 if successfull, not 0 otherwise.
  */
 int main(int argc, char** argv) {
     if(argc < 2) {
         std::cout <<  "Storm-DyFTeE should be called with a filename as argument." << std::endl;
         return 1;
     }
-    // Construct PCTL forumla
-    std::string inputFormula;
-    if (argc < 3) {
-        // Set explicit reachability formula
-        inputFormula = "Pmax=?[true U \"failed\"]";
-    } else {
-        // Read formula from input
-        inputFormula = argv[2];
+
+    // Parse cli arguments
+    bool parametric = false;
+    std::string filename = argv[1];
+    std::string pctlFormula = "Pmax=?[true U \"failed\"]";
+    for (int i = 2; i < argc; ++i) {
+        std::string option = argv[i];
+        if (option == "--parametric") {
+            parametric = true;
+        } else {
+            pctlFormula = option;
+        }
     }
 
     storm::utility::setUp();
@@ -30,23 +68,11 @@ int main(int argc, char** argv) {
     logger.setLogLevel(level);
     logger.getAppender("mainConsoleAppender")->setThreshold(level);
 
-    std::cout << "Parsing DFT file..." << std::endl;
-    storm::parser::DFTGalileoParser<VALUE_TYPE> parser;
-    storm::storage::DFT<VALUE_TYPE> dft = parser.parseDFT(argv[1]);
-    std::cout << "Built data structure" << std::endl;
+    std::cout << "Running " << (parametric ? "parametric " : "") << "DFT analysis on file " << filename << " with property " << pctlFormula << std::endl;
 
-    // Verify the model as CTMC
-    std::cout << "Building CTMC..." << std::endl;
-    storm::builder::ExplicitDFTModelBuilder<VALUE_TYPE> builder(dft);
-    std::shared_ptr<storm::models::sparse::Model<VALUE_TYPE>> model = builder.buildCTMC();
-    std::cout << "Built CTMC" << std::endl;
-    std::cout << "Model checking..." << std::endl;
-    std::vector<std::shared_ptr<storm::logic::Formula>> formulas = storm::parseFormulasForExplicit(inputFormula);
-    assert(formulas.size() == 1);
-    std::unique_ptr<storm::modelchecker::CheckResult> resultCtmc(storm::verifySparseModel(model, formulas[0]));
-    assert(resultCtmc);
-    std::cout << "Result (initial states): ";
-    resultCtmc->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates()));
-    std::cout << *resultCtmc << std::endl;
-    std::cout << "Checked CTMC" << std::endl;
+    if (parametric) {
+        analyzeDFT<storm::RationalFunction>(filename, pctlFormula);
+    } else {
+        analyzeDFT<double>(filename, pctlFormula);
+    }
 }