From 7f346d2f0b8b5624ba335f95eac70945bb5cc796 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 17 May 2017 21:35:48 +0200 Subject: [PATCH] more work on quotient extraction --- src/storm/abstraction/MenuGame.cpp | 2 +- src/storm/builder/DdJaniModelBuilder.cpp | 17 +- src/storm/builder/DdPrismModelBuilder.cpp | 18 +- src/storm/models/symbolic/Ctmc.cpp | 37 +++- src/storm/models/symbolic/Ctmc.h | 58 ++++++- .../models/symbolic/DeterministicModel.cpp | 19 ++- .../models/symbolic/DeterministicModel.h | 30 +++- src/storm/models/symbolic/Dtmc.cpp | 18 +- src/storm/models/symbolic/Dtmc.h | 28 ++- src/storm/models/symbolic/Mdp.cpp | 19 ++- src/storm/models/symbolic/Mdp.h | 31 +++- src/storm/models/symbolic/Model.cpp | 91 +++++++--- src/storm/models/symbolic/Model.h | 44 +++-- .../models/symbolic/NondeterministicModel.cpp | 30 +++- .../models/symbolic/NondeterministicModel.h | 33 +++- .../symbolic/StochasticTwoPlayerGame.cpp | 33 +++- .../models/symbolic/StochasticTwoPlayerGame.h | 39 ++++- .../settings/modules/BisimulationSettings.cpp | 19 +++ .../settings/modules/BisimulationSettings.h | 16 +- src/storm/storage/dd/Add.cpp | 62 ++++++- src/storm/storage/dd/Add.h | 13 +- src/storm/storage/dd/Bdd.cpp | 52 +++++- src/storm/storage/dd/Bdd.h | 11 ++ .../storage/dd/BisimulationDecomposition.cpp | 20 ++- .../storage/dd/BisimulationDecomposition.h | 9 +- src/storm/storage/dd/DdManager.cpp | 15 ++ src/storm/storage/dd/DdManager.h | 15 +- .../storage/dd/bisimulation/Partition.cpp | 114 ++++++++++--- src/storm/storage/dd/bisimulation/Partition.h | 81 ++++++--- .../bisimulation/PreservationInformation.cpp | 24 +++ .../dd/bisimulation/PreservationInformation.h | 30 ++++ .../dd/bisimulation/QuotientExtractor.cpp | 161 ++++++++++++++++++ .../dd/bisimulation/QuotientExtractor.h | 37 ++++ src/storm/utility/storm.h | 5 +- 34 files changed, 1056 insertions(+), 175 deletions(-) create mode 100644 src/storm/storage/dd/bisimulation/PreservationInformation.cpp create mode 100644 src/storm/storage/dd/bisimulation/PreservationInformation.h create mode 100644 src/storm/storage/dd/bisimulation/QuotientExtractor.cpp create mode 100644 src/storm/storage/dd/bisimulation/QuotientExtractor.h diff --git a/src/storm/abstraction/MenuGame.cpp b/src/storm/abstraction/MenuGame.cpp index 799003820..9272784ec 100644 --- a/src/storm/abstraction/MenuGame.cpp +++ b/src/storm/abstraction/MenuGame.cpp @@ -29,7 +29,7 @@ namespace storm { std::set const& player2Variables, std::set const& allNondeterminismVariables, std::set const& probabilisticBranchingVariables, - std::map> const& expressionToBddMap) : storm::models::symbolic::StochasticTwoPlayerGame(manager, reachableStates, initialStates, deadlockStates, transitionMatrix.sumAbstract(probabilisticBranchingVariables), rowVariables, nullptr, columnVariables, nullptr, rowColumnMetaVariablePairs, player1Variables, player2Variables, allNondeterminismVariables), extendedTransitionMatrix(transitionMatrix), probabilisticBranchingVariables(probabilisticBranchingVariables), expressionToBddMap(expressionToBddMap), bottomStates(bottomStates) { + std::map> const& expressionToBddMap) : storm::models::symbolic::StochasticTwoPlayerGame(manager, reachableStates, initialStates, deadlockStates, transitionMatrix.sumAbstract(probabilisticBranchingVariables), rowVariables, nullptr, columnVariables, rowColumnMetaVariablePairs, player1Variables, player2Variables, allNondeterminismVariables), extendedTransitionMatrix(transitionMatrix), probabilisticBranchingVariables(probabilisticBranchingVariables), expressionToBddMap(expressionToBddMap), bottomStates(bottomStates) { // Intentionally left empty. } diff --git a/src/storm/builder/DdJaniModelBuilder.cpp b/src/storm/builder/DdJaniModelBuilder.cpp index 6ea6e4470..f0ca60f85 100644 --- a/src/storm/builder/DdJaniModelBuilder.cpp +++ b/src/storm/builder/DdJaniModelBuilder.cpp @@ -141,7 +141,7 @@ namespace storm { template class ParameterCreator { public: - void create(storm::jani::Model const& model, storm::adapters::AddExpressionAdapter& rowExpressionAdapter, storm::adapters::AddExpressionAdapter& columnExpressionAdapter) { + void create(storm::jani::Model const& model, storm::adapters::AddExpressionAdapter& rowExpressionAdapter) { // Intentionally left empty: no support for parameters for this data type. } @@ -160,14 +160,13 @@ namespace storm { // Intentionally left empty. } - void create(storm::jani::Model const& model, storm::adapters::AddExpressionAdapter& rowExpressionAdapter, storm::adapters::AddExpressionAdapter& columnExpressionAdapter) { + void create(storm::jani::Model const& model, storm::adapters::AddExpressionAdapter& rowExpressionAdapter) { for (auto const& constant : model.getConstants()) { if (!constant.isDefined()) { carl::Variable carlVariable = carl::freshRealVariable(constant.getExpressionVariable().getName()); parameters.insert(carlVariable); auto rf = convertVariableToPolynomial(carlVariable); rowExpressionAdapter.setValue(constant.getExpressionVariable(), rf); - columnExpressionAdapter.setValue(constant.getExpressionVariable(), rf); } } } @@ -202,8 +201,7 @@ namespace storm { CompositionVariables() : manager(std::make_shared>()), variableToRowMetaVariableMap(std::make_shared>()), rowExpressionAdapter(std::make_shared>(manager, variableToRowMetaVariableMap)), - variableToColumnMetaVariableMap(std::make_shared>()), - columnExpressionAdapter(std::make_shared>(manager, variableToColumnMetaVariableMap)) { + variableToColumnMetaVariableMap(std::make_shared>()) { // Intentionally left empty. } @@ -217,7 +215,6 @@ namespace storm { // The meta variables for the column encoding. std::set columnMetaVariables; std::shared_ptr> variableToColumnMetaVariableMap; - std::shared_ptr> columnExpressionAdapter; // All pairs of row/column meta variables. std::vector> rowColumnMetaVariablePairs; @@ -392,7 +389,7 @@ namespace storm { } ParameterCreator parameterCreator; - parameterCreator.create(model, *result.rowExpressionAdapter, *result.columnExpressionAdapter); + parameterCreator.create(model, *result.rowExpressionAdapter); if (std::is_same::value) { result.parameters = parameterCreator.getParameters(); } @@ -1706,11 +1703,11 @@ namespace storm { std::shared_ptr> createModel(storm::jani::ModelType const& modelType, CompositionVariables const& variables, ModelComponents const& modelComponents) { std::shared_ptr> result; if (modelType == storm::jani::ModelType::DTMC) { - result = std::make_shared>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, modelComponents.labelToExpressionMap, modelComponents.rewardModels); + result = std::make_shared>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.rowColumnMetaVariablePairs, modelComponents.labelToExpressionMap, modelComponents.rewardModels); } else if (modelType == storm::jani::ModelType::CTMC) { - result = std::make_shared>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, modelComponents.labelToExpressionMap, modelComponents.rewardModels); + result = std::make_shared>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.rowColumnMetaVariablePairs, modelComponents.labelToExpressionMap, modelComponents.rewardModels); } else if (modelType == storm::jani::ModelType::MDP || modelType == storm::jani::ModelType::LTS) { - result = std::make_shared>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, variables.allNondeterminismVariables, modelComponents.labelToExpressionMap, modelComponents.rewardModels); + result = std::make_shared>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.rowColumnMetaVariablePairs, variables.allNondeterminismVariables, modelComponents.labelToExpressionMap, modelComponents.rewardModels); } else { STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Model type '" << modelType << "' not supported."); } diff --git a/src/storm/builder/DdPrismModelBuilder.cpp b/src/storm/builder/DdPrismModelBuilder.cpp index b0749616d..73bf1c1e0 100644 --- a/src/storm/builder/DdPrismModelBuilder.cpp +++ b/src/storm/builder/DdPrismModelBuilder.cpp @@ -34,7 +34,7 @@ namespace storm { template class ParameterCreator { public: - void create(storm::prism::Program const& program, storm::adapters::AddExpressionAdapter& rowExpressionAdapter, storm::adapters::AddExpressionAdapter& columnExpressionAdapter) { + void create(storm::prism::Program const& program, storm::adapters::AddExpressionAdapter& rowExpressionAdapter) { // Intentionally left empty: no support for parameters for this data type. } @@ -53,14 +53,13 @@ namespace storm { // Intentionally left empty. } - void create(storm::prism::Program const& program, storm::adapters::AddExpressionAdapter& rowExpressionAdapter, storm::adapters::AddExpressionAdapter& columnExpressionAdapter) { + void create(storm::prism::Program const& program, storm::adapters::AddExpressionAdapter& rowExpressionAdapter) { for (auto const& constant : program.getConstants()) { if (!constant.isDefined()) { carl::Variable carlVariable = carl::freshRealVariable(constant.getExpressionVariable().getName()); parameters.insert(carlVariable); auto rf = convertVariableToPolynomial(carlVariable); rowExpressionAdapter.setValue(constant.getExpressionVariable(), rf); - columnExpressionAdapter.setValue(constant.getExpressionVariable(), rf); } } } @@ -93,14 +92,14 @@ namespace storm { template class DdPrismModelBuilder::GenerationInformation { public: - GenerationInformation(storm::prism::Program const& program) : program(program), manager(std::make_shared>()), rowMetaVariables(), variableToRowMetaVariableMap(std::make_shared>()), rowExpressionAdapter(std::make_shared>(manager, variableToRowMetaVariableMap)), columnMetaVariables(), variableToColumnMetaVariableMap((std::make_shared>())), columnExpressionAdapter(std::make_shared>(manager, variableToColumnMetaVariableMap)), rowColumnMetaVariablePairs(), nondeterminismMetaVariables(), variableToIdentityMap(), allGlobalVariables(), moduleToIdentityMap(), parameters() { + GenerationInformation(storm::prism::Program const& program) : program(program), manager(std::make_shared>()), rowMetaVariables(), variableToRowMetaVariableMap(std::make_shared>()), rowExpressionAdapter(std::make_shared>(manager, variableToRowMetaVariableMap)), columnMetaVariables(), variableToColumnMetaVariableMap((std::make_shared>())), rowColumnMetaVariablePairs(), nondeterminismMetaVariables(), variableToIdentityMap(), allGlobalVariables(), moduleToIdentityMap(), parameters() { // Initializes variables and identity DDs. createMetaVariablesAndIdentities(); // Initialize the parameters (if any). ParameterCreator parameterCreator; - parameterCreator.create(this->program, *this->rowExpressionAdapter, *this->columnExpressionAdapter); + parameterCreator.create(this->program, *this->rowExpressionAdapter); if (std::is_same::value) { this->parameters = parameterCreator.getParameters(); } @@ -120,7 +119,6 @@ namespace storm { // The meta variables for the column encoding. std::set columnMetaVariables; std::shared_ptr> variableToColumnMetaVariableMap; - std::shared_ptr> columnExpressionAdapter; // All pairs of row/column meta variables. std::vector> rowColumnMetaVariablePairs; @@ -1358,7 +1356,7 @@ namespace storm { } else { STORM_LOG_THROW(labelName == "init" || labelName == "deadlock", storm::exceptions::InvalidArgumentException, "Terminal states refer to illegal label '" << labelName << "'."); } - } + } if (terminalExpression.isInitialized()) { // If the expression refers to constants of the model, we need to substitute them. @@ -1484,11 +1482,11 @@ namespace storm { std::shared_ptr> result; if (program.getModelType() == storm::prism::Program::ModelType::DTMC) { - result = std::shared_ptr>(new storm::models::symbolic::Dtmc(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, labelToExpressionMapping, rewardModels)); + result = std::shared_ptr>(new storm::models::symbolic::Dtmc(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.rowColumnMetaVariablePairs, labelToExpressionMapping, rewardModels)); } else if (program.getModelType() == storm::prism::Program::ModelType::CTMC) { - result = std::shared_ptr>(new storm::models::symbolic::Ctmc(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, system.stateActionDd, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, labelToExpressionMapping, rewardModels)); + result = std::shared_ptr>(new storm::models::symbolic::Ctmc(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, system.stateActionDd, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.rowColumnMetaVariablePairs, labelToExpressionMapping, rewardModels)); } else if (program.getModelType() == storm::prism::Program::ModelType::MDP) { - result = std::shared_ptr>(new storm::models::symbolic::Mdp(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, generationInfo.allNondeterminismVariables, labelToExpressionMapping, rewardModels)); + result = std::shared_ptr>(new storm::models::symbolic::Mdp(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.rowColumnMetaVariablePairs, generationInfo.allNondeterminismVariables, labelToExpressionMapping, rewardModels)); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Invalid model type."); } diff --git a/src/storm/models/symbolic/Ctmc.cpp b/src/storm/models/symbolic/Ctmc.cpp index 543bc7d90..05907bc03 100644 --- a/src/storm/models/symbolic/Ctmc.cpp +++ b/src/storm/models/symbolic/Ctmc.cpp @@ -21,11 +21,10 @@ namespace storm { std::set const& rowVariables, std::shared_ptr> rowExpressionAdapter, std::set const& columnVariables, - std::shared_ptr> columnExpressionAdapter, std::vector> const& rowColumnMetaVariablePairs, std::map labelToExpressionMap, std::unordered_map const& rewardModels) - : DeterministicModel(storm::models::ModelType::Ctmc, manager, reachableStates, initialStates, deadlockStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, labelToExpressionMap, rewardModels) { + : DeterministicModel(storm::models::ModelType::Ctmc, manager, reachableStates, initialStates, deadlockStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, rowColumnMetaVariablePairs, labelToExpressionMap, rewardModels) { // Intentionally left empty. } @@ -39,11 +38,41 @@ namespace storm { std::set const& rowVariables, std::shared_ptr> rowExpressionAdapter, std::set const& columnVariables, - std::shared_ptr> columnExpressionAdapter, std::vector> const& rowColumnMetaVariablePairs, std::map labelToExpressionMap, std::unordered_map const& rewardModels) - : DeterministicModel(storm::models::ModelType::Ctmc, manager, reachableStates, initialStates, deadlockStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, labelToExpressionMap, rewardModels), exitRates(exitRateVector) { + : DeterministicModel(storm::models::ModelType::Ctmc, manager, reachableStates, initialStates, deadlockStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, rowColumnMetaVariablePairs, labelToExpressionMap, rewardModels), exitRates(exitRateVector) { + // Intentionally left empty. + } + + template + Ctmc::Ctmc(std::shared_ptr> manager, + storm::dd::Bdd reachableStates, + storm::dd::Bdd initialStates, + storm::dd::Bdd deadlockStates, + storm::dd::Add transitionMatrix, + std::set const& rowVariables, + std::set const& columnVariables, + std::vector> const& rowColumnMetaVariablePairs, + std::map> labelToBddMap, + std::unordered_map const& rewardModels) + : DeterministicModel(storm::models::ModelType::Ctmc, manager, reachableStates, initialStates, deadlockStates, transitionMatrix, rowVariables, columnVariables, rowColumnMetaVariablePairs, labelToBddMap, rewardModels) { + // Intentionally left empty. + } + + template + Ctmc::Ctmc(std::shared_ptr> manager, + storm::dd::Bdd reachableStates, + storm::dd::Bdd initialStates, + storm::dd::Bdd deadlockStates, + storm::dd::Add transitionMatrix, + boost::optional> exitRateVector, + std::set const& rowVariables, + std::set const& columnVariables, + std::vector> const& rowColumnMetaVariablePairs, + std::map> labelToBddMap, + std::unordered_map const& rewardModels) + : DeterministicModel(storm::models::ModelType::Ctmc, manager, reachableStates, initialStates, deadlockStates, transitionMatrix, rowVariables, columnVariables, rowColumnMetaVariablePairs, labelToBddMap, rewardModels), exitRates(exitRateVector) { // Intentionally left empty. } diff --git a/src/storm/models/symbolic/Ctmc.h b/src/storm/models/symbolic/Ctmc.h index c0c4054a3..68c4e7b35 100644 --- a/src/storm/models/symbolic/Ctmc.h +++ b/src/storm/models/symbolic/Ctmc.h @@ -36,8 +36,6 @@ namespace storm { * @param rowExpressionAdapter An object that can be used to translate expressions in terms of the row * meta variables. * @param columVariables The set of column meta variables used in the DDs. - * @param columnExpressionAdapter An object that can be used to translate expressions in terms of the - * column meta variables. * @param rowColumnMetaVariablePairs All pairs of row/column meta variables. * @param labelToExpressionMap A mapping from label names to their defining expressions. * @param rewardModels The reward models associated with the model. @@ -50,7 +48,6 @@ namespace storm { std::set const& rowVariables, std::shared_ptr> rowExpressionAdapter, std::set const& columnVariables, - std::shared_ptr> columnExpressionAdapter, std::vector> const& rowColumnMetaVariablePairs, std::map labelToExpressionMap = std::map(), std::unordered_map const& rewardModels = std::unordered_map()); @@ -68,8 +65,6 @@ namespace storm { * @param rowExpressionAdapter An object that can be used to translate expressions in terms of the row * meta variables. * @param columVariables The set of column meta variables used in the DDs. - * @param columnExpressionAdapter An object that can be used to translate expressions in terms of the - * column meta variables. * @param rowColumnMetaVariablePairs All pairs of row/column meta variables. * @param labelToExpressionMap A mapping from label names to their defining expressions. * @param rewardModels The reward models associated with the model. @@ -83,11 +78,62 @@ namespace storm { std::set const& rowVariables, std::shared_ptr> rowExpressionAdapter, std::set const& columnVariables, - std::shared_ptr> columnExpressionAdapter, std::vector> const& rowColumnMetaVariablePairs, std::map labelToExpressionMap = std::map(), std::unordered_map const& rewardModels = std::unordered_map()); + /*! + * Constructs a model from the given data. + * + * @param manager The manager responsible for the decision diagrams. + * @param reachableStates A DD representing the reachable states. + * @param initialStates A DD representing the initial states of the model. + * @param deadlockStates A DD representing the deadlock states of the model. + * @param transitionMatrix The matrix representing the transitions in the model. + * @param rowVariables The set of row meta variables used in the DDs. + * @param columVariables The set of column meta variables used in the DDs. + * @param rowColumnMetaVariablePairs All pairs of row/column meta variables. + * @param labelToBddMap A mapping from label names to their defining BDDs. + * @param rewardModels The reward models associated with the model. + */ + Ctmc(std::shared_ptr> manager, + storm::dd::Bdd reachableStates, + storm::dd::Bdd initialStates, + storm::dd::Bdd deadlockStates, + storm::dd::Add transitionMatrix, + std::set const& rowVariables, + std::set const& columnVariables, + std::vector> const& rowColumnMetaVariablePairs, + std::map> labelToBddMap = std::map>(), + std::unordered_map const& rewardModels = std::unordered_map()); + + /*! + * Constructs a model from the given data. + * + * @param manager The manager responsible for the decision diagrams. + * @param reachableStates A DD representing the reachable states. + * @param initialStates A DD representing the initial states of the model. + * @param deadlockStates A DD representing the deadlock states of the model. + * @param transitionMatrix The matrix representing the transitions in the model. + * @param exitRateVector The vector specifying the exit rates for the states. + * @param rowVariables The set of row meta variables used in the DDs. + * @param columVariables The set of column meta variables used in the DDs. + * @param rowColumnMetaVariablePairs All pairs of row/column meta variables. + * @param labelToBddMap A mapping from label names to their defining BDDs. + * @param rewardModels The reward models associated with the model. + */ + Ctmc(std::shared_ptr> manager, + storm::dd::Bdd reachableStates, + storm::dd::Bdd initialStates, + storm::dd::Bdd deadlockStates, + storm::dd::Add transitionMatrix, + boost::optional> exitRateVector, + std::set const& rowVariables, + std::set const& columnVariables, + std::vector> const& rowColumnMetaVariablePairs, + std::map> labelToBddMap = std::map>(), + std::unordered_map const& rewardModels = std::unordered_map()); + /*! * Retrieves the exit rate vector of the CTMC. * diff --git a/src/storm/models/symbolic/DeterministicModel.cpp b/src/storm/models/symbolic/DeterministicModel.cpp index a9d9c92df..28543fec3 100644 --- a/src/storm/models/symbolic/DeterministicModel.cpp +++ b/src/storm/models/symbolic/DeterministicModel.cpp @@ -22,11 +22,26 @@ namespace storm { std::set const& rowVariables, std::shared_ptr> rowExpressionAdapter, std::set const& columnVariables, - std::shared_ptr> columnExpressionAdapter, std::vector> const& rowColumnMetaVariablePairs, std::map labelToExpressionMap, std::unordered_map const& rewardModels) - : Model(modelType, manager, reachableStates, initialStates, deadlockStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, labelToExpressionMap, rewardModels) { + : Model(modelType, manager, reachableStates, initialStates, deadlockStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, rowColumnMetaVariablePairs, labelToExpressionMap, rewardModels) { + // Intentionally left empty. + } + + template + DeterministicModel::DeterministicModel(storm::models::ModelType const& modelType, + std::shared_ptr> manager, + storm::dd::Bdd reachableStates, + storm::dd::Bdd initialStates, + storm::dd::Bdd deadlockStates, + storm::dd::Add transitionMatrix, + std::set const& rowVariables, + std::set const& columnVariables, + std::vector> const& rowColumnMetaVariablePairs, + std::map> labelToBddMap, + std::unordered_map const& rewardModels) + : Model(modelType, manager, reachableStates, initialStates, deadlockStates, transitionMatrix, rowVariables, columnVariables, rowColumnMetaVariablePairs, labelToBddMap, rewardModels) { // Intentionally left empty. } diff --git a/src/storm/models/symbolic/DeterministicModel.h b/src/storm/models/symbolic/DeterministicModel.h index af8bc1fc1..83d25fe0d 100644 --- a/src/storm/models/symbolic/DeterministicModel.h +++ b/src/storm/models/symbolic/DeterministicModel.h @@ -37,8 +37,6 @@ namespace storm { * @param rowExpressionAdapter An object that can be used to translate expressions in terms of the row * meta variables. * @param columVariables The set of column meta variables used in the DDs. - * @param columnExpressionAdapter An object that can be used to translate expressions in terms of the - * column meta variables. * @param rowColumnMetaVariablePairs All pairs of row/column meta variables. * @param labelToExpressionMap A mapping from label names to their defining expressions. * @param rewardModels The reward models associated with the model. @@ -52,10 +50,36 @@ namespace storm { std::set const& rowVariables, std::shared_ptr> rowExpressionAdapter, std::set const& columnVariables, - std::shared_ptr> columnExpressionAdapter, std::vector> const& rowColumnMetaVariablePairs, std::map labelToExpressionMap = std::map(), std::unordered_map const& rewardModels = std::unordered_map()); + + /*! + * Constructs a model from the given data. + * + * @param modelType The type of the model. + * @param manager The manager responsible for the decision diagrams. + * @param reachableStates A DD representing the reachable states. + * @param initialStates A DD representing the initial states of the model. + * @param deadlockStates A DD representing the deadlock states of the model. + * @param transitionMatrix The matrix representing the transitions in the model. + * @param rowVariables The set of row meta variables used in the DDs. + * @param columVariables The set of column meta variables used in the DDs. + * @param rowColumnMetaVariablePairs All pairs of row/column meta variables. + * @param labelToBddMap A mapping from label names to their defining BDDs. + * @param rewardModels The reward models associated with the model. + */ + DeterministicModel(storm::models::ModelType const& modelType, + std::shared_ptr> manager, + storm::dd::Bdd reachableStates, + storm::dd::Bdd initialStates, + storm::dd::Bdd deadlockStates, + storm::dd::Add transitionMatrix, + std::set const& rowVariables, + std::set const& columnVariables, + std::vector> const& rowColumnMetaVariablePairs, + std::map> labelToBddMap = std::map>(), + std::unordered_map const& rewardModels = std::unordered_map()); }; } // namespace symbolic diff --git a/src/storm/models/symbolic/Dtmc.cpp b/src/storm/models/symbolic/Dtmc.cpp index 3f7153ead..6278d7052 100644 --- a/src/storm/models/symbolic/Dtmc.cpp +++ b/src/storm/models/symbolic/Dtmc.cpp @@ -21,11 +21,25 @@ namespace storm { std::set const& rowVariables, std::shared_ptr> rowExpressionAdapter, std::set const& columnVariables, - std::shared_ptr> columnExpressionAdapter, std::vector> const& rowColumnMetaVariablePairs, std::map labelToExpressionMap, std::unordered_map const& rewardModels) - : DeterministicModel(storm::models::ModelType::Dtmc, manager, reachableStates, initialStates, deadlockStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, labelToExpressionMap, rewardModels) { + : DeterministicModel(storm::models::ModelType::Dtmc, manager, reachableStates, initialStates, deadlockStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, rowColumnMetaVariablePairs, labelToExpressionMap, rewardModels) { + // Intentionally left empty. + } + + template + Dtmc::Dtmc(std::shared_ptr> manager, + storm::dd::Bdd reachableStates, + storm::dd::Bdd initialStates, + storm::dd::Bdd deadlockStates, + storm::dd::Add transitionMatrix, + std::set const& rowVariables, + std::set const& columnVariables, + std::vector> const& rowColumnMetaVariablePairs, + std::map> labelToBddMap, + std::unordered_map const& rewardModels) + : DeterministicModel(storm::models::ModelType::Dtmc, manager, reachableStates, initialStates, deadlockStates, transitionMatrix, rowVariables, columnVariables, rowColumnMetaVariablePairs, labelToBddMap, rewardModels) { // Intentionally left empty. } diff --git a/src/storm/models/symbolic/Dtmc.h b/src/storm/models/symbolic/Dtmc.h index 538ff4977..ebe837e1c 100644 --- a/src/storm/models/symbolic/Dtmc.h +++ b/src/storm/models/symbolic/Dtmc.h @@ -36,8 +36,6 @@ namespace storm { * @param rowExpressionAdapter An object that can be used to translate expressions in terms of the row * meta variables. * @param columVariables The set of column meta variables used in the DDs. - * @param columnExpressionAdapter An object that can be used to translate expressions in terms of the - * column meta variables. * @param rowColumnMetaVariablePairs All pairs of row/column meta variables. * @param labelToExpressionMap A mapping from label names to their defining expressions. * @param rewardModels The reward models associated with the model. @@ -50,10 +48,34 @@ namespace storm { std::set const& rowVariables, std::shared_ptr> rowExpressionAdapter, std::set const& columnVariables, - std::shared_ptr> columnExpressionAdapter, std::vector> const& rowColumnMetaVariablePairs, std::map labelToExpressionMap = std::map(), std::unordered_map const& rewardModels = std::unordered_map()); + + /*! + * Constructs a model from the given data. + * + * @param manager The manager responsible for the decision diagrams. + * @param reachableStates A DD representing the reachable states. + * @param initialStates A DD representing the initial states of the model. + * @param deadlockStates A DD representing the deadlock states of the model. + * @param transitionMatrix The matrix representing the transitions in the model. + * @param rowVariables The set of row meta variables used in the DDs. + * @param columVariables The set of column meta variables used in the DDs. + * @param rowColumnMetaVariablePairs All pairs of row/column meta variables. + * @param labelToBddMap A mapping from label names to their defining BDDs. + * @param rewardModels The reward models associated with the model. + */ + Dtmc(std::shared_ptr> manager, + storm::dd::Bdd reachableStates, + storm::dd::Bdd initialStates, + storm::dd::Bdd deadlockStates, + storm::dd::Add transitionMatrix, + std::set const& rowVariables, + std::set const& columnVariables, + std::vector> const& rowColumnMetaVariablePairs, + std::map> labelToBddMap = std::map>(), + std::unordered_map const& rewardModels = std::unordered_map()); }; } // namespace symbolic diff --git a/src/storm/models/symbolic/Mdp.cpp b/src/storm/models/symbolic/Mdp.cpp index 20bd9ad2c..1a1644338 100644 --- a/src/storm/models/symbolic/Mdp.cpp +++ b/src/storm/models/symbolic/Mdp.cpp @@ -21,12 +21,27 @@ namespace storm { std::set const& rowVariables, std::shared_ptr> rowExpressionAdapter, std::set const& columnVariables, - std::shared_ptr> columnExpressionAdapter, std::vector> const& rowColumnMetaVariablePairs, std::set const& nondeterminismVariables, std::map labelToExpressionMap, std::unordered_map const& rewardModels) - : NondeterministicModel(storm::models::ModelType::Mdp, manager, reachableStates, initialStates, deadlockStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, nondeterminismVariables, labelToExpressionMap, rewardModels) { + : NondeterministicModel(storm::models::ModelType::Mdp, manager, reachableStates, initialStates, deadlockStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, rowColumnMetaVariablePairs, nondeterminismVariables, labelToExpressionMap, rewardModels) { + // Intentionally left empty. + } + + template + Mdp::Mdp(std::shared_ptr> manager, + storm::dd::Bdd reachableStates, + storm::dd::Bdd initialStates, + storm::dd::Bdd deadlockStates, + storm::dd::Add transitionMatrix, + std::set const& rowVariables, + std::set const& columnVariables, + std::vector> const& rowColumnMetaVariablePairs, + std::set const& nondeterminismVariables, + std::map> labelToBddMap, + std::unordered_map const& rewardModels) + : NondeterministicModel(storm::models::ModelType::Mdp, manager, reachableStates, initialStates, deadlockStates, transitionMatrix, rowVariables, columnVariables, rowColumnMetaVariablePairs, nondeterminismVariables, labelToBddMap, rewardModels) { // Intentionally left empty. } diff --git a/src/storm/models/symbolic/Mdp.h b/src/storm/models/symbolic/Mdp.h index ab5b59b99..771f0bd05 100644 --- a/src/storm/models/symbolic/Mdp.h +++ b/src/storm/models/symbolic/Mdp.h @@ -37,8 +37,6 @@ namespace storm { * @param rowExpressionAdapter An object that can be used to translate expressions in terms of the row * meta variables. * @param columVariables The set of column meta variables used in the DDs. - * @param columnExpressionAdapter An object that can be used to translate expressions in terms of the - * column meta variables. * @param rowColumnMetaVariablePairs All pairs of row/column meta variables. * @param nondeterminismVariables The meta variables used to encode the nondeterminism in the model. * @param labelToExpressionMap A mapping from label names to their defining expressions. @@ -52,12 +50,39 @@ namespace storm { std::set const& rowVariables, std::shared_ptr> rowExpressionAdapter, std::set const& columnVariables, - std::shared_ptr> columnExpressionAdapter, std::vector> const& rowColumnMetaVariablePairs, std::set const& nondeterminismVariables, std::map labelToExpressionMap = std::map(), std::unordered_map const& rewardModels = std::unordered_map()); + /*! + * Constructs a model from the given data. + * + * @param modelType The type of the model. + * @param manager The manager responsible for the decision diagrams. + * @param reachableStates A DD representing the reachable states. + * @param initialStates A DD representing the initial states of the model. + * @param deadlockStates A DD representing the deadlock states of the model. + * @param transitionMatrix The matrix representing the transitions in the model. + * @param rowVariables The set of row meta variables used in the DDs. + * @param columVariables The set of column meta variables used in the DDs. + * @param rowColumnMetaVariablePairs All pairs of row/column meta variables. + * @param nondeterminismVariables The meta variables used to encode the nondeterminism in the model. + * @param labelToBddMap A mapping from label names to their defining BDDs. + * @param rewardModels The reward models associated with the model. + */ + Mdp(std::shared_ptr> manager, + storm::dd::Bdd reachableStates, + storm::dd::Bdd initialStates, + storm::dd::Bdd deadlockStates, + storm::dd::Add transitionMatrix, + std::set const& rowVariables, + std::set const& columnVariables, + std::vector> const& rowColumnMetaVariablePairs, + std::set const& nondeterminismVariables, + std::map> labelToBddMap = std::map>(), + std::unordered_map const& rewardModels = std::unordered_map()); + }; } // namespace symbolic diff --git a/src/storm/models/symbolic/Model.cpp b/src/storm/models/symbolic/Model.cpp index 94b185b15..1ec8ef7d9 100644 --- a/src/storm/models/symbolic/Model.cpp +++ b/src/storm/models/symbolic/Model.cpp @@ -17,6 +17,7 @@ #include "storm/utility/dd.h" #include "storm/exceptions/NotSupportedException.h" +#include "storm/exceptions/WrongFormatException.h" namespace storm { namespace models { @@ -31,12 +32,31 @@ namespace storm { std::set const& rowVariables, std::shared_ptr> rowExpressionAdapter, std::set const& columnVariables, - std::shared_ptr> columnExpressionAdapter, std::vector> const& rowColumnMetaVariablePairs, std::map labelToExpressionMap, std::unordered_map const& rewardModels) - : ModelBase(modelType), manager(manager), reachableStates(reachableStates), initialStates(initialStates), deadlockStates(deadlockStates), transitionMatrix(transitionMatrix), rowVariables(rowVariables), rowExpressionAdapter(rowExpressionAdapter), columnVariables(columnVariables), columnExpressionAdapter(columnExpressionAdapter), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), labelToExpressionMap(labelToExpressionMap), rewardModels(rewardModels) { - // Intentionally left empty. + : ModelBase(modelType), manager(manager), reachableStates(reachableStates), transitionMatrix(transitionMatrix), rowVariables(rowVariables), rowExpressionAdapter(rowExpressionAdapter), columnVariables(columnVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), labelToExpressionMap(labelToExpressionMap), rewardModels(rewardModels) { + this->labelToBddMap.emplace("init", initialStates); + this->labelToBddMap.emplace("deadlock", deadlockStates); + } + + template + Model::Model(storm::models::ModelType const& modelType, + std::shared_ptr> manager, + storm::dd::Bdd reachableStates, + storm::dd::Bdd initialStates, + storm::dd::Bdd deadlockStates, + storm::dd::Add transitionMatrix, + std::set const& rowVariables, + std::set const& columnVariables, + std::vector> const& rowColumnMetaVariablePairs, + std::map> labelToBddMap, + std::unordered_map const& rewardModels) + : ModelBase(modelType), manager(manager), reachableStates(reachableStates), transitionMatrix(transitionMatrix), rowVariables(rowVariables), rowExpressionAdapter(nullptr), columnVariables(columnVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), labelToBddMap(labelToBddMap), rewardModels(rewardModels) { + STORM_LOG_THROW(this->labelToBddMap.find("init") == this->labelToBddMap.end(), storm::exceptions::WrongFormatException, "Illegal custom label 'init'."); + STORM_LOG_THROW(this->labelToBddMap.find("deadlock") == this->labelToBddMap.end(), storm::exceptions::WrongFormatException, "Illegal custom label 'deadlock'."); + this->labelToBddMap.emplace("init", initialStates); + this->labelToBddMap.emplace("deadlock", deadlockStates); } template @@ -53,7 +73,7 @@ namespace storm { storm::dd::DdManager& Model::getManager() const { return *manager; } - + template std::shared_ptr> const& Model::getManagerAsSharedPointer() const { return manager; @@ -66,24 +86,33 @@ namespace storm { template storm::dd::Bdd const& Model::getInitialStates() const { - return initialStates; + return labelToBddMap.at("init"); } - + template storm::dd::Bdd const& Model::getDeadlockStates() const { - return deadlockStates; + return labelToBddMap.at("deadlock"); } template storm::dd::Bdd Model::getStates(std::string const& label) const { - STORM_LOG_THROW(labelToExpressionMap.find(label) != labelToExpressionMap.end(), storm::exceptions::IllegalArgumentException, "The label " << label << " is invalid for the labeling of the model."); - return this->getStates(labelToExpressionMap.at(label)); + // First check whether we have a BDD for this label. + auto bddIt = labelToBddMap.find(label); + if (bddIt != labelToBddMap.end()) { + return bddIt->second; + } else { + // If not, check for an expression we can translate. + auto expressionIt = labelToExpressionMap.find(label); + STORM_LOG_THROW(expressionIt != labelToExpressionMap.end(), storm::exceptions::IllegalArgumentException, "The label " << label << " is invalid for the labeling of the model."); + return this->getStates(expressionIt->second); + } } template storm::expressions::Expression Model::getExpression(std::string const& label) const { - STORM_LOG_THROW(labelToExpressionMap.find(label) != labelToExpressionMap.end(), storm::exceptions::IllegalArgumentException, "The label " << label << " is invalid for the labeling of the model."); - return labelToExpressionMap.at(label); + auto expressionIt = labelToExpressionMap.find(label); + STORM_LOG_THROW(expressionIt != labelToExpressionMap.end(), storm::exceptions::IllegalArgumentException, "Cannot retrieve the expression for the label " << label << "."); + return expressionIt->second; } template @@ -93,17 +122,32 @@ namespace storm { } else if (expression.isFalse()) { return manager->getBddZero(); } + + // Look up the string equivalent of the expression. + std::stringstream stream; + stream << expression; + auto bddIt = labelToBddMap.find(stream.str()); + if (bddIt != labelToBddMap.end()) { + return bddIt->second; + } + + // Finally try to translate the expression with an adapter. STORM_LOG_THROW(rowExpressionAdapter != nullptr, storm::exceptions::InvalidOperationException, "Cannot create BDD for expression without expression adapter."); return rowExpressionAdapter->translateExpression(expression).toBdd() && this->reachableStates; } template bool Model::hasLabel(std::string const& label) const { - auto labelIt = labelToExpressionMap.find(label); - if (labelIt != labelToExpressionMap.end()) { + auto bddIt = labelToBddMap.find(label); + if (bddIt != labelToBddMap.end()) { + return true; + } + + auto expressionIt = labelToExpressionMap.find(label); + if (expressionIt != labelToExpressionMap.end()) { return true; } else { - return label == "init" || label == "deadlock"; + return false; } } @@ -179,13 +223,13 @@ namespace storm { STORM_LOG_THROW(this->hasUniqueRewardModel(), storm::exceptions::InvalidOperationException, "Cannot retrieve unique reward model, because there is no unique one."); return this->rewardModels.cbegin()->second; } - + template typename Model::RewardModelType& Model::getUniqueRewardModel() { STORM_LOG_THROW(this->hasUniqueRewardModel(), storm::exceptions::InvalidOperationException, "Cannot retrieve unique reward model, because there is no unique one."); return this->rewardModels.begin()->second; } - + template bool Model::hasUniqueRewardModel() const { return this->rewardModels.size() == 1; @@ -195,7 +239,7 @@ namespace storm { bool Model::hasRewardModel() const { return !this->rewardModels.empty(); } - + template std::unordered_map::RewardModelType> const& Model::getRewardModels() const { return this->rewardModels; @@ -206,7 +250,7 @@ namespace storm { this->printModelInformationHeaderToStream(out); this->printModelInformationFooterToStream(out); } - + template std::vector Model::getLabels() const { std::vector labels; @@ -229,7 +273,10 @@ namespace storm { this->printRewardModelsInformationToStream(out); this->printDdVariableInformationToStream(out); out << std::endl; - out << "Labels: \t" << this->labelToExpressionMap.size() << std::endl; + out << "Labels: \t" << (this->labelToExpressionMap.size() + this->labelToBddMap.size()) << std::endl; + for (auto const& label : labelToBddMap) { + out << " * " << label.first << " -> " << label.second.getNonZeroCount() << " state(s) (" << label.second.getNodeCount() << " nodes)" << std::endl; + } for (auto const& label : labelToExpressionMap) { out << " * " << label.first << std::endl; } @@ -278,7 +325,7 @@ namespace storm { std::set const& Model::getParameters() const { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This value type does not support parameters."); } - + template<> void Model::addParameters(std::set const& parameters) { this->parameters.insert(parameters.begin(), parameters.end()); @@ -288,13 +335,13 @@ namespace storm { std::set const& Model::getParameters() const { return parameters; } - + // Explicitly instantiate the template class. template class Model; template class Model; template class Model; - template class Model; + template class Model; } // namespace symbolic } // namespace models } // namespace storm diff --git a/src/storm/models/symbolic/Model.h b/src/storm/models/symbolic/Model.h index fa7d683ff..cae2e3c85 100644 --- a/src/storm/models/symbolic/Model.h +++ b/src/storm/models/symbolic/Model.h @@ -73,8 +73,6 @@ namespace storm { * @param rowExpressionAdapter An object that can be used to translate expressions in terms of the row * meta variables. * @param columVariables The set of column meta variables used in the DDs. - * @param columnExpressionAdapter An object that can be used to translate expressions in terms of the - * column meta variables. * @param rowColumnMetaVariablePairs All pairs of row/column meta variables. * @param labelToExpressionMap A mapping from label names to their defining expressions. * @param rewardModels The reward models associated with the model. @@ -88,11 +86,37 @@ namespace storm { std::set const& rowVariables, std::shared_ptr> rowExpressionAdapter, std::set const& columnVariables, - std::shared_ptr> columnExpressionAdapter, std::vector> const& rowColumnMetaVariablePairs, std::map labelToExpressionMap = std::map(), std::unordered_map const& rewardModels = std::unordered_map()); + /*! + * Constructs a model from the given data. + * + * @param modelType The type of the model. + * @param manager The manager responsible for the decision diagrams. + * @param reachableStates A DD representing the reachable states. + * @param initialStates A DD representing the initial states of the model. + * @param deadlockStates A DD representing the deadlock states of the model. + * @param transitionMatrix The matrix representing the transitions in the model. + * @param rowVariables The set of row meta variables used in the DDs. + * @param columVariables The set of column meta variables used in the DDs. + * @param rowColumnMetaVariablePairs All pairs of row/column meta variables. + * @param labelToBddMap A mapping from label names to their defining BDDs. + * @param rewardModels The reward models associated with the model. + */ + Model(storm::models::ModelType const& modelType, + std::shared_ptr> manager, + storm::dd::Bdd reachableStates, + storm::dd::Bdd initialStates, + storm::dd::Bdd deadlockStates, + storm::dd::Add transitionMatrix, + std::set const& rowVariables, + std::set const& columnVariables, + std::vector> const& rowColumnMetaVariablePairs, + std::map> labelToBddMap = std::map>(), + std::unordered_map const& rewardModels = std::unordered_map()); + virtual uint_fast64_t getNumberOfStates() const override; virtual uint_fast64_t getNumberOfTransitions() const override; @@ -324,13 +348,7 @@ namespace storm { // A vector representing the reachable states of the model. storm::dd::Bdd reachableStates; - - // A vector representing the initial states of the model. - storm::dd::Bdd initialStates; - - // A vector representing the deadlock states of the model. - storm::dd::Bdd deadlockStates; - + // A matrix representing transition relation. storm::dd::Add transitionMatrix; @@ -343,9 +361,6 @@ namespace storm { // The meta variables used to encode the columns of the transition matrix. std::set columnVariables; - // An adapter that can translate expressions to DDs over the column meta variables. - std::shared_ptr> columnExpressionAdapter; - // A vector holding all pairs of row and column meta variable pairs. This is used to swap the variables // in the DDs from row to column variables and vice versa. std::vector> rowColumnMetaVariablePairs; @@ -353,6 +368,9 @@ namespace storm { // A mapping from labels to expressions defining them. std::map labelToExpressionMap; + // A mapping from labels to BDDs characterizing the labeled states. + std::map> labelToBddMap; + // The reward models associated with the model. std::unordered_map rewardModels; diff --git a/src/storm/models/symbolic/NondeterministicModel.cpp b/src/storm/models/symbolic/NondeterministicModel.cpp index eb8c1a73d..6a42da0d3 100644 --- a/src/storm/models/symbolic/NondeterministicModel.cpp +++ b/src/storm/models/symbolic/NondeterministicModel.cpp @@ -23,15 +23,29 @@ namespace storm { std::set const& rowVariables, std::shared_ptr> rowExpressionAdapter, std::set const& columnVariables, - std::shared_ptr> columnExpressionAdapter, std::vector> const& rowColumnMetaVariablePairs, std::set const& nondeterminismVariables, std::map labelToExpressionMap, std::unordered_map const& rewardModels) - : Model(modelType, manager, reachableStates, initialStates, deadlockStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, labelToExpressionMap, rewardModels), nondeterminismVariables(nondeterminismVariables) { - - // Prepare the mask of illegal nondeterministic choices. - illegalMask = !(transitionMatrix.notZero().existsAbstract(this->getColumnVariables())) && reachableStates; + : Model(modelType, manager, reachableStates, initialStates, deadlockStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, rowColumnMetaVariablePairs, labelToExpressionMap, rewardModels), nondeterminismVariables(nondeterminismVariables) { + createIllegalMask(); + } + + template + NondeterministicModel::NondeterministicModel(storm::models::ModelType const& modelType, + std::shared_ptr> manager, + storm::dd::Bdd reachableStates, + storm::dd::Bdd initialStates, + storm::dd::Bdd deadlockStates, + storm::dd::Add transitionMatrix, + std::set const& rowVariables, + std::set const& columnVariables, + std::vector> const& rowColumnMetaVariablePairs, + std::set const& nondeterminismVariables, + std::map> labelToBddMap, + std::unordered_map const& rewardModels) + : Model(modelType, manager, reachableStates, initialStates, deadlockStates, transitionMatrix, rowVariables, columnVariables, rowColumnMetaVariablePairs, labelToBddMap, rewardModels), nondeterminismVariables(nondeterminismVariables) { + createIllegalMask(); } template @@ -76,6 +90,12 @@ namespace storm { out << ", nondeterminism: " << this->getNondeterminismVariables().size() << " meta variables (" << nondeterminismVariableCount << " DD variables)"; } + template + void NondeterministicModel::createIllegalMask() { + // Prepare the mask of illegal nondeterministic choices. + illegalMask = !(this->getTransitionMatrix().notZero().existsAbstract(this->getColumnVariables())) && this->getReachableStates(); + } + // Explicitly instantiate the template class. template class NondeterministicModel; template class NondeterministicModel; diff --git a/src/storm/models/symbolic/NondeterministicModel.h b/src/storm/models/symbolic/NondeterministicModel.h index cec5b0cb8..e97347c44 100644 --- a/src/storm/models/symbolic/NondeterministicModel.h +++ b/src/storm/models/symbolic/NondeterministicModel.h @@ -37,8 +37,6 @@ namespace storm { * @param rowExpressionAdapter An object that can be used to translate expressions in terms of the row * meta variables. * @param columVariables The set of column meta variables used in the DDs. - * @param columnExpressionAdapter An object that can be used to translate expressions in terms of the - * column meta variables. * @param rowColumnMetaVariablePairs All pairs of row/column meta variables. * @param nondeterminismVariables The meta variables used to encode the nondeterminism in the model. * @param labelToExpressionMap A mapping from label names to their defining expressions. @@ -53,12 +51,40 @@ namespace storm { std::set const& rowVariables, std::shared_ptr> rowExpressionAdapter, std::set const& columnVariables, - std::shared_ptr> columnExpressionAdapter, std::vector> const& rowColumnMetaVariablePairs, std::set const& nondeterminismVariables, std::map labelToExpressionMap = std::map(), std::unordered_map const& rewardModels = std::unordered_map()); + /*! + * Constructs a model from the given data. + * + * @param modelType The type of the model. + * @param manager The manager responsible for the decision diagrams. + * @param reachableStates A DD representing the reachable states. + * @param initialStates A DD representing the initial states of the model. + * @param deadlockStates A DD representing the deadlock states of the model. + * @param transitionMatrix The matrix representing the transitions in the model. + * @param rowVariables The set of row meta variables used in the DDs. + * @param columVariables The set of column meta variables used in the DDs. + * @param rowColumnMetaVariablePairs All pairs of row/column meta variables. + * @param nondeterminismVariables The meta variables used to encode the nondeterminism in the model. + * @param labelToBddMap A mapping from label names to their defining BDDs. + * @param rewardModels The reward models associated with the model. + */ + NondeterministicModel(storm::models::ModelType const& modelType, + std::shared_ptr> manager, + storm::dd::Bdd reachableStates, + storm::dd::Bdd initialStates, + storm::dd::Bdd deadlockStates, + storm::dd::Add transitionMatrix, + std::set const& rowVariables, + std::set const& columnVariables, + std::vector> const& rowColumnMetaVariablePairs, + std::set const& nondeterminismVariables, + std::map> labelToBddMap = std::map>(), + std::unordered_map const& rewardModels = std::unordered_map()); + /*! * Retrieves the number of nondeterministic choices in the model. * @@ -97,6 +123,7 @@ namespace storm { storm::dd::Bdd illegalMask; private: + void createIllegalMask(); // The meta variables encoding the nondeterminism in the model. std::set nondeterminismVariables; diff --git a/src/storm/models/symbolic/StochasticTwoPlayerGame.cpp b/src/storm/models/symbolic/StochasticTwoPlayerGame.cpp index fdff99c36..b9ed23107 100644 --- a/src/storm/models/symbolic/StochasticTwoPlayerGame.cpp +++ b/src/storm/models/symbolic/StochasticTwoPlayerGame.cpp @@ -22,23 +22,44 @@ namespace storm { std::set const& rowVariables, std::shared_ptr> rowExpressionAdapter, std::set const& columnVariables, - std::shared_ptr> columnExpressionAdapter, std::vector> const& rowColumnMetaVariablePairs, std::set const& player1Variables, std::set const& player2Variables, std::set const& nondeterminismVariables, std::map labelToExpressionMap, std::unordered_map const& rewardModels) - : NondeterministicModel(storm::models::ModelType::S2pg, manager, reachableStates, initialStates, deadlockStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, nondeterminismVariables, labelToExpressionMap, rewardModels), player1Variables(player1Variables), player2Variables(player2Variables) { - + : NondeterministicModel(storm::models::ModelType::S2pg, manager, reachableStates, initialStates, deadlockStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, rowColumnMetaVariablePairs, nondeterminismVariables, labelToExpressionMap, rewardModels), player1Variables(player1Variables), player2Variables(player2Variables) { + createIllegalMasks(); + } + + template + StochasticTwoPlayerGame::StochasticTwoPlayerGame(std::shared_ptr> manager, + storm::dd::Bdd reachableStates, + storm::dd::Bdd initialStates, + storm::dd::Bdd deadlockStates, + storm::dd::Add transitionMatrix, + std::set const& rowVariables, + std::set const& columnVariables, + std::vector> const& rowColumnMetaVariablePairs, + std::set const& player1Variables, + std::set const& player2Variables, + std::set const& nondeterminismVariables, + std::map> labelToBddMap, + std::unordered_map const& rewardModels) + : NondeterministicModel(storm::models::ModelType::S2pg, manager, reachableStates, initialStates, deadlockStates, transitionMatrix, rowVariables, columnVariables, rowColumnMetaVariablePairs, nondeterminismVariables, labelToBddMap, rewardModels), player1Variables(player1Variables), player2Variables(player2Variables) { + createIllegalMasks(); + } + + template + void StochasticTwoPlayerGame::createIllegalMasks() { // Compute legal player 1 mask. - illegalPlayer1Mask = transitionMatrix.notZero().existsAbstract(this->getColumnVariables()).existsAbstract(this->getPlayer2Variables()); + this->illegalPlayer1Mask = this->getTransitionMatrix().notZero().existsAbstract(this->getColumnVariables()).existsAbstract(this->getPlayer2Variables()); // Correct the mask for player 2. This is necessary, because it is not yet restricted to the legal choices of player 1. - illegalPlayer2Mask = this->getIllegalMask() && illegalPlayer1Mask; + illegalPlayer2Mask = this->getIllegalMask() && this->illegalPlayer1Mask; // Then set the illegal mask for player 1 correctly. - illegalPlayer1Mask = !illegalPlayer1Mask && reachableStates; + this->illegalPlayer1Mask = !illegalPlayer1Mask && this->getReachableStates(); } template diff --git a/src/storm/models/symbolic/StochasticTwoPlayerGame.h b/src/storm/models/symbolic/StochasticTwoPlayerGame.h index 15383b056..d3f009593 100644 --- a/src/storm/models/symbolic/StochasticTwoPlayerGame.h +++ b/src/storm/models/symbolic/StochasticTwoPlayerGame.h @@ -36,8 +36,6 @@ namespace storm { * @param rowExpressionAdapter An object that can be used to translate expressions in terms of the row * meta variables. * @param columVariables The set of column meta variables used in the DDs. - * @param columnExpressionAdapter An object that can be used to translate expressions in terms of the - * column meta variables. * @param rowColumnMetaVariablePairs All pairs of row/column meta variables. * @param player1Variables The meta variables used to encode the nondeterministic choices of player 1. * @param player2Variables The meta variables used to encode the nondeterministic choices of player 2. @@ -53,7 +51,6 @@ namespace storm { std::set const& rowVariables, std::shared_ptr> rowExpressionAdapter, std::set const& columnVariables, - std::shared_ptr> columnExpressionAdapter, std::vector> const& rowColumnMetaVariablePairs, std::set const& player1Variables, std::set const& player2Variables, @@ -61,6 +58,37 @@ namespace storm { std::map labelToExpressionMap = std::map(), std::unordered_map const& rewardModels = std::unordered_map()); + /*! + * Constructs a model from the given data. + * + * @param manager The manager responsible for the decision diagrams. + * @param reachableStates A DD representing the reachable states. + * @param initialStates A DD representing the initial states of the model. + * @param deadlockStates A DD representing the deadlock states of the model. + * @param transitionMatrix The matrix representing the transitions in the model. + * @param rowVariables The set of row meta variables used in the DDs. + * @param columVariables The set of column meta variables used in the DDs. + * @param rowColumnMetaVariablePairs All pairs of row/column meta variables. + * @param player1Variables The meta variables used to encode the nondeterministic choices of player 1. + * @param player2Variables The meta variables used to encode the nondeterministic choices of player 2. + * @param allNondeterminismVariables The meta variables used to encode the nondeterminism in the model. + * @param labelToBddMap A mapping from label names to their defining BDDs. + * @param rewardModels The reward models associated with the model. + */ + StochasticTwoPlayerGame(std::shared_ptr> manager, + storm::dd::Bdd reachableStates, + storm::dd::Bdd initialStates, + storm::dd::Bdd deadlockStates, + storm::dd::Add transitionMatrix, + std::set const& rowVariables, + std::set const& columnVariables, + std::vector> const& rowColumnMetaVariablePairs, + std::set const& player1Variables, + std::set const& player2Variables, + std::set const& allNondeterminismVariables, + std::map> labelToBddMap = std::map>(), + std::unordered_map const& rewardModels = std::unordered_map()); + /*! * Retrieeves the set of meta variables used to encode the nondeterministic choices of player 1. * @@ -90,6 +118,11 @@ namespace storm { storm::dd::Bdd getIllegalPlayer2Mask() const; private: + /*! + * Prepare all illegal masks. + */ + void createIllegalMasks(); + // A mask that characterizes all illegal player 1 choices. storm::dd::Bdd illegalPlayer1Mask; diff --git a/src/storm/settings/modules/BisimulationSettings.cpp b/src/storm/settings/modules/BisimulationSettings.cpp index a626df55e..fdef27093 100644 --- a/src/storm/settings/modules/BisimulationSettings.cpp +++ b/src/storm/settings/modules/BisimulationSettings.cpp @@ -14,10 +14,17 @@ namespace storm { const std::string BisimulationSettings::moduleName = "bisimulation"; const std::string BisimulationSettings::typeOptionName = "type"; + const std::string BisimulationSettings::representativeOptionName = "repr"; + const std::string BisimulationSettings::quotientFormatOptionName = "quot"; BisimulationSettings::BisimulationSettings() : ModuleSettings(moduleName) { std::vector types = { "strong", "weak" }; this->addOption(storm::settings::OptionBuilder(moduleName, typeOptionName, true, "Sets the kind of bisimulation quotienting used.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the type to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(types)).setDefaultValueString("strong").build()).build()); + + std::vector quotTypes = { "sparse", "dd" }; + this->addOption(storm::settings::OptionBuilder(moduleName, typeOptionName, true, "Sets the format in which the quotient is extracted (only applies to DD-based bisimulation).").addArgument(storm::settings::ArgumentBuilder::createStringArgument("format", "The format of the quotient.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(quotTypes)).setDefaultValueString("dd").build()).build()); + + this->addOption(storm::settings::OptionBuilder(moduleName, representativeOptionName, false, "Sets whether to use representatives in the quotient rather than block numbers.").build()); } bool BisimulationSettings::isStrongBisimulationSet() const { @@ -34,6 +41,18 @@ namespace storm { return false; } + BisimulationSettings::QuotientFormat BisimulationSettings::getQuotientFormat() const { + std::string quotientFormatAsString = this->getOption(typeOptionName).getArgumentByName("format").getValueAsString(); + if (quotientFormatAsString == "sparse") { + return BisimulationSettings::QuotientFormat::Sparse; + } + return BisimulationSettings::QuotientFormat::Dd; + } + + bool BisimulationSettings::isUseRepresentativesSet() const { + return this->getOption(representativeOptionName).getHasOptionBeenSet(); + } + bool BisimulationSettings::check() const { bool optionsSet = this->getOption(typeOptionName).getHasOptionBeenSet(); STORM_LOG_WARN_COND(storm::settings::getModule().isBisimulationSet() || !optionsSet, "Bisimulation minimization is not selected, so setting options for bisimulation has no effect."); diff --git a/src/storm/settings/modules/BisimulationSettings.h b/src/storm/settings/modules/BisimulationSettings.h index cd8dffbe2..ccdea9e5d 100644 --- a/src/storm/settings/modules/BisimulationSettings.h +++ b/src/storm/settings/modules/BisimulationSettings.h @@ -15,7 +15,7 @@ namespace storm { // An enumeration of all available bisimulation types. enum class BisimulationType { Strong, Weak }; - enum class CachingStrategy { FullDirect, FullLate, Granularity, Minimal }; + enum class QuotientFormat { Sparse, Dd }; /*! * Creates a new set of bisimulation settings. @@ -36,6 +36,18 @@ namespace storm { */ bool isWeakBisimulationSet() const; + /*! + * Retrieves the format in which the quotient is to be extracted. + * NOTE: only applies to DD-based bisimulation. + */ + QuotientFormat getQuotientFormat() const; + + /*! + * Retrieves whether representatives for blocks are to be used instead of the block numbers. + * NOTE: only applies to DD-based bisimulation. + */ + bool isUseRepresentativesSet() const; + virtual bool check() const override; // The name of the module. @@ -44,6 +56,8 @@ namespace storm { private: // Define the string names of the options as constants. static const std::string typeOptionName; + static const std::string representativeOptionName; + static const std::string quotientFormatOptionName; }; } // namespace modules } // namespace settings diff --git a/src/storm/storage/dd/Add.cpp b/src/storm/storage/dd/Add.cpp index 23403e843..70e277f3c 100644 --- a/src/storm/storage/dd/Add.cpp +++ b/src/storm/storage/dd/Add.cpp @@ -186,9 +186,37 @@ namespace storm { return internalAdd.equalModuloPrecision(other, precision, relative); } + template + Add Add::renameVariables(std::set const& from, std::set const& to) const { + std::vector> fromBdds; + std::vector> toBdds; + + for (auto const& metaVariable : from) { + STORM_LOG_THROW(this->containsMetaVariable(metaVariable), storm::exceptions::InvalidOperationException, "Cannot rename variable '" << metaVariable.getName() << "' that is not present."); + DdMetaVariable const& ddMetaVariable = this->getDdManager().getMetaVariable(metaVariable); + for (auto const& ddVariable : ddMetaVariable.getDdVariables()) { + fromBdds.push_back(ddVariable); + } + } + for (auto const& metaVariable : to) { + STORM_LOG_THROW(!this->containsMetaVariable(metaVariable), storm::exceptions::InvalidOperationException, "Cannot rename to variable '" << metaVariable.getName() << "' that is already present."); + DdMetaVariable const& ddMetaVariable = this->getDdManager().getMetaVariable(metaVariable); + for (auto const& ddVariable : ddMetaVariable.getDdVariables()) { + toBdds.push_back(ddVariable); + } + } + + std::set newContainedMetaVariables = to; + std::set_difference(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), from.begin(), from.end(), std::inserter(newContainedMetaVariables, newContainedMetaVariables.begin())); + + STORM_LOG_THROW(fromBdds.size() == toBdds.size(), storm::exceptions::InvalidArgumentException, "Unable to rename mismatching meta variables."); + return Add(this->getDdManager(), internalAdd.swapVariables(fromBdds, toBdds), newContainedMetaVariables); + } + template Add Add::swapVariables(std::vector> const& metaVariablePairs) const { std::set newContainedMetaVariables; + std::set deletedMetaVariables; std::vector> from; std::vector> to; for (auto const& metaVariablePair : metaVariablePairs) { @@ -197,12 +225,20 @@ namespace storm { // Keep track of the contained meta variables in the DD. if (this->containsMetaVariable(metaVariablePair.first)) { - newContainedMetaVariables.insert(metaVariablePair.second); - } - if (this->containsMetaVariable(metaVariablePair.second)) { - newContainedMetaVariables.insert(metaVariablePair.first); + if (this->containsMetaVariable(metaVariablePair.second)) { + // Nothing to do here. + } else { + newContainedMetaVariables.insert(metaVariablePair.second); + deletedMetaVariables.insert(metaVariablePair.first); + } + } else { + if (!this->containsMetaVariable(metaVariablePair.second)) { + // Nothing to do here. + } else { + newContainedMetaVariables.insert(metaVariablePair.first); + deletedMetaVariables.insert(metaVariablePair.second); + } } - for (auto const& ddVariable : variable1.getDdVariables()) { from.push_back(ddVariable); } @@ -210,13 +246,19 @@ namespace storm { to.push_back(ddVariable); } } + + std::set tmp; + std::set_difference(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), deletedMetaVariables.begin(), deletedMetaVariables.end(), std::inserter(tmp, tmp.begin())); + std::set containedMetaVariables; + std::set_union(tmp.begin(), tmp.end(), newContainedMetaVariables.begin(), newContainedMetaVariables.end(), std::inserter(containedMetaVariables, containedMetaVariables.begin())); STORM_LOG_THROW(from.size() == to.size(), storm::exceptions::InvalidArgumentException, "Unable to swap mismatching meta variables."); - return Add(this->getDdManager(), internalAdd.swapVariables(from, to), newContainedMetaVariables); + return Add(this->getDdManager(), internalAdd.swapVariables(from, to), containedMetaVariables); } template Add Add::permuteVariables(std::vector> const& metaVariablePairs) const { std::set newContainedMetaVariables; + std::set deletedMetaVariables; std::vector> from; std::vector> to; for (auto const& metaVariablePair : metaVariablePairs) { @@ -225,6 +267,7 @@ namespace storm { // Keep track of the contained meta variables in the DD. if (this->containsMetaVariable(metaVariablePair.first)) { + deletedMetaVariables.insert(metaVariablePair.first); newContainedMetaVariables.insert(metaVariablePair.second); } @@ -235,8 +278,13 @@ namespace storm { to.push_back(ddVariable); } } + + std::set tmp; + std::set_difference(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), deletedMetaVariables.begin(), deletedMetaVariables.end(), std::inserter(tmp, tmp.begin())); + std::set containedMetaVariables; + std::set_union(tmp.begin(), tmp.end(), newContainedMetaVariables.begin(), newContainedMetaVariables.end(), std::inserter(containedMetaVariables, containedMetaVariables.begin())); STORM_LOG_THROW(from.size() == to.size(), storm::exceptions::InvalidArgumentException, "Unable to swap mismatching meta variables."); - return Add(this->getDdManager(), internalAdd.permuteVariables(from, to), newContainedMetaVariables); + return Add(this->getDdManager(), internalAdd.permuteVariables(from, to), containedMetaVariables); } template diff --git a/src/storm/storage/dd/Add.h b/src/storm/storage/dd/Add.h index d8466e46d..ad217ecfc 100644 --- a/src/storm/storage/dd/Add.h +++ b/src/storm/storage/dd/Add.h @@ -310,6 +310,17 @@ namespace storm { * values. */ bool equalModuloPrecision(Add const& other, ValueType const& precision, bool relative = true) const; + + /*! + * Renames the given meta variables in the ADD. The number of the underlying DD variables of the both meta + * variable sets needs to agree. + * + * @param from The meta variables to be renamed. The current ADD needs to contain all these meta variables. + * @param to The meta variables that are the target of the renaming process. The current ADD must not contain + * any of these meta variables. + * @return The resulting ADD. + */ + Add renameVariables(std::set const& from, std::set const& to) const; /*! * Swaps the given pairs of meta variables in the ADD. The pairs of meta variables must be guaranteed to have @@ -319,7 +330,7 @@ namespace storm { * @return The resulting ADD. */ Add swapVariables(std::vector> const& metaVariablePairs) const; - + /*! * Permutes the given pairs of meta variables in the ADD. The pairs of meta variables must be guaranteed to have * the same number of underlying ADD variables. The first component of the i-th entry is substituted by the second component. diff --git a/src/storm/storage/dd/Bdd.cpp b/src/storm/storage/dd/Bdd.cpp index 7af94004c..bde9d4a30 100644 --- a/src/storm/storage/dd/Bdd.cpp +++ b/src/storm/storage/dd/Bdd.cpp @@ -253,6 +253,7 @@ namespace storm { template Bdd Bdd::swapVariables(std::vector> const& metaVariablePairs) const { std::set newContainedMetaVariables; + std::set deletedMetaVariables; std::vector> from; std::vector> to; for (auto const& metaVariablePair : metaVariablePairs) { @@ -261,10 +262,19 @@ namespace storm { // Keep track of the contained meta variables in the DD. if (this->containsMetaVariable(metaVariablePair.first)) { - newContainedMetaVariables.insert(metaVariablePair.second); - } - if (this->containsMetaVariable(metaVariablePair.second)) { - newContainedMetaVariables.insert(metaVariablePair.first); + if (this->containsMetaVariable(metaVariablePair.second)) { + // Nothing to do here. + } else { + newContainedMetaVariables.insert(metaVariablePair.second); + deletedMetaVariables.insert(metaVariablePair.first); + } + } else { + if (!this->containsMetaVariable(metaVariablePair.second)) { + // Nothing to do here. + } else { + newContainedMetaVariables.insert(metaVariablePair.first); + deletedMetaVariables.insert(metaVariablePair.second); + } } for (auto const& ddVariable : variable1.getDdVariables()) { @@ -274,7 +284,39 @@ namespace storm { to.push_back(ddVariable); } } - return Bdd(this->getDdManager(), internalBdd.swapVariables(from, to), newContainedMetaVariables); + + std::set tmp; + std::set_difference(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), deletedMetaVariables.begin(), deletedMetaVariables.end(), std::inserter(tmp, tmp.begin())); + std::set containedMetaVariables; + std::set_union(tmp.begin(), tmp.end(), newContainedMetaVariables.begin(), newContainedMetaVariables.end(), std::inserter(containedMetaVariables, containedMetaVariables.begin())); + return Bdd(this->getDdManager(), internalBdd.swapVariables(from, to), containedMetaVariables); + } + + template + Bdd Bdd::renameVariables(std::set const& from, std::set const& to) const { + std::vector> fromBdds; + std::vector> toBdds; + + for (auto const& metaVariable : from) { + STORM_LOG_THROW(this->containsMetaVariable(metaVariable), storm::exceptions::InvalidOperationException, "Cannot rename variable '" << metaVariable.getName() << "' that is not present."); + DdMetaVariable const& ddMetaVariable = this->getDdManager().getMetaVariable(metaVariable); + for (auto const& ddVariable : ddMetaVariable.getDdVariables()) { + fromBdds.push_back(ddVariable); + } + } + for (auto const& metaVariable : to) { + STORM_LOG_THROW(!this->containsMetaVariable(metaVariable), storm::exceptions::InvalidOperationException, "Cannot rename to variable '" << metaVariable.getName() << "' that is already present."); + DdMetaVariable const& ddMetaVariable = this->getDdManager().getMetaVariable(metaVariable); + for (auto const& ddVariable : ddMetaVariable.getDdVariables()) { + toBdds.push_back(ddVariable); + } + } + + std::set newContainedMetaVariables = to; + std::set_difference(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), from.begin(), from.end(), std::inserter(newContainedMetaVariables, newContainedMetaVariables.begin())); + + STORM_LOG_THROW(fromBdds.size() == toBdds.size(), storm::exceptions::InvalidArgumentException, "Unable to rename mismatching meta variables."); + return Bdd(this->getDdManager(), internalBdd.swapVariables(fromBdds, toBdds), newContainedMetaVariables); } template diff --git a/src/storm/storage/dd/Bdd.h b/src/storm/storage/dd/Bdd.h index 1250b2632..4a6ae2309 100644 --- a/src/storm/storage/dd/Bdd.h +++ b/src/storm/storage/dd/Bdd.h @@ -274,6 +274,17 @@ namespace storm { */ Bdd swapVariables(std::vector> const& metaVariablePairs) const; + /*! + * Renames the given meta variables in the BDD. The number of the underlying DD variables of the both meta + * variable sets needs to agree. + * + * @param from The meta variables to be renamed. The current BDD needs to contain all these meta variables. + * @param to The meta variables that are the target of the renaming process. The current BDD must not contain + * any of these meta variables. + * @return The resulting BDD. + */ + Bdd renameVariables(std::set const& from, std::set const& to) const; + /*! * Retrieves whether this DD represents the constant one function. * diff --git a/src/storm/storage/dd/BisimulationDecomposition.cpp b/src/storm/storage/dd/BisimulationDecomposition.cpp index 4893340a6..a1698404a 100644 --- a/src/storm/storage/dd/BisimulationDecomposition.cpp +++ b/src/storm/storage/dd/BisimulationDecomposition.cpp @@ -2,9 +2,11 @@ #include "storm/storage/dd/bisimulation/SignatureComputer.h" #include "storm/storage/dd/bisimulation/SignatureRefiner.h" +#include "storm/storage/dd/bisimulation/QuotientExtractor.h" #include "storm/utility/macros.h" #include "storm/exceptions/InvalidOperationException.h" +#include "storm/exceptions/NotSupportedException.h" #include @@ -16,15 +18,20 @@ namespace storm { using namespace bisimulation; template - BisimulationDecomposition::BisimulationDecomposition(storm::models::symbolic::Model const& model) : status(Status::Initialized), model(model), currentPartition(bisimulation::Partition::create(model)) { + BisimulationDecomposition::BisimulationDecomposition(storm::models::symbolic::Model const& model) : BisimulationDecomposition(model, bisimulation::Partition::create(model)) { // Intentionally left empty. } template - BisimulationDecomposition::BisimulationDecomposition(storm::models::symbolic::Model const& model, Partition const& initialPartition) : model(model), currentPartition(initialPartition) { + BisimulationDecomposition::BisimulationDecomposition(storm::models::symbolic::Model const& model, std::vector> const& formulas) : BisimulationDecomposition(model, bisimulation::Partition::create(model, formulas)) { // Intentionally left empty. } + template + BisimulationDecomposition::BisimulationDecomposition(storm::models::symbolic::Model const& model, Partition const& initialPartition) : model(model), currentPartition(initialPartition) { + STORM_LOG_THROW(!model.hasRewardModel(), storm::exceptions::NotSupportedException, "Symbolic bisimulation currently does not support preserving rewards."); + } + template void BisimulationDecomposition::compute() { this->status = Status::InComputation; @@ -52,7 +59,6 @@ namespace storm { auto refinementStart = std::chrono::high_resolution_clock::now(); Partition newPartition = refiner.refine(currentPartition, signature); -// newPartition.getPartitionAdd().exportToDot("part" + std::to_string(iterations) + ".dot"); auto refinementEnd = std::chrono::high_resolution_clock::now(); totalRefinementTime += (refinementEnd - refinementStart); @@ -78,7 +84,13 @@ namespace storm { template std::shared_ptr> BisimulationDecomposition::getQuotient() const { STORM_LOG_THROW(this->status == Status::FixedPoint, storm::exceptions::InvalidOperationException, "Cannot extract quotient, because bisimulation decomposition was not completed."); - return nullptr; + + STORM_LOG_TRACE("Starting quotient extraction."); + QuotientExtractor extractor; + std::shared_ptr> quotient = extractor.extract(model, currentPartition); + STORM_LOG_TRACE("Quotient extraction done."); + + return quotient; } template class BisimulationDecomposition; diff --git a/src/storm/storage/dd/BisimulationDecomposition.h b/src/storm/storage/dd/BisimulationDecomposition.h index 131a672e1..e0ec00d27 100644 --- a/src/storm/storage/dd/BisimulationDecomposition.h +++ b/src/storm/storage/dd/BisimulationDecomposition.h @@ -1,10 +1,15 @@ #pragma once +#include +#include + #include "storm/storage/dd/DdType.h" +#include "storm/storage/dd/bisimulation/Partition.h" + #include "storm/models/symbolic/Model.h" -#include "storm/storage/dd/bisimulation/Partition.h" +#include "storm/logic/Formula.h" namespace storm { namespace dd { @@ -17,7 +22,7 @@ namespace storm { }; BisimulationDecomposition(storm::models::symbolic::Model const& model); - + BisimulationDecomposition(storm::models::symbolic::Model const& model, std::vector> const& formulas); BisimulationDecomposition(storm::models::symbolic::Model const& model, bisimulation::Partition const& initialPartition); /*! diff --git a/src/storm/storage/dd/DdManager.cpp b/src/storm/storage/dd/DdManager.cpp index 65a46debf..2d89a82ae 100644 --- a/src/storm/storage/dd/DdManager.cpp +++ b/src/storm/storage/dd/DdManager.cpp @@ -21,6 +21,16 @@ namespace storm { // Intentionally left empty. } + template + std::shared_ptr> DdManager::asSharedPointer() { + return this->shared_from_this(); + } + + template + std::shared_ptr const> DdManager::asSharedPointer() const { + return this->shared_from_this(); + } + template Bdd DdManager::getBddOne() const { return Bdd(*this, internalDdManager.getBddOne()); @@ -221,6 +231,11 @@ namespace storm { return result; } + template + std::vector DdManager::addBitVectorMetaVariable(std::string const& variableName, uint64_t bits, uint64_t numberOfLayers, boost::optional> const& position) { + return this->addMetaVariable(variableName, 0, (1ull << bits) - 1, numberOfLayers, position); + } + template std::pair DdManager::addMetaVariable(std::string const& name, boost::optional> const& position) { std::vector result = addMetaVariable(name, 2, position); diff --git a/src/storm/storage/dd/DdManager.h b/src/storm/storage/dd/DdManager.h index cade43736..fdee32589 100644 --- a/src/storm/storage/dd/DdManager.h +++ b/src/storm/storage/dd/DdManager.h @@ -21,7 +21,7 @@ namespace storm { namespace dd { // Declare DdManager class so we can then specialize it for the different DD types. template - class DdManager { + class DdManager : public std::enable_shared_from_this> { public: friend class Bdd; @@ -41,6 +41,9 @@ namespace storm { DdManager& operator=(DdManager const& other) = delete; DdManager(DdManager&& other) = default; DdManager& operator=(DdManager&& other) = default; + + std::shared_ptr> asSharedPointer(); + std::shared_ptr const> asSharedPointer() const; /*! * Retrieves a BDD representing the constant one function. @@ -160,7 +163,15 @@ namespace storm { * @param numberOfLayers The number of layers of this variable (must be greater or equal 1). */ std::vector addMetaVariable(std::string const& variableName, int_fast64_t low, int_fast64_t high, uint64_t numberOfLayers, boost::optional> const& position = boost::none); - + + /*! + * Creates a meta variable with the given number of layers. + * + * @param variableName The name of the variable. + * @param numberOfLayers The number of layers of this variable (must be greater or equal 1). + */ + std::vector addBitVectorMetaVariable(std::string const& variableName, uint64_t bits, uint64_t numberOfLayers, boost::optional> const& position = boost::none); + /*! * Adds a boolean meta variable with two layers (a 'normal' and a 'primed' one). * diff --git a/src/storm/storage/dd/bisimulation/Partition.cpp b/src/storm/storage/dd/bisimulation/Partition.cpp index 994db80c7..6e71074eb 100644 --- a/src/storm/storage/dd/bisimulation/Partition.cpp +++ b/src/storm/storage/dd/bisimulation/Partition.cpp @@ -2,33 +2,42 @@ #include "storm/storage/dd/DdManager.h" +#include "storm/storage/dd/bisimulation/PreservationInformation.h" + +#include "storm/logic/Formula.h" +#include "storm/logic/AtomicExpressionFormula.h" +#include "storm/logic/AtomicLabelFormula.h" + +#include "storm/utility/macros.h" +#include "storm/exceptions/InvalidPropertyException.h" + namespace storm { namespace dd { namespace bisimulation { template - Partition::Partition(storm::dd::Add const& partitionAdd, storm::expressions::Variable const& blockVariable, uint64_t nextFreeBlockIndex) : partition(partitionAdd), blockVariable(blockVariable), nextFreeBlockIndex(nextFreeBlockIndex) { + Partition::Partition(std::shared_ptr preservationInformation, storm::dd::Add const& partitionAdd, std::pair const& blockVariables, uint64_t nextFreeBlockIndex) : preservationInformation(preservationInformation), partition(partitionAdd), blockVariables(blockVariables), nextFreeBlockIndex(nextFreeBlockIndex) { // Intentionally left empty. } template - Partition::Partition(storm::dd::Bdd const& partitionBdd, storm::expressions::Variable const& blockVariable, uint64_t nextFreeBlockIndex) : partition(partitionBdd), blockVariable(blockVariable), nextFreeBlockIndex(nextFreeBlockIndex) { + Partition::Partition(std::shared_ptr preservationInformation, storm::dd::Bdd const& partitionBdd, std::pair const& blockVariables, uint64_t nextFreeBlockIndex) : preservationInformation(preservationInformation), partition(partitionBdd), blockVariables(blockVariables), nextFreeBlockIndex(nextFreeBlockIndex) { // Intentionally left empty. } template bool Partition::operator==(Partition const& other) { - return this->partition == other.partition && this->blockVariable == other.blockVariable && this->nextFreeBlockIndex == other.nextFreeBlockIndex; + return this->partition == other.partition && this->blockVariables == other.blockVariables && this->nextFreeBlockIndex == other.nextFreeBlockIndex; } template Partition Partition::replacePartition(storm::dd::Add const& newPartitionAdd, uint64_t nextFreeBlockIndex) const { - return Partition(newPartitionAdd, blockVariable, nextFreeBlockIndex); + return Partition(preservationInformation, newPartitionAdd, blockVariables, nextFreeBlockIndex); } template Partition Partition::replacePartition(storm::dd::Bdd const& newPartitionBdd, uint64_t nextFreeBlockIndex) const { - return Partition(newPartitionBdd, blockVariable, nextFreeBlockIndex); + return Partition(preservationInformation, newPartitionBdd, blockVariables, nextFreeBlockIndex); } template @@ -38,15 +47,57 @@ namespace storm { template Partition Partition::create(storm::models::symbolic::Model const& model, std::vector const& labels) { + std::shared_ptr preservationInformation = std::make_shared(); std::vector expressions; for (auto const& label : labels) { + preservationInformation->addLabel(label); expressions.push_back(model.getExpression(label)); } - return create(model, expressions); + return create(model, expressions, preservationInformation); } template Partition Partition::create(storm::models::symbolic::Model const& model, std::vector const& expressions) { + std::shared_ptr preservationInformation = std::make_shared(); + for (auto const& expression : expressions) { + preservationInformation->addExpression(expression); + } + return create(model, expressions, preservationInformation); + } + + template + Partition Partition::create(storm::models::symbolic::Model const& model, std::vector> const& formulas) { + if (formulas.empty()) { + return create(model); + } + + std::shared_ptr preservationInformation = std::make_shared(); + std::set labels; + std::set expressions; + + for (auto const& formula : formulas) { + for (auto const& expressionFormula : formula->getAtomicExpressionFormulas()) { + expressions.insert(expressionFormula->getExpression()); + preservationInformation->addExpression(expressionFormula->getExpression()); + } + for (auto const& labelFormula : formula->getAtomicLabelFormulas()) { + std::string const& label = labelFormula->getLabel(); + STORM_LOG_THROW(model.hasLabel(label), storm::exceptions::InvalidPropertyException, "Property refers to illegal label '" << label << "'."); + preservationInformation->addLabel(label); + expressions.insert(model.getExpression(label)); + } + } + + std::vector expressionVector; + for (auto const& expression : expressions) { + expressionVector.emplace_back(expression); + } + + return create(model, expressionVector, preservationInformation); + } + + template + Partition Partition::create(storm::models::symbolic::Model const& model, std::vector const& expressions, std::shared_ptr const& preservationInformation) { storm::dd::DdManager& manager = model.getManager(); std::vector> stateSets; @@ -54,14 +105,20 @@ namespace storm { stateSets.emplace_back(model.getStates(expression)); } - storm::expressions::Variable blockVariable = createBlockVariable(manager, model.getReachableStates().getNonZeroCount()); - std::pair, uint64_t> partitionBddAndBlockCount = createPartitionBdd(manager, model, stateSets, blockVariable); + uint64_t numberOfDdVariables = 0; + for (auto const& metaVariable : model.getRowVariables()) { + auto const& ddMetaVariable = manager.getMetaVariable(metaVariable); + numberOfDdVariables += ddMetaVariable.getNumberOfDdVariables(); + } + + std::pair blockVariables = createBlockVariables(manager, numberOfDdVariables); + std::pair, uint64_t> partitionBddAndBlockCount = createPartitionBdd(manager, model, stateSets, blockVariables.first); // Store the partition as an ADD only in the case of CUDD. if (DdType == storm::dd::DdType::CUDD) { - return Partition(partitionBddAndBlockCount.first.template toAdd(), blockVariable, partitionBddAndBlockCount.second); + return Partition(preservationInformation, partitionBddAndBlockCount.first.template toAdd(), blockVariables, partitionBddAndBlockCount.second); } else { - return Partition(partitionBddAndBlockCount.first, blockVariable, partitionBddAndBlockCount.second); + return Partition(preservationInformation, partitionBddAndBlockCount.first, blockVariables, partitionBddAndBlockCount.second); } } @@ -92,7 +149,12 @@ namespace storm { template storm::expressions::Variable const& Partition::getBlockVariable() const { - return blockVariable; + return blockVariables.first; + } + + template + storm::expressions::Variable const& Partition::getPrimedBlockVariable() const { + return blockVariables.second; } template @@ -109,6 +171,11 @@ namespace storm { } } + template + PreservationInformation const& Partition::getPreservationInformation() const { + return *preservationInformation; + } + template void enumerateBlocksRec(std::vector> const& stateSets, storm::dd::Bdd const& currentStateSet, uint64_t offset, storm::expressions::Variable const& blockVariable, std::function const&)> const& callback) { if (currentStateSet.isZero()) { @@ -125,34 +192,33 @@ namespace storm { template std::pair, uint64_t> Partition::createPartitionBdd(storm::dd::DdManager const& manager, storm::models::symbolic::Model const& model, std::vector> const& stateSets, storm::expressions::Variable const& blockVariable) { uint64_t blockCount = 0; - storm::dd::Bdd partitionAdd = manager.getBddZero(); + storm::dd::Bdd partitionBdd = manager.getBddZero(); // Enumerate all realizable blocks. - enumerateBlocksRec(stateSets, model.getReachableStates(), 0, blockVariable, [&manager, &partitionAdd, &blockVariable, &blockCount](storm::dd::Bdd const& stateSet) { - stateSet.template toAdd().exportToDot("states_" + std::to_string(blockCount) + ".dot"); - partitionAdd |= (stateSet && manager.getEncoding(blockVariable, blockCount, false)); + enumerateBlocksRec(stateSets, model.getReachableStates(), 0, blockVariable, [&manager, &partitionBdd, &blockVariable, &blockCount](storm::dd::Bdd const& stateSet) { + partitionBdd |= (stateSet && manager.getEncoding(blockVariable, blockCount, false)); blockCount++; } ); - + // Move the partition over to the primed variables. - partitionAdd = partitionAdd.swapVariables(model.getRowColumnMetaVariablePairs()); - - return std::make_pair(partitionAdd, blockCount); + partitionBdd = partitionBdd.swapVariables(model.getRowColumnMetaVariablePairs()); + + return std::make_pair(partitionBdd, blockCount); } template - storm::expressions::Variable Partition::createBlockVariable(storm::dd::DdManager& manager, uint64_t numberOfStates) { - storm::expressions::Variable blockVariable; + std::pair Partition::createBlockVariables(storm::dd::DdManager& manager, uint64_t numberOfDdVariables) { + std::vector blockVariables; if (manager.hasMetaVariable("blocks")) { int64_t counter = 0; while (manager.hasMetaVariable("block" + std::to_string(counter))) { ++counter; } - blockVariable = manager.addMetaVariable("blocks" + std::to_string(counter), 0, numberOfStates, 1).front(); + blockVariables = manager.addBitVectorMetaVariable("blocks" + std::to_string(counter), numberOfDdVariables, 2); } else { - blockVariable = manager.addMetaVariable("blocks", 0, numberOfStates, 1).front(); + blockVariables = manager.addBitVectorMetaVariable("blocks", numberOfDdVariables, 2); } - return blockVariable; + return std::make_pair(blockVariables[0], blockVariables[1]); } template class Partition; diff --git a/src/storm/storage/dd/bisimulation/Partition.h b/src/storm/storage/dd/bisimulation/Partition.h index a206c33a5..f52c827cb 100644 --- a/src/storm/storage/dd/bisimulation/Partition.h +++ b/src/storm/storage/dd/bisimulation/Partition.h @@ -1,5 +1,8 @@ #pragma once +#include +#include + #include #include "storm/storage/dd/DdType.h" @@ -9,38 +12,20 @@ #include "storm/models/symbolic/Model.h" namespace storm { + namespace logic { + class Formula; + } + namespace dd { namespace bisimulation { + class PreservationInformation; + template class Partition { public: Partition() = default; - /*! - * Creates a new partition from the given data. - * - * @param partitionAdd An ADD that maps encoding over the state/row variables and the block variable to - * one iff the state is in the block. - * @param blockVariable The variable to use for the block encoding. Its range must be [0, x] where x is - * the number of states in the partition. - * @param nextFreeBlockIndex The next free block index. The existing blocks must be encoded with indices - * between 0 and this number. - */ - Partition(storm::dd::Add const& partitionAdd, storm::expressions::Variable const& blockVariable, uint64_t nextFreeBlockIndex); - - /*! - * Creates a new partition from the given data. - * - * @param partitionBdd A BDD that maps encoding over the state/row variables and the block variable to - * true iff the state is in the block. - * @param blockVariable The variable to use for the block encoding. Its range must be [0, x] where x is - * the number of states in the partition. - * @param nextFreeBlockIndex The next free block index. The existing blocks must be encoded with indices - * between 0 and this number. - */ - Partition(storm::dd::Bdd const& partitionBdd, storm::expressions::Variable const& blockVariable, uint64_t nextFreeBlockIndex); - bool operator==(Partition const& other); Partition replacePartition(storm::dd::Add const& newPartitionAdd, uint64_t nextFreeBlockIndex) const; @@ -62,6 +47,11 @@ namespace storm { */ static Partition create(storm::models::symbolic::Model const& model, std::vector const& expressions); + /*! + * Creates a partition from the given model that preserves the given formulas. + */ + static Partition create(storm::models::symbolic::Model const& model, std::vector> const& formulas); + uint64_t getNumberOfBlocks() const; bool storedAsAdd() const; @@ -71,21 +61,56 @@ namespace storm { storm::dd::Bdd const& asBdd() const; storm::expressions::Variable const& getBlockVariable() const; + storm::expressions::Variable const& getPrimedBlockVariable() const; uint64_t getNextFreeBlockIndex() const; - uint64_t getNodeCount() const; + + PreservationInformation const& getPreservationInformation() const; private: + /*! + * Creates a new partition from the given data. + * + * @param preservationInformation Informatin about which labels/expressions this partition preserves. + * @param partitionAdd An ADD that maps encoding over the state/row variables and the block variable to + * one iff the state is in the block. + * @param blockVariables The variables to use for the block encoding. Its range must be [0, x] where x is + * greater or equal than the number of states in the partition. + * @param nextFreeBlockIndex The next free block index. The existing blocks must be encoded with indices + * between 0 and this number. + */ + Partition(std::shared_ptr preservationInformation, storm::dd::Add const& partitionAdd, std::pair const& blockVariables, uint64_t nextFreeBlockIndex); + + /*! + * Creates a new partition from the given data. + * + * @param preservationInformation Informatin about which labels/expressions this partition preserves. + * @param partitionBdd A BDD that maps encoding over the state/row variables and the block variable to + * true iff the state is in the block. + * @param blockVariables The variables to use for the block encoding. Their range must be [0, x] where x is + * greater or equal than the number of states in the partition. + * @param nextFreeBlockIndex The next free block index. The existing blocks must be encoded with indices + * between 0 and this number. + */ + Partition(std::shared_ptr preservationInformation, storm::dd::Bdd const& partitionBdd, std::pair const& blockVariables, uint64_t nextFreeBlockIndex); + + /*! + * Creates a partition from the given model that respects the given expressions. + */ + static Partition create(storm::models::symbolic::Model const& model, std::vector const& expressions, std::shared_ptr const& preservationInformation); + static std::pair, uint64_t> createPartitionBdd(storm::dd::DdManager const& manager, storm::models::symbolic::Model const& model, std::vector> const& stateSets, storm::expressions::Variable const& blockVariable); - static storm::expressions::Variable createBlockVariable(storm::dd::DdManager& manager, uint64_t numberOfStates); + static std::pair createBlockVariables(storm::dd::DdManager& manager, uint64_t numberOfDdVariables); + + std::shared_ptr preservationInformation; /// The DD representing the partition. The DD is over the row variables of the model and the block variable. boost::variant, storm::dd::Add> partition; - /// The meta variable used to encode the block of each state in this partition. - storm::expressions::Variable blockVariable; + /// The meta variables used to encode the block of each state in this partition. + std::pair blockVariables; /// The next free block index. uint64_t nextFreeBlockIndex; diff --git a/src/storm/storage/dd/bisimulation/PreservationInformation.cpp b/src/storm/storage/dd/bisimulation/PreservationInformation.cpp new file mode 100644 index 000000000..f6d25ff4d --- /dev/null +++ b/src/storm/storage/dd/bisimulation/PreservationInformation.cpp @@ -0,0 +1,24 @@ +#include "storm/storage/dd/bisimulation/PreservationInformation.h" + +namespace storm { + namespace dd { + namespace bisimulation { + + void PreservationInformation::addLabel(std::string const& label) { + labels.insert(label); + } + + void PreservationInformation::addExpression(storm::expressions::Expression const& expression) { + expressions.insert(expression); + } + + std::set const& PreservationInformation::getLabels() const { + return labels; + } + + std::set const& PreservationInformation::getExpressions() const { + return expressions; + } + } + } +} diff --git a/src/storm/storage/dd/bisimulation/PreservationInformation.h b/src/storm/storage/dd/bisimulation/PreservationInformation.h new file mode 100644 index 000000000..e936d3b0d --- /dev/null +++ b/src/storm/storage/dd/bisimulation/PreservationInformation.h @@ -0,0 +1,30 @@ +#pragma once + +#include +#include + +#include "storm/storage/expressions/Expression.h" + +namespace storm { + namespace dd { + namespace bisimulation { + + class PreservationInformation { + public: + + PreservationInformation() = default; + + void addLabel(std::string const& label); + void addExpression(storm::expressions::Expression const& expression); + + std::set const& getLabels() const; + std::set const& getExpressions() const; + + private: + std::set labels; + std::set expressions; + }; + + } + } +} diff --git a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp new file mode 100644 index 000000000..bef5d3fc3 --- /dev/null +++ b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp @@ -0,0 +1,161 @@ +#include "storm/storage/dd/bisimulation/QuotientExtractor.h" + +#include "storm/storage/dd/DdManager.h" + +#include "storm/models/symbolic/Dtmc.h" +#include "storm/models/symbolic/Ctmc.h" +#include "storm/models/symbolic/StandardRewardModel.h" + +#include "storm/storage/dd/bisimulation/PreservationInformation.h" + +#include "storm/settings/SettingsManager.h" + +#include "storm/utility/macros.h" +#include "storm/exceptions/NotSupportedException.h" + +namespace storm { + namespace dd { + namespace bisimulation { + + template + QuotientExtractor::QuotientExtractor() : useRepresentatives(false) { + auto const& settings = storm::settings::getModule(); + this->useRepresentatives = settings.isUseRepresentativesSet(); + this->quotientFormat = settings.getQuotientFormat(); + } + + template + std::shared_ptr> QuotientExtractor::extract(storm::models::symbolic::Model const& model, Partition const& partition) { + auto start = std::chrono::high_resolution_clock::now(); + std::shared_ptr> result; + if (quotientFormat == storm::settings::modules::BisimulationSettings::QuotientFormat::Sparse) { + result = extractSparseQuotient(model, partition); + } else { + result = extractDdQuotient(model, partition); + } + auto end = std::chrono::high_resolution_clock::now(); + STORM_LOG_TRACE("Quotient extraction completed in " << std::chrono::duration_cast(end - start).count() << "ms."); + return result; + } + + template + std::shared_ptr> QuotientExtractor::extractSparseQuotient(storm::models::symbolic::Model const& model, Partition const& partition) { + return nullptr; + } + + template + std::shared_ptr> QuotientExtractor::extractDdQuotient(storm::models::symbolic::Model const& model, Partition const& partition) { + return extractQuotientUsingBlockVariables(model, partition); + } + + template + std::shared_ptr> QuotientExtractor::extractQuotientUsingBlockVariables(storm::models::symbolic::Model const& model, Partition const& partition) { + auto modelType = model.getType(); + + if (modelType == storm::models::ModelType::Dtmc || modelType == storm::models::ModelType::Ctmc) { + std::set blockVariableSet = {partition.getBlockVariable()}; + std::set blockPrimeVariableSet = {partition.getPrimedBlockVariable()}; + std::vector> blockMetaVariablePairs = {std::make_pair(partition.getBlockVariable(), partition.getPrimedBlockVariable())}; + + storm::dd::Bdd partitionAsBdd = partition.storedAsBdd() ? partition.asBdd() : partition.asAdd().notZero(); + if (useRepresentatives) { + storm::dd::Bdd partitionAsBddOverPrimedBlockVariable = partitionAsBdd.renameVariables(blockVariableSet, blockPrimeVariableSet); + storm::dd::Bdd representativePartition = partitionAsBddOverPrimedBlockVariable.existsAbstractRepresentative(model.getColumnVariables()).renameVariables(model.getColumnVariables(), blockVariableSet); + partitionAsBdd = (representativePartition && partitionAsBddOverPrimedBlockVariable).existsAbstract(blockPrimeVariableSet); + } + + storm::dd::Add partitionAsAdd = partitionAsBdd.template toAdd(); + storm::dd::Add quotientTransitionMatrix = model.getTransitionMatrix().multiplyMatrix(partitionAsAdd.renameVariables(blockVariableSet, blockPrimeVariableSet), model.getColumnVariables()); + quotientTransitionMatrix = quotientTransitionMatrix.multiplyMatrix(partitionAsAdd.renameVariables(model.getColumnVariables(), model.getRowVariables()), model.getRowVariables()); + storm::dd::Bdd quotientTransitionMatrixBdd = quotientTransitionMatrix.notZero(); + + storm::dd::Bdd partitionAsBddOverRowVariables = partitionAsBdd.renameVariables(model.getColumnVariables(), model.getRowVariables()); + storm::dd::Bdd reachableStates = partitionAsBdd.existsAbstract(model.getColumnVariables()); + storm::dd::Bdd initialStates = (model.getInitialStates() && partitionAsBddOverRowVariables).existsAbstract(model.getRowVariables()); + storm::dd::Bdd deadlockStates = !quotientTransitionMatrixBdd.existsAbstract(blockPrimeVariableSet) && reachableStates; + + std::map> preservedLabelBdds; + for (auto const& label : partition.getPreservationInformation().getLabels()) { + preservedLabelBdds.emplace(label, (model.getStates(label) && partitionAsBddOverRowVariables).existsAbstract(model.getRowVariables())); + } + for (auto const& expression : partition.getPreservationInformation().getExpressions()) { + std::stringstream stream; + stream << expression; + std::string expressionAsString = stream.str(); + + auto it = preservedLabelBdds.find(expressionAsString); + if (it != preservedLabelBdds.end()) { + STORM_LOG_WARN("Duplicate label '" << expressionAsString << "', dropping second label definition."); + } else { + preservedLabelBdds.emplace(stream.str(), (model.getStates(expression) && partitionAsBddOverRowVariables).existsAbstract(model.getRowVariables())); + } + } + + if (modelType == storm::models::ModelType::Dtmc) { + return std::shared_ptr>(new storm::models::symbolic::Dtmc(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, preservedLabelBdds, {})); + } else { + return std::shared_ptr>(new storm::models::symbolic::Ctmc(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, preservedLabelBdds, {})); + } + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Cannot exctract quotient for this model type."); + } + } + + template + std::shared_ptr> QuotientExtractor::extractQuotientUsingOriginalVariables(storm::models::symbolic::Model const& model, Partition const& partition) { + auto modelType = model.getType(); + + if (modelType == storm::models::ModelType::Dtmc || modelType == storm::models::ModelType::Ctmc) { + std::set blockVariableSet = {partition.getBlockVariable()}; + std::set blockPrimeVariableSet = {partition.getPrimedBlockVariable()}; + std::vector> blockMetaVariablePairs = {std::make_pair(partition.getBlockVariable(), partition.getPrimedBlockVariable())}; + + storm::dd::Add partitionAsAdd = partition.storedAsBdd() ? partition.asBdd().template toAdd() : partition.asAdd(); + storm::dd::Add quotientTransitionMatrix = model.getTransitionMatrix().multiplyMatrix(partitionAsAdd, model.getColumnVariables()); + quotientTransitionMatrix = quotientTransitionMatrix.renameVariables(blockVariableSet, model.getColumnVariables()); + quotientTransitionMatrix = quotientTransitionMatrix.multiplyMatrix(partitionAsAdd, model.getRowVariables()); + quotientTransitionMatrix = quotientTransitionMatrix.renameVariables(blockVariableSet, model.getRowVariables()); + storm::dd::Bdd quotientTransitionMatrixBdd = quotientTransitionMatrix.notZero(); + + storm::dd::Bdd partitionAsBdd = partition.storedAsBdd() ? partition.asBdd() : partition.asAdd().notZero(); + storm::dd::Bdd partitionAsBddOverRowVariables = partitionAsBdd.renameVariables(model.getColumnVariables(), model.getRowVariables()); + storm::dd::Bdd reachableStates = partitionAsBdd.existsAbstract(model.getColumnVariables()).renameVariables(blockVariableSet, model.getRowVariables()); + storm::dd::Bdd initialStates = (model.getInitialStates() && partitionAsBdd.renameVariables(model.getColumnVariables(), model.getRowVariables())).existsAbstract(model.getRowVariables()).renameVariables(blockVariableSet, model.getRowVariables()); + storm::dd::Bdd deadlockStates = !quotientTransitionMatrixBdd.existsAbstract(model.getColumnVariables()) && reachableStates; + + std::map> preservedLabelBdds; + for (auto const& label : partition.getPreservationInformation().getLabels()) { + preservedLabelBdds.emplace(label, (model.getStates(label) && partitionAsBddOverRowVariables).existsAbstract(model.getRowVariables())); + } + for (auto const& expression : partition.getPreservationInformation().getExpressions()) { + std::stringstream stream; + stream << expression; + std::string expressionAsString = stream.str(); + + auto it = preservedLabelBdds.find(expressionAsString); + if (it != preservedLabelBdds.end()) { + STORM_LOG_WARN("Duplicate label '" << expressionAsString << "', dropping second label definition."); + } else { + preservedLabelBdds.emplace(stream.str(), (model.getStates(expression) && partitionAsBddOverRowVariables).existsAbstract(model.getRowVariables())); + } + } + + if (modelType == storm::models::ModelType::Dtmc) { + return std::shared_ptr>(new storm::models::symbolic::Dtmc(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs(), preservedLabelBdds, {})); + } else { + return std::shared_ptr>(new storm::models::symbolic::Ctmc(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, preservedLabelBdds, {})); + } + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Cannot exctract quotient for this model type."); + } + } + + template class QuotientExtractor; + + template class QuotientExtractor; + template class QuotientExtractor; + template class QuotientExtractor; + + } + } +} diff --git a/src/storm/storage/dd/bisimulation/QuotientExtractor.h b/src/storm/storage/dd/bisimulation/QuotientExtractor.h new file mode 100644 index 000000000..eb6cbef4b --- /dev/null +++ b/src/storm/storage/dd/bisimulation/QuotientExtractor.h @@ -0,0 +1,37 @@ +#pragma once + +#include + +#include "storm/storage/dd/DdType.h" + +#include "storm/models/symbolic/Model.h" + +#include "storm/storage/dd/bisimulation/Partition.h" + +#include "storm/settings/modules/BisimulationSettings.h" + +namespace storm { + namespace dd { + namespace bisimulation { + + template + class QuotientExtractor { + public: + QuotientExtractor(); + + std::shared_ptr> extract(storm::models::symbolic::Model const& model, Partition const& partition); + + private: + std::shared_ptr> extractSparseQuotient(storm::models::symbolic::Model const& model, Partition const& partition); + + std::shared_ptr> extractDdQuotient(storm::models::symbolic::Model const& model, Partition const& partition); + std::shared_ptr> extractQuotientUsingBlockVariables(storm::models::symbolic::Model const& model, Partition const& partition); + std::shared_ptr> extractQuotientUsingOriginalVariables(storm::models::symbolic::Model const& model, Partition const& partition); + + bool useRepresentatives; + storm::settings::modules::BisimulationSettings::QuotientFormat quotientFormat; + }; + + } + } +} diff --git a/src/storm/utility/storm.h b/src/storm/utility/storm.h index 9dc2d1a60..a913917be 100644 --- a/src/storm/utility/storm.h +++ b/src/storm/utility/storm.h @@ -192,10 +192,9 @@ namespace storm { } if (storm::settings::getModule().isBisimulationSet()) { - storm::dd::BisimulationDecomposition decomposition(*result); + storm::dd::BisimulationDecomposition decomposition(*result, formulas); decomposition.compute(); - - // TODO build quotient and return it. + result = decomposition.getQuotient(); } return result;