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; -// template class DeterministicModelStrongBisimulationDecomposition; + template class DeterministicModelStrongBisimulationDecomposition; } } \ 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> dtmc = model->as>(); -// Perform bisimulation minimization if requested. -// if (storm::settings::generalSettings().isBisimulationSet()) { -// storm::storage::DeterministicModelStrongBisimulationDecomposition bisimulationDecomposition(*dtmc, true); -// dtmc = bisimulationDecomposition.getQuotient()->as>(); -// } + // Perform bisimulation minimization if requested. + if (storm::settings::generalSettings().isBisimulationSet()) { + storm::storage::DeterministicModelStrongBisimulationDecomposition bisimulationDecomposition(*dtmc, true); + dtmc = bisimulationDecomposition.getQuotient()->as>(); + } assert(dtmc); storm::modelchecker::reachability::CollectConstraints constraintCollector;