From 8a01765005d5a60a2a91b299976c3463c00f1e56 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 23 Jul 2017 18:43:10 +0200 Subject: [PATCH] enabling symbolic bisimulation from cli --- src/storm/api/bisimulation.h | 18 ++++++++++++++++++ src/storm/cli/cli.cpp | 19 ++++++++++++++++++- src/storm/storage/SparseMatrix.cpp | 5 ++--- .../dd/bisimulation/QuotientExtractor.cpp | 7 ------- 4 files changed, 38 insertions(+), 11 deletions(-) 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 + typename std::enable_if::value, std::shared_ptr>>::type performBisimulationMinimization(std::shared_ptr> const& model, std::vector> 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 decomposition(*model, formulas); + decomposition.compute(); + return decomposition.getQuotient(); + } + + template + typename std::enable_if::value, std::shared_ptr>>::type performBisimulationMinimization(std::shared_ptr> const& model, std::vector> 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 + std::shared_ptr> preprocessDdModelBisimulation(std::shared_ptr> 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(model, createFormulasToRespect(input.properties)); + } + template std::pair, bool> preprocessDdModel(std::shared_ptr> const& model, SymbolicInput const& input) { - return std::make_pair(model, false); + auto bisimulationSettings = storm::settings::getModule(); + auto generalSettings = storm::settings::getModule(); + std::pair>, bool> result = std::make_pair(model, false); + + if (generalSettings.isBisimulationSet()) { + result.first = preprocessDdModelBisimulation(model, input, bisimulationSettings); + result.second = true; + } + + return result; } template 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 sparseExtractor(model.getManager(), model.getRowVariables()); storm::storage::SparseMatrix 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> result; if (model.getType() == storm::models::ModelType::Dtmc) { result = std::make_shared>(std::move(quotientTransitionMatrix), std::move(quotientStateLabeling));