Reenabled bisimulation, because carl now supports operator< for rational functions.

Former-commit-id: 9d7eef92ec

src/storage/DeterministicModelStrongBisimulationDecomposition.cpp

@@ -900,6 +900,6 @@ namespace storm {
         }
         
         template class DeterministicModelStrongBisimulationDecomposition<double>;
-//        template class DeterministicModelStrongBisimulationDecomposition<storm::RationalFunction>;
+        template class DeterministicModelStrongBisimulationDecomposition<storm::RationalFunction>;
     }
 }

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

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"
 /*!
@@ -44,10 +44,10 @@ 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>>();
-//        }
+        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;