From b93f5c2f624ebb87316d191b7104badcd65dc23f Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@rwth-aachen.de>
Date: Fri, 19 Feb 2016 16:19:36 +0100
Subject: [PATCH] refactored a bit, plus bisimulation is now done

Former-commit-id: 42877cdb29c91063c626f4efd711fc8f2d1460d0
---
 src/builder/ExplicitDFTModelBuilder.cpp |  1 -
 src/storm-dyftee.cpp                    | 23 ++++++++++++++++++++---
 2 files changed, 20 insertions(+), 4 deletions(-)

diff --git a/src/builder/ExplicitDFTModelBuilder.cpp b/src/builder/ExplicitDFTModelBuilder.cpp
index c6d59d6cb..cbb9b69d0 100644
--- a/src/builder/ExplicitDFTModelBuilder.cpp
+++ b/src/builder/ExplicitDFTModelBuilder.cpp
@@ -145,7 +145,6 @@ namespace storm {
                 }
             }
             
-            model->printModelInformationToStream(std::cout);
             return model;
         }
 
diff --git a/src/storm-dyftee.cpp b/src/storm-dyftee.cpp
index 805ef7570..2160ed210 100644
--- a/src/storm-dyftee.cpp
+++ b/src/storm-dyftee.cpp
@@ -16,12 +16,19 @@
  */
 template <typename ValueType>
 void analyzeDFT(std::string filename, std::string property, bool symred = false) {
+    storm::settings::SettingsManager& manager = storm::settings::mutableManager();
+    manager.setFromString("");
+
     // 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;
-    
+    std::cout << "Parse formula..." << std::endl;
+    std::vector<std::shared_ptr<storm::logic::Formula>> parsedFormulas = storm::parseFormulasForExplicit(property);
+    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas(parsedFormulas.begin(), parsedFormulas.end());
+    assert(formulas.size() == 1);
+    std::cout << "parsed formula." << std::endl;
     if(symred) {
         std::cout << dft.getElementsString() << std::endl;
         auto colouring = dft.colourDFT();
@@ -36,10 +43,20 @@ void analyzeDFT(std::string filename, std::string property, bool symred = false)
     std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.buildModel(labeloptions);
     std::cout << "Built Model" << std::endl;
 
+    
+    model->printModelInformationToStream(std::cout);
+    
+    std::cout << "Bisimulation..." << std::endl;
+    
+    if (model->isOfType(storm::models::ModelType::Ctmc)) {
+            model =  storm::performDeterministicSparseBisimulationMinimization<storm::models::sparse::Ctmc<ValueType>>(model->template as<storm::models::sparse::Ctmc<ValueType>>(), formulas, storm::storage::BisimulationType::Weak)->template as<storm::models::sparse::Ctmc<ValueType>>();
+    }
+    
+    
+    model->printModelInformationToStream(std::cout);
+    
     // 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> result(storm::verifySparseModel(model, formulas[0]));
     assert(result);
     std::cout << "Result: ";