enabling symbolic bisimulation from cli

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;
+        }
+
     }
 }

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>

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) {

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