Small refactoring

Former-commit-id: 102054c604

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

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

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;
 }
 
 /*!