From 11d2ee2fdab3136a049037b4ba8445599d3a7685 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 23 Aug 2017 09:18:05 +0200 Subject: [PATCH] making sure to add meta variables to transition matrix DD to make sure one can abstract from them later --- src/storm/builder/DdPrismModelBuilder.cpp | 23 +++++++++++++------ src/storm/builder/DdPrismModelBuilder.h | 8 ++++++- src/storm/storage/dd/Dd.cpp | 2 +- .../dd/bisimulation/QuotientExtractor.cpp | 2 +- 4 files changed, 25 insertions(+), 10 deletions(-) diff --git a/src/storm/builder/DdPrismModelBuilder.cpp b/src/storm/builder/DdPrismModelBuilder.cpp index 23f856c58..eea14d863 100644 --- a/src/storm/builder/DdPrismModelBuilder.cpp +++ b/src/storm/builder/DdPrismModelBuilder.cpp @@ -1057,10 +1057,21 @@ namespace storm { } template - storm::dd::Add DdPrismModelBuilder::createSystemFromModule(GenerationInformation& generationInfo, ModuleDecisionDiagram const& module) { + storm::dd::Add DdPrismModelBuilder::createSystemFromModule(GenerationInformation& generationInfo, ModuleDecisionDiagram& module) { + storm::dd::Add result; + + // Make sure all actions contain all necessary meta variables. + module.independentAction.ensureContainsVariables(generationInfo.rowMetaVariables, generationInfo.columnMetaVariables); + for (auto& synchronizingAction : module.synchronizingActionToDecisionDiagramMap) { + synchronizingAction.second.ensureContainsVariables(generationInfo.rowMetaVariables, generationInfo.columnMetaVariables); + } + + + + // If the model is an MDP, we need to encode the nondeterminism using additional variables. if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) { - storm::dd::Add result = generationInfo.manager->template getAddZero(); + result = generationInfo.manager->template getAddZero(); // First, determine the highest number of nondeterminism variables that is used in any action and make // all actions use the same amout of nondeterminism variables. @@ -1080,6 +1091,7 @@ namespace storm { for (uint_fast64_t i = module.independentAction.numberOfUsedNondeterminismVariables; i < numberOfUsedNondeterminismVariables; ++i) { nondeterminismEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0).template toAdd(); } + result = identityEncoding * module.independentAction.transitionsDd * nondeterminismEncoding; // Add variables to synchronized action DDs. @@ -1112,8 +1124,6 @@ namespace storm { for (auto const& synchronizingAction : synchronizingActionToDdMap) { result += synchronizingAction.second; } - - return result; } else if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC || generationInfo.program.getModelType() == storm::prism::Program::ModelType::CTMC) { // Simply add all actions, but make sure to include the missing global variable identities. @@ -1126,8 +1136,7 @@ namespace storm { identityEncoding *= generationInfo.variableToIdentityMap.at(variable); } - storm::dd::Add result = identityEncoding * module.independentAction.transitionsDd; - + result = identityEncoding * module.independentAction.transitionsDd; for (auto const& synchronizingAction : module.synchronizingActionToDecisionDiagramMap) { // Compute missing global variable identities in synchronizing actions. missingIdentities = std::set(); @@ -1140,10 +1149,10 @@ namespace storm { result += identityEncoding * synchronizingAction.second.transitionsDd; } - return result; } else { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Illegal model type."); } + return result; } template diff --git a/src/storm/builder/DdPrismModelBuilder.h b/src/storm/builder/DdPrismModelBuilder.h index f3b7adc31..57d990b23 100644 --- a/src/storm/builder/DdPrismModelBuilder.h +++ b/src/storm/builder/DdPrismModelBuilder.h @@ -130,6 +130,12 @@ namespace storm { // Intentionally left empty. } + void ensureContainsVariables(std::set const& rowMetaVariables, std::set const& columnMetaVariables) { + guardDd.addMetaVariables(rowMetaVariables); + transitionsDd.addMetaVariables(rowMetaVariables); + transitionsDd.addMetaVariables(columnMetaVariables); + } + ActionDecisionDiagram(ActionDecisionDiagram const& other) = default; ActionDecisionDiagram& operator=(ActionDecisionDiagram const& other) = default; @@ -228,7 +234,7 @@ namespace storm { static storm::dd::Add getSynchronizationDecisionDiagram(GenerationInformation& generationInfo, uint_fast64_t actionIndex = 0); - static storm::dd::Add createSystemFromModule(GenerationInformation& generationInfo, ModuleDecisionDiagram const& module); + static storm::dd::Add createSystemFromModule(GenerationInformation& generationInfo, ModuleDecisionDiagram& module); static std::unordered_map> createRewardModelDecisionDiagrams(std::vector> const& selectedRewardModels, SystemResult& system, GenerationInformation& generationInfo, ModuleDecisionDiagram const& globalModule, storm::dd::Add const& reachableStatesAdd, storm::dd::Add const& transitionMatrix); diff --git a/src/storm/storage/dd/Dd.cpp b/src/storm/storage/dd/Dd.cpp index 52aaceac2..f0619c633 100644 --- a/src/storm/storage/dd/Dd.cpp +++ b/src/storm/storage/dd/Dd.cpp @@ -78,7 +78,7 @@ namespace storm { template std::set Dd::subtractMetaVariables(storm::dd::Dd const& first, storm::dd::Dd const& second) { bool includesAllMetaVariables = std::includes(first.getContainedMetaVariables().begin(), first.getContainedMetaVariables().end(), second.getContainedMetaVariables().begin(), second.getContainedMetaVariables().end()); - STORM_LOG_WARN_COND(includesAllMetaVariables, "Subtracting from meta variables that are not contained in the DD."); + STORM_LOG_THROW(includesAllMetaVariables, storm::exceptions::InvalidArgumentException, "Cannot subtract meta variables that are not contained in the DD."); std::set metaVariables; std::set_difference(first.getContainedMetaVariables().begin(), first.getContainedMetaVariables().end(), second.getContainedMetaVariables().begin(), second.getContainedMetaVariables().end(), std::inserter(metaVariables, metaVariables.begin())); return metaVariables; diff --git a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp index 63ba5d63a..0e6e310f5 100644 --- a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp +++ b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp @@ -896,7 +896,7 @@ namespace storm { quotientRewardModels.emplace(rewardModelName, storm::models::sparse::StandardRewardModel(std::move(quotientStateRewards), std::move(quotientStateActionRewards), boost::none)); } - start = std::chrono::high_resolution_clock::now(); + end = std::chrono::high_resolution_clock::now(); STORM_LOG_TRACE("Reward models extracted in " << std::chrono::duration_cast(end - start).count() << "ms."); std::shared_ptr> result;