From f7e2ff08437977187421d92dffbebce3490caea1 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Thu, 20 Feb 2020 12:02:32 +0100 Subject: [PATCH] Apply max. Prog. assumption while building with the dd engine. --- CHANGELOG.md | 1 + src/storm/api/builder.h | 11 ++--- src/storm/builder/DdJaniModelBuilder.cpp | 52 ++++++++++++++++++++--- src/storm/builder/DdJaniModelBuilder.h | 11 +++-- src/storm/builder/DdPrismModelBuilder.cpp | 2 +- 5 files changed, 61 insertions(+), 16 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index df9f29923..d9504338f 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -10,6 +10,7 @@ Version 1.4.x ## Version 1.4.2 (under development) - DRN: support import of choice labelling - Added option `--build:buildchoiceorig` to build a model (PRISM or JANI) with choice origins (which are exported with, e.g. `--exportscheduler`). +- Apply the maximum progress assumption while building a Markov automata with the Dd engine. - Added option `--build:nomaxprog` to disable applying the maximum progress assumption during model building (for Markov Automata) - `storm-pomdp`: Only accept POMDPs that are canonical - `storm-pomdp`: Prism language extended with observable expressions diff --git a/src/storm/api/builder.h b/src/storm/api/builder.h index 6be939496..4e22d6662 100644 --- a/src/storm/api/builder.h +++ b/src/storm/api/builder.h @@ -47,7 +47,6 @@ namespace storm { if (model.isPrismProgram()) { typename storm::builder::DdPrismModelBuilder::Options options; options = typename storm::builder::DdPrismModelBuilder::Options(formulas); - if (buildFullModel) { options.buildAllLabels = true; options.buildAllRewardModels = true; @@ -58,13 +57,15 @@ namespace storm { return builder.build(model.asPrismProgram(), options); } else { STORM_LOG_THROW(model.isJaniModel(), storm::exceptions::NotSupportedException, "Building symbolic model from this model description is unsupported."); - typename storm::builder::DdJaniModelBuilder::Options options; - options = typename storm::builder::DdJaniModelBuilder::Options(formulas); + typename storm::builder::DdJaniModelBuilder::Options options(formulas); if (buildFullModel) { options.buildAllLabels = true; options.buildAllRewardModels = true; + options.applyMaximumProgressAssumption = false; options.terminalStates.clear(); + } else { + options.applyMaximumProgressAssumption = (model.getModelType() == storm::storage::SymbolicModelDescription::ModelType::MA && applyMaximumProgress); } storm::builder::DdJaniModelBuilder builder; @@ -73,12 +74,12 @@ namespace storm { } template<> - inline std::shared_ptr> buildSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas, bool buildFullModel) { + inline std::shared_ptr> buildSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas, bool, bool) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "CUDD does not support rational numbers."); } template<> - inline std::shared_ptr> buildSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas, bool buildFullModel) { + inline std::shared_ptr> buildSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas, bool, bool) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "CUDD does not support rational functions."); } diff --git a/src/storm/builder/DdJaniModelBuilder.cpp b/src/storm/builder/DdJaniModelBuilder.cpp index ff52955ee..2175dd2e1 100644 --- a/src/storm/builder/DdJaniModelBuilder.cpp +++ b/src/storm/builder/DdJaniModelBuilder.cpp @@ -46,7 +46,7 @@ namespace storm { namespace builder { template - DdJaniModelBuilder::Options::Options(bool buildAllLabels, bool buildAllRewardModels) : buildAllLabels(buildAllLabels), buildAllRewardModels(buildAllRewardModels), rewardModelsToBuild(), constantDefinitions() { + DdJaniModelBuilder::Options::Options(bool buildAllLabels, bool buildAllRewardModels, bool applyMaximumProgressAssumption) : buildAllLabels(buildAllLabels), buildAllRewardModels(buildAllRewardModels), applyMaximumProgressAssumption(applyMaximumProgressAssumption), rewardModelsToBuild(), constantDefinitions() { // Intentionally left empty. } @@ -71,7 +71,7 @@ namespace storm { template void DdJaniModelBuilder::Options::preserveFormula(storm::logic::Formula const& formula) { // If we already had terminal states, we need to erase them. - terminalStates = storm::builder::TerminalStates(); + terminalStates.clear(); // If we are not required to build all reward models, we determine the reward models we need to build. if (!buildAllRewardModels) { @@ -662,6 +662,19 @@ namespace storm { return ActionDd(newGuard, newTransitions, newTransientEdgeAssignments, newLocalNondeterminismVariables, newVariableToWritingFragment, newIllegalFragment); } + /*! + * Conjuncts the guard of the action with the provided condition, i.e., this action is only enabled if the provided condition is true. + */ + void conjunctGuardWith(storm::dd::Bdd const& condition) { + guard &= condition; + storm::dd::Add conditionAdd = condition.template toAdd(); + transitions *= conditionAdd; + for (auto& t : transientEdgeAssignments) { + t.second *= conditionAdd; + } + illegalFragment &= condition; + } + bool isInputEnabled() const { return inputEnabled; } @@ -670,10 +683,10 @@ namespace storm { inputEnabled = true; } - // A DD that represents all states that have this edge enabled. + // A DD that represents all states that have this action enabled. storm::dd::Bdd guard; - // A DD that represents the transitions of this edge. + // A DD that represents the transitions of this action. storm::dd::Add transitions; // A mapping from transient variables to their assignments. @@ -787,11 +800,12 @@ namespace storm { std::pair localNondeterminismVariables; }; - CombinedEdgesSystemComposer(storm::jani::Model const& model, storm::jani::CompositionInformation const& actionInformation, CompositionVariables const& variables, std::vector const& transientVariables) : SystemComposer(model, variables, transientVariables), actionInformation(actionInformation) { + CombinedEdgesSystemComposer(storm::jani::Model const& model, storm::jani::CompositionInformation const& actionInformation, CompositionVariables const& variables, std::vector const& transientVariables, bool applyMaximumProgress) : SystemComposer(model, variables, transientVariables), actionInformation(actionInformation), applyMaximumProgress(applyMaximumProgress) { // Intentionally left empty. } storm::jani::CompositionInformation const& actionInformation; + bool applyMaximumProgress; ComposerResult compose() override { STORM_LOG_THROW(this->model.hasStandardCompliantComposition(), storm::exceptions::WrongFormatException, "Model builder only supports non-nested parallel compositions."); @@ -936,6 +950,9 @@ namespace storm { AutomatonDd composeInParallel(std::vector const& subautomata, std::vector const& synchronizationVectors) { AutomatonDd result(this->variables.manager->template getAddOne()); + // Disjunction of all guards of non-markovian actions (only required for maximum progress assumption. + storm::dd::Bdd nonMarkovianActionGuards = this->variables.manager->getBddZero(); + // Build the results of the synchronization vectors. std::unordered_map, ActionIdentificationHash> actions; for (uint64_t synchronizationVectorIndex = 0; synchronizationVectorIndex < synchronizationVectors.size(); ++synchronizationVectorIndex) { @@ -943,6 +960,11 @@ namespace storm { boost::optional synchronizingAction = combineSynchronizingActions(subautomata, synchVector, synchronizationVectorIndex); if (synchronizingAction) { + if (applyMaximumProgress) { + STORM_LOG_ASSERT(this->model.getModelType() == storm::jani::ModelType::MA, "Maximum progress assumption enabled for unexpected model type."); + // By the JANI standard, we can assume that synchronizing actions of MAs are always non-Markovian. + nonMarkovianActionGuards |= synchronizingAction->guard; + } actions[ActionIdentification(actionInformation.getActionIndex(synchVector.getOutput()), this->model.getModelType() == storm::jani::ModelType::CTMC)].emplace_back(synchronizingAction.get()); } } @@ -986,9 +1008,26 @@ namespace storm { auto& allSilentActionDds = actions[silentActionIdentification]; allSilentActionDds.insert(allSilentActionDds.end(), silentActionDds.begin(), silentActionDds.end()); } + + // Add guards of non-markovian actions + if (applyMaximumProgress) { + auto allSilentActionDdsIt = actions.find(silentActionIdentification); + if (allSilentActionDdsIt != actions.end()) { + for (ActionDd const& silentActionDd : allSilentActionDdsIt->second) { + nonMarkovianActionGuards |= silentActionDd.guard; + } + } + } + if (!silentMarkovianActionDds.empty()) { auto& allMarkovianSilentActionDds = actions[silentMarkovianActionIdentification]; allMarkovianSilentActionDds.insert(allMarkovianSilentActionDds.end(), silentMarkovianActionDds.begin(), silentMarkovianActionDds.end()); + if (applyMaximumProgress && !nonMarkovianActionGuards.isZero()) { + auto invertedNonMarkovianGuards = !nonMarkovianActionGuards; + for (ActionDd& markovianActionDd : allMarkovianSilentActionDds) { + markovianActionDd.conjunctGuardWith(invertedNonMarkovianGuards); + } + } } // Finally, combine (potentially) multiple action DDs. @@ -2062,7 +2101,8 @@ namespace storm { std::vector rewardVariables = selectRewardVariables(preparedModel, options); // Create a builder to compose and build the model. - CombinedEdgesSystemComposer composer(preparedModel, actionInformation, variables, rewardVariables); + bool applyMaximumProgress = options.applyMaximumProgressAssumption && model.getModelType() == storm::jani::ModelType::MA; + CombinedEdgesSystemComposer composer(preparedModel, actionInformation, variables, rewardVariables, applyMaximumProgress); ComposerResult system = composer.compose(); // Postprocess the variables in place. diff --git a/src/storm/builder/DdJaniModelBuilder.h b/src/storm/builder/DdJaniModelBuilder.h index 9dfe6f232..23684f4f9 100644 --- a/src/storm/builder/DdJaniModelBuilder.h +++ b/src/storm/builder/DdJaniModelBuilder.h @@ -28,7 +28,7 @@ namespace storm { /*! * Creates an object representing the default building options. */ - Options(bool buildAllLabels = false, bool buildAllRewardModels = false); + Options(bool buildAllLabels = false, bool buildAllRewardModels = false, bool applyMaximumProgressAssumption = true); /*! Creates an object representing the suggested building options assuming that the given formula is the * only one to check. Additional formulas may be preserved by calling preserveFormula. @@ -79,9 +79,6 @@ namespace storm { /// A flag that indicates whether all labels are to be built. In this case, the label names are to be ignored. bool buildAllLabels; - - /// A set of labels to build. - std::set labelNames; /*! * Retrieves whether the flag to build all reward models is set. @@ -91,6 +88,12 @@ namespace storm { // A flag that indicates whether or not all reward models are to be build. bool buildAllRewardModels; + /// A flag that indicates whether the maximum progress assumption should be applied. + bool applyMaximumProgressAssumption; + + /// A set of labels to build. + std::set labelNames; + // A list of reward models to be build in case not all reward models are to be build. std::set rewardModelsToBuild; diff --git a/src/storm/builder/DdPrismModelBuilder.cpp b/src/storm/builder/DdPrismModelBuilder.cpp index 0e5a05c9a..4633ebdbc 100644 --- a/src/storm/builder/DdPrismModelBuilder.cpp +++ b/src/storm/builder/DdPrismModelBuilder.cpp @@ -563,7 +563,7 @@ namespace storm { template void DdPrismModelBuilder::Options::preserveFormula(storm::logic::Formula const& formula) { // If we already had terminal states, we need to erase them. - terminalStates = storm::builder::TerminalStates(); + terminalStates.clear(); // If we are not required to build all reward models, we determine the reward models we need to build. if (!buildAllRewardModels) {