diff --git a/src/storm/api/bisimulation.h b/src/storm/api/bisimulation.h
index be95e335d..ac8797fc8 100644
--- a/src/storm/api/bisimulation.h
+++ b/src/storm/api/bisimulation.h
@@ -3,6 +3,9 @@
#include "storm/storage/bisimulation/DeterministicModelBisimulationDecomposition.h"
#include "storm/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h"
+#include "storm/storage/dd/DdType.h"
+#include "storm/storage/dd/BisimulationDecomposition.h"
+
#include "storm/utility/macros.h"
#include "storm/exceptions/NotSupportedException.h"
@@ -51,5 +54,20 @@ namespace storm {
}
}
+ template <storm::dd::DdType DdType, typename ValueType>
+ typename std::enable_if<DdType == storm::dd::DdType::Sylvan || std::is_same<ValueType, double>::value, std::shared_ptr<storm::models::Model<ValueType>>>::type performBisimulationMinimization(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
+ STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Dtmc) || model->isOfType(storm::models::ModelType::Ctmc), storm::exceptions::NotSupportedException, "Symbolic bisimulation minimization is currently only available for DTMCs and CTMCs.");
+
+ storm::dd::BisimulationDecomposition<DdType, ValueType> decomposition(*model, formulas);
+ decomposition.compute();
+ return decomposition.getQuotient();
+ }
+
+ template <storm::dd::DdType DdType, typename ValueType>
+ typename std::enable_if<DdType != storm::dd::DdType::Sylvan && !std::is_same<ValueType, double>::value, std::shared_ptr<storm::models::Model<ValueType>>>::type performBisimulationMinimization(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Symbolic bisimulation minimization is not supported for this combination of DD library and value type.");
+ return nullptr;
+ }
+
}
}
diff --git a/src/storm/cli/cli.cpp b/src/storm/cli/cli.cpp
index 343006c6d..7a1ef8066 100644
--- a/src/storm/cli/cli.cpp
+++ b/src/storm/cli/cli.cpp
@@ -480,9 +480,26 @@ namespace storm {
}
}
+ template <storm::dd::DdType DdType, typename ValueType>
+ std::shared_ptr<storm::models::Model<ValueType>> preprocessDdModelBisimulation(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model, SymbolicInput const& input, storm::settings::modules::BisimulationSettings const& bisimulationSettings) {
+ STORM_LOG_WARN_COND(!bisimulationSettings.isWeakBisimulationSet(), "Weak bisimulation is currently not supported on DDs. Falling back to strong bisimulation.");
+
+ STORM_LOG_INFO("Performing bisimulation minimization...");
+ return storm::api::performBisimulationMinimization<DdType, ValueType>(model, createFormulasToRespect(input.properties));
+ }
+
template <storm::dd::DdType DdType, typename ValueType>
std::pair<std::shared_ptr<storm::models::ModelBase>, bool> preprocessDdModel(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model, SymbolicInput const& input) {
- return std::make_pair(model, false);
+ auto bisimulationSettings = storm::settings::getModule<storm::settings::modules::BisimulationSettings>();
+ auto generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
+ std::pair<std::shared_ptr<storm::models::Model<ValueType>>, bool> result = std::make_pair(model, false);
+
+ if (generalSettings.isBisimulationSet()) {
+ result.first = preprocessDdModelBisimulation(model, input, bisimulationSettings);
+ result.second = true;
+ }
+
+ return result;
}
template <storm::dd::DdType DdType, typename ValueType>
diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp
index 9e779c108..7e239c14e 100644
--- a/src/storm/storage/SparseMatrix.cpp
+++ b/src/storm/storage/SparseMatrix.cpp
@@ -135,9 +135,8 @@ namespace storm {
bool fixCurrentRow = row == lastRow && column < lastColumn;
// If the element is in the same row and column as the previous entry, we add them up.
- if (row == lastRow && column == lastColumn) {
- columnsAndValues.back().setColumn(column);
- columnsAndValues.back().setValue(value);
+ if (row == lastRow && column == lastColumn && !columnsAndValues.empty()) {
+ columnsAndValues.back().setValue(columnsAndValues.back().getValue() + value);
} else {
// If we switched to another row, we have to adjust the missing entries in the row indices vector.
if (row != lastRow) {
diff --git a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp
index a59eed3bd..aee570395 100644
--- a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp
+++ b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp
@@ -492,17 +492,12 @@ namespace storm {
InternalSparseQuotientExtractor<DdType, ValueType> sparseExtractor(model.getManager(), model.getRowVariables());
storm::storage::SparseMatrix<ValueType> quotientTransitionMatrix = sparseExtractor.extractTransitionMatrix(model.getTransitionMatrix(), partition);
- std::cout << "Matrix has " << quotientTransitionMatrix.getEntryCount() << " entries" << std::endl;
-
storm::models::sparse::StateLabeling quotientStateLabeling(partition.getNumberOfBlocks());
quotientStateLabeling.addLabel("init", sparseExtractor.extractStates(model.getInitialStates(), partition));
- std::cout << "init: " << quotientStateLabeling.getStates("init").getNumberOfSetBits() << std::endl;
quotientStateLabeling.addLabel("deadlock", sparseExtractor.extractStates(model.getDeadlockStates(), partition));
- std::cout << "deadlock: " << quotientStateLabeling.getStates("init").getNumberOfSetBits() << std::endl;
for (auto const& label : partition.getPreservationInformation().getLabels()) {
quotientStateLabeling.addLabel(label, sparseExtractor.extractStates(model.getStates(label), partition));
- std::cout << label << ": " << quotientStateLabeling.getStates(label).getNumberOfSetBits() << std::endl;
}
for (auto const& expression : partition.getPreservationInformation().getExpressions()) {
std::stringstream stream;
@@ -513,11 +508,9 @@ namespace storm {
STORM_LOG_WARN("Duplicate label '" << expressionAsString << "', dropping second label definition.");
} else {
quotientStateLabeling.addLabel(stream.str(), sparseExtractor.extractStates(model.getStates(expression), partition));
- std::cout << stream.str() << ": " << quotientStateLabeling.getStates(stream.str()).getNumberOfSetBits() << std::endl;
}
}
-
std::shared_ptr<storm::models::sparse::Model<ValueType>> result;
if (model.getType() == storm::models::ModelType::Dtmc) {
result = std::make_shared<storm::models::sparse::Dtmc<ValueType>>(std::move(quotientTransitionMatrix), std::move(quotientStateLabeling));