From 656e823287de5a4ffdf7a9014068d4af81437f83 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Sun, 24 Jan 2021 22:18:55 +0100
Subject: [PATCH] Refactored DFT Api Test

---
 .../storm-dft/api/DftModelCheckerTest.cpp     | 27 +++++++++----------
 1 file changed, 12 insertions(+), 15 deletions(-)

diff --git a/src/test/storm-dft/api/DftModelCheckerTest.cpp b/src/test/storm-dft/api/DftModelCheckerTest.cpp
index 8c6bab4a8..9eb7145ea 100644
--- a/src/test/storm-dft/api/DftModelCheckerTest.cpp
+++ b/src/test/storm-dft/api/DftModelCheckerTest.cpp
@@ -72,38 +72,35 @@ namespace {
             return config;
         }
 
-        double analyzeMTTF(std::string const& file) {
+        double analyze(std::string const& file, std::string const& property) {
+            // Load, build and prepare DFT
             storm::transformations::dft::DftTransformator<double> dftTransformator = storm::transformations::dft::DftTransformator<double>();
             std::shared_ptr<storm::storage::DFT<double>> dft = dftTransformator.transformBinaryFDEPs(*(storm::api::loadDFTGalileoFile<double>(file)));
             EXPECT_TRUE(storm::api::isWellFormed(*dft).first);
-            std::string property = "Tmin=? [F \"failed\"]";
+
+            // Create property
             std::vector<std::shared_ptr<storm::logic::Formula const>> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property));
 
+            // Create relevant names
             std::vector<std::string> relevantNames;
             if (!config.useDC) {
                 relevantNames.push_back("all");
             }
             storm::utility::RelevantEvents relevantEvents = storm::api::computeRelevantEvents<ValueType>(*dft, properties, relevantNames, false);
 
+            // Perform model checking
             typename storm::modelchecker::DFTModelChecker<double>::dft_results results = storm::api::analyzeDFT<double>(*dft, properties, config.useSR, config.useMod, relevantEvents);
             return boost::get<double>(results[0]);
         }
 
+        double analyzeMTTF(std::string const& file) {
+            std::string property = "Tmin=? [F \"failed\"]";
+            return analyze(file, property);
+        }
+
         double analyzeReliability(std::string const &file, double bound) {
-            storm::transformations::dft::DftTransformator<double> dftTransformator = storm::transformations::dft::DftTransformator<double>();
-            std::shared_ptr<storm::storage::DFT<double>> dft = dftTransformator.transformBinaryFDEPs(*(storm::api::loadDFTGalileoFile<double>(file)));
-            EXPECT_TRUE(storm::api::isWellFormed(*dft).first);
             std::string property = "Pmin=? [F<=" + std::to_string(bound) + " \"failed\"]";
-            std::vector<std::shared_ptr<storm::logic::Formula const>> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property));
-
-            std::vector<std::string> relevantNames;
-            if (!config.useDC) {
-                relevantNames.push_back("all");
-            }
-            storm::utility::RelevantEvents relevantEvents = storm::api::computeRelevantEvents<ValueType>(*dft, properties, relevantNames, false);
-
-            typename storm::modelchecker::DFTModelChecker<double>::dft_results results = storm::api::analyzeDFT<double>(*dft, properties, config.useSR, config.useMod, relevantEvents);
-            return boost::get<double>(results[0]);
+            return analyze(file, property);
         }
 
     private: