From 7464f958647b7db927f97d1672f0ca051d425d47 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Wed, 15 Oct 2014 10:22:49 +0200
Subject: [PATCH] Reenabled bisimulation, because carl now supports operator<
 for rational functions.

Former-commit-id: 9d7eef92ecd2d9e3964c171eb34482528b535292
---
 ...rministicModelStrongBisimulationDecomposition.cpp |  2 +-
 src/storage/expressions/ExpressionEvaluation.h       |  2 --
 src/stormParametric.cpp                              | 12 ++++++------
 3 files changed, 7 insertions(+), 9 deletions(-)

diff --git a/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp b/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp
index 92fb2a142..27cf123ff 100644
--- a/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp
+++ b/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp
@@ -900,6 +900,6 @@ namespace storm {
         }
         
         template class DeterministicModelStrongBisimulationDecomposition<double>;
-//        template class DeterministicModelStrongBisimulationDecomposition<storm::RationalFunction>;
+        template class DeterministicModelStrongBisimulationDecomposition<storm::RationalFunction>;
     }
 }
\ No newline at end of file
diff --git a/src/storage/expressions/ExpressionEvaluation.h b/src/storage/expressions/ExpressionEvaluation.h
index 156e8b0d3..29b05ea31 100644
--- a/src/storage/expressions/ExpressionEvaluation.h
+++ b/src/storage/expressions/ExpressionEvaluation.h
@@ -85,9 +85,7 @@ namespace storm {
 						mValue += visitor->value();
 						break;
 					case BinaryNumericalFunctionExpression::OperatorType::Minus:
-                        std::cout << "mValue: " << mValue << " - " << visitor->value() << std::endl;
 						mValue -= visitor->value();
-                        std::cout << mValue << std::endl;
 						break;
 					case BinaryNumericalFunctionExpression::OperatorType::Times:
 						mValue *= visitor->value();
diff --git a/src/stormParametric.cpp b/src/stormParametric.cpp
index c0ac68ef2..f5649a70f 100644
--- a/src/stormParametric.cpp
+++ b/src/stormParametric.cpp
@@ -10,7 +10,7 @@
 #include "src/modelchecker/reachability/CollectConstraints.h"
 
 #include "src/modelchecker/reachability/DirectEncoding.h"
-//#include "src/storage/DeterministicModelStrongBisimulationDecomposition.h"
+#include "src/storage/DeterministicModelStrongBisimulationDecomposition.h"
 #include "src/modelchecker/reachability/SparseSccModelChecker.h"
 #include "src/storage/parameters.h"
 /*!
@@ -43,11 +43,11 @@ int main(const int argc, const char** argv) {
 
         std::shared_ptr<storm::models::Dtmc<storm::RationalFunction>> dtmc = model->as<storm::models::Dtmc<storm::RationalFunction>>();
         
-//        Perform bisimulation minimization if requested.
-//        if (storm::settings::generalSettings().isBisimulationSet()) {
-//            storm::storage::DeterministicModelStrongBisimulationDecomposition<storm::RationalFunction> bisimulationDecomposition(*dtmc, true);
-//            dtmc = bisimulationDecomposition.getQuotient()->as<storm::models::Dtmc<storm::RationalFunction>>();
-//        }
+        // Perform bisimulation minimization if requested.
+        if (storm::settings::generalSettings().isBisimulationSet()) {
+            storm::storage::DeterministicModelStrongBisimulationDecomposition<storm::RationalFunction> bisimulationDecomposition(*dtmc, true);
+            dtmc = bisimulationDecomposition.getQuotient()->as<storm::models::Dtmc<storm::RationalFunction>>();
+        }
         
         assert(dtmc);
         storm::modelchecker::reachability::CollectConstraints<storm::RationalFunction> constraintCollector;