From 35f5f9de1529b780a2c21b00b695d80f2de0dc72 Mon Sep 17 00:00:00 2001
From: Mavo <matthias.volk@rwth-aachen.de>
Date: Tue, 9 Feb 2016 11:42:07 +0100
Subject: [PATCH] Small refactoring

Former-commit-id: 102054c6043d08de0caf3db6db0ee85684aa1c98
---
 src/builder/ExplicitDFTModelBuilder.cpp |  3 ++-
 src/builder/ExplicitDFTModelBuilder.h   |  2 +-
 src/storm-dyftee.cpp                    | 16 ++++++++--------
 3 files changed, 11 insertions(+), 10 deletions(-)

diff --git a/src/builder/ExplicitDFTModelBuilder.cpp b/src/builder/ExplicitDFTModelBuilder.cpp
index d4de53d64..1bfc445e7 100644
--- a/src/builder/ExplicitDFTModelBuilder.cpp
+++ b/src/builder/ExplicitDFTModelBuilder.cpp
@@ -1,5 +1,6 @@
 #include "src/builder/ExplicitDFTModelBuilder.h"
 #include <src/models/sparse/MarkovAutomaton.h>
+#include <src/models/sparse/CTMC.h>
 #include <src/utility/constants.h>
 #include <src/exceptions/UnexpectedException.h>
 #include <map>
@@ -13,7 +14,7 @@ namespace storm {
         }
 
         template <typename ValueType>
-        std::shared_ptr<storm::models::sparse::Model<ValueType>> ExplicitDFTModelBuilder<ValueType>::buildMA() {
+        std::shared_ptr<storm::models::sparse::Model<ValueType>> ExplicitDFTModelBuilder<ValueType>::buildModel() {
             // Initialize
             DFTStatePointer state = std::make_shared<storm::storage::DFTState<ValueType>>(mDft, newIndex++);
             mStates.findOrAdd(state->status(), state);
diff --git a/src/builder/ExplicitDFTModelBuilder.h b/src/builder/ExplicitDFTModelBuilder.h
index edb2e1a94..b2d27aadd 100644
--- a/src/builder/ExplicitDFTModelBuilder.h
+++ b/src/builder/ExplicitDFTModelBuilder.h
@@ -53,7 +53,7 @@ namespace storm {
                 // 2^nrBE is upper bound for state space
             }
 
-            std::shared_ptr<storm::models::sparse::Model<ValueType>> buildMA();
+            std::shared_ptr<storm::models::sparse::Model<ValueType>> buildModel();
 
         private:
             void exploreStates(std::queue<DFTStatePointer>& stateQueue, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<uint_fast64_t>& markovianStates, std::vector<ValueType>& exitRates);
diff --git a/src/storm-dyftee.cpp b/src/storm-dyftee.cpp
index a86347e3b..a8122f2bd 100644
--- a/src/storm-dyftee.cpp
+++ b/src/storm-dyftee.cpp
@@ -6,7 +6,7 @@
 #include "utility/storm.h"
 
 /*!
- * Load DFT from filename, build corresponding Markov Automaton and check against given property.
+ * 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.
@@ -20,20 +20,20 @@ void analyzeDFT(std::string filename, std::string property) {
     std::cout << "Built data structure" << std::endl;
 
     // Building Markov Automaton
-    std::cout << "Building Markov Automaton..." << std::endl;
+    std::cout << "Building Model..." << std::endl;
     storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft);
-    std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.buildMA();
-    std::cout << "Built Markov Automaton" << std::endl;
+    std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.buildModel();
+    std::cout << "Built Model" << 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> resultMA(storm::verifySparseModel(model, formulas[0]));
-    assert(resultMA);
+    std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySparseModel(model, formulas[0]));
+    assert(result);
     std::cout << "Result: ";
-    resultMA->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates()));
-    std::cout << *resultMA << std::endl;
+    result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates()));
+    std::cout << *result << std::endl;
 }
 
 /*!