From 02977da3d7fb9437a745f5fb7fb6db6c3ddb9600 Mon Sep 17 00:00:00 2001 From: TimQu Date: Sat, 1 Dec 2018 23:03:30 +0100 Subject: [PATCH] Apply maximum progress assumption while building a Markov Automaton explicitly. --- src/storm-cli-utilities/model-handling.h | 5 ++- src/storm/builder/BuilderOptions.cpp | 17 ++++++-- src/storm/builder/BuilderOptions.h | 12 ++++++ .../generator/JaniNextStateGenerator.cpp | 26 +++++++++++- src/storm/generator/JaniNextStateGenerator.h | 4 +- .../generator/PrismNextStateGenerator.cpp | 42 +++++++++++++++---- src/storm/generator/PrismNextStateGenerator.h | 9 ++-- 7 files changed, 95 insertions(+), 20 deletions(-) diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index beba289d1..08b4a6e30 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -232,11 +232,12 @@ namespace storm { } else { options.setBuildChoiceOrigins(false); } - options.setBuildAllLabels(buildSettings.isBuildFullModelSet()); - options.setBuildAllRewardModels(buildSettings.isBuildFullModelSet()); options.setAddOutOfBoundsState(buildSettings.isBuildOutOfBoundsStateSet()); if (buildSettings.isBuildFullModelSet()) { options.clearTerminalStates(); + options.setApplyMaximalProgressAssumption(false); + options.setBuildAllLabels(true); + options.setBuildAllRewardModels(true); } return storm::api::buildSparseModel(input.model.get(), options, buildSettings.isJitSet(), storm::settings::getModule().isDoctorSet()); } diff --git a/src/storm/builder/BuilderOptions.cpp b/src/storm/builder/BuilderOptions.cpp index 50eb412e3..4110442d6 100644 --- a/src/storm/builder/BuilderOptions.cpp +++ b/src/storm/builder/BuilderOptions.cpp @@ -38,13 +38,12 @@ namespace storm { } - BuilderOptions::BuilderOptions(bool buildAllRewardModels, bool buildAllLabels) : buildAllRewardModels(buildAllRewardModels), buildAllLabels(buildAllLabels), buildChoiceLabels(false), buildStateValuations(false), buildChoiceOrigins(false), scaleAndLiftTransitionRewards(true), explorationChecks(false), inferObservationsFromActions(false), addOverlappingGuardsLabel(false), addOutOfBoundsState(false), reservedBitsForUnboundedVariables(32), showProgress(false), showProgressDelay(0) { + BuilderOptions::BuilderOptions(bool buildAllRewardModels, bool buildAllLabels) : buildAllRewardModels(buildAllRewardModels), buildAllLabels(buildAllLabels), applyMaximalProgressAssumption(false), buildChoiceLabels(false), buildStateValuations(false), buildChoiceOrigins(false), scaleAndLiftTransitionRewards(true), explorationChecks(false), inferObservationsFromActions(false), addOverlappingGuardsLabel(false), addOutOfBoundsState(false), reservedBitsForUnboundedVariables(32), showProgress(false), showProgressDelay(0) { // Intentionally left empty. } - BuilderOptions::BuilderOptions(storm::logic::Formula const& formula, storm::storage::SymbolicModelDescription const& modelDescription) : BuilderOptions() { - this->preserveFormula(formula, modelDescription); - this->setTerminalStatesFromFormula(formula); + BuilderOptions::BuilderOptions(storm::logic::Formula const& formula, storm::storage::SymbolicModelDescription const& modelDescription) : BuilderOptions({formula.asSharedPointer()}, modelDescription) { + // Intentionally left empty. } BuilderOptions::BuilderOptions(std::vector> const& formulas, storm::storage::SymbolicModelDescription const& modelDescription) : BuilderOptions() { @@ -59,6 +58,7 @@ namespace storm { auto const& buildSettings = storm::settings::getModule(); auto const& generalSettings = storm::settings::getModule(); + this->setApplyMaximalProgressAssumption(modelDescription.getModelType() == storm::storage::SymbolicModelDescription::ModelType::MA); explorationChecks = buildSettings.isExplorationChecksSet(); reservedBitsForUnboundedVariables = buildSettings.getBitsForUnboundedVariables(); showProgress = generalSettings.isVerboseSet(); @@ -145,6 +145,10 @@ namespace storm { terminalStates.clear(); } + bool BuilderOptions::isApplyMaximalProgressAssumptionSet() const { + return applyMaximalProgressAssumption; + } + bool BuilderOptions::isBuildChoiceLabelsSet() const { return buildChoiceLabels; } @@ -241,6 +245,11 @@ namespace storm { return *this; } + BuilderOptions& BuilderOptions::setApplyMaximalProgressAssumption(bool newValue) { + applyMaximalProgressAssumption = newValue; + return *this; + } + BuilderOptions& BuilderOptions::setBuildChoiceLabels(bool newValue) { buildChoiceLabels = newValue; return *this; diff --git a/src/storm/builder/BuilderOptions.h b/src/storm/builder/BuilderOptions.h index c23a053f9..a06817816 100644 --- a/src/storm/builder/BuilderOptions.h +++ b/src/storm/builder/BuilderOptions.h @@ -103,6 +103,7 @@ namespace storm { std::vector> const& getTerminalStates() const; bool hasTerminalStates() const; void clearTerminalStates(); + bool isApplyMaximalProgressAssumptionSet() const; bool isBuildChoiceLabelsSet() const; bool isBuildStateValuationsSet() const; bool isBuildChoiceOriginsSet() const; @@ -139,6 +140,13 @@ namespace storm { BuilderOptions& addLabel(std::string const& labelName); BuilderOptions& addTerminalExpression(storm::expressions::Expression const& expression, bool value); BuilderOptions& addTerminalLabel(std::string const& label, bool value); + /** + * Should the maximal progress assumption be applied when building a Markov Automaton? + * @param newValue If this is true, Markovian edges are not explored from probabilistic states + * @return this + */ + BuilderOptions& setApplyMaximalProgressAssumption(bool newValue = true); + /** * Should the choice labels be built? * @param newValue The new value (default true) @@ -218,6 +226,10 @@ namespace storm { /// If one of these labels/expressions evaluates to the given bool, the builder can abort the exploration. std::vector> terminalStates; + + /// A flag indicating whether the maximal progress assumption is applied when building a Markov Automaton. + /// If this is true, Markovian edges are not explored from probabilistic states. + bool applyMaximalProgressAssumption; /// A flag indicating whether or not to build choice labels. bool buildChoiceLabels; diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp index f5d10d703..7b12a4f96 100644 --- a/src/storm/generator/JaniNextStateGenerator.cpp +++ b/src/storm/generator/JaniNextStateGenerator.cpp @@ -457,7 +457,17 @@ namespace storm { // Get all choices for the state. result.setExpanded(); - std::vector> allChoices = getActionChoices(locations, *this->state, stateToIdCallback); + std::vector> allChoices; + if (this->getOptions().isApplyMaximalProgressAssumptionSet()) { + // First explore only edges without a rate + allChoices = getActionChoices(locations, *this->state, stateToIdCallback, EdgeFilter::WithoutRate); + if (allChoices.empty()) { + // Expand the Markovian edges if there are no probabilistic ones. + allChoices = getActionChoices(locations, *this->state, stateToIdCallback, EdgeFilter::WithRate); + } + } else { + allChoices = getActionChoices(locations, *this->state, stateToIdCallback); + } std::size_t totalNumberOfChoices = allChoices.size(); // If there is not a single choice, we return immediately, because the state has no behavior (other than @@ -800,7 +810,7 @@ namespace storm { } template - std::vector> JaniNextStateGenerator::getActionChoices(std::vector const& locations, CompressedState const& state, StateToIdCallback stateToIdCallback) { + std::vector> JaniNextStateGenerator::getActionChoices(std::vector const& locations, CompressedState const& state, StateToIdCallback stateToIdCallback, EdgeFilter const& edgeFilter) { std::vector> result; for (auto const& outputAndEdges : edges) { @@ -813,6 +823,12 @@ namespace storm { auto edgesIt = nonsychingEdges.second.find(locations[automatonIndex]); if (edgesIt != nonsychingEdges.second.end()) { for (auto const& indexAndEdge : edgesIt->second) { + if (edgeFilter != EdgeFilter::All) { + STORM_LOG_ASSERT(edgeFilter == EdgeFilter::WithRate || edgeFilter == EdgeFilter::WithoutRate, "Unexpected edge filter."); + if ((edgeFilter == EdgeFilter::WithRate) != indexAndEdge.second->hasRate()) { + continue; + } + } if (!this->evaluator->asBool(indexAndEdge.second->getGuard())) { continue; } @@ -842,6 +858,12 @@ namespace storm { auto edgesIt = automatonAndEdges.second.find(locations[automatonIndex]); if (edgesIt != automatonAndEdges.second.end()) { for (auto const& indexAndEdge : edgesIt->second) { + if (edgeFilter != EdgeFilter::All) { + STORM_LOG_ASSERT(edgeFilter == EdgeFilter::WithRate || edgeFilter == EdgeFilter::WithoutRate, "Unexpected edge filter."); + if ((edgeFilter == EdgeFilter::WithRate) != indexAndEdge.second->hasRate()) { + continue; + } + } if (!this->evaluator->asBool(indexAndEdge.second->getGuard())) { continue; } diff --git a/src/storm/generator/JaniNextStateGenerator.h b/src/storm/generator/JaniNextStateGenerator.h index 62241dde1..350429944 100644 --- a/src/storm/generator/JaniNextStateGenerator.h +++ b/src/storm/generator/JaniNextStateGenerator.h @@ -29,6 +29,7 @@ namespace storm { public: typedef typename NextStateGenerator::StateToIdCallback StateToIdCallback; typedef boost::container::flat_set EdgeIndexSet; + enum class EdgeFilter {All, WithRate, WithoutRate}; JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options = NextStateGeneratorOptions()); @@ -97,9 +98,10 @@ namespace storm { * * @param locations The current locations of all automata. * @param state The state for which to retrieve the silent choices. + * @param edgeFilter Restricts the kind of edges to be considered. * @return The action choices of the state. */ - std::vector> getActionChoices(std::vector const& locations, CompressedState const& state, StateToIdCallback stateToIdCallback); + std::vector> getActionChoices(std::vector const& locations, CompressedState const& state, StateToIdCallback stateToIdCallback, EdgeFilter const& edgeFilter = EdgeFilter::All); /*! * Retrieves the choice generated by the given edge. diff --git a/src/storm/generator/PrismNextStateGenerator.cpp b/src/storm/generator/PrismNextStateGenerator.cpp index 627aa2d7f..8a7030b17 100644 --- a/src/storm/generator/PrismNextStateGenerator.cpp +++ b/src/storm/generator/PrismNextStateGenerator.cpp @@ -279,11 +279,26 @@ namespace storm { // Get all choices for the state. result.setExpanded(); - std::vector> allChoices = getUnlabeledChoices(*this->state, stateToIdCallback); - std::vector> allLabeledChoices = getLabeledChoices(*this->state, stateToIdCallback); + + std::vector> allChoices; + std::vector> allLabeledChoices; + if (this->getOptions().isApplyMaximalProgressAssumptionSet()) { + // First explore only edges without a rate + allChoices = getUnlabeledChoices(*this->state, stateToIdCallback, CommandFilter::Probabilistic); + allLabeledChoices = getLabeledChoices(*this->state, stateToIdCallback, CommandFilter::Probabilistic); + if (allChoices.empty() && allLabeledChoices.empty()) { + // Expand the Markovian edges if there are no probabilistic ones. + allChoices = getUnlabeledChoices(*this->state, stateToIdCallback, CommandFilter::Markovian); + allLabeledChoices = getLabeledChoices(*this->state, stateToIdCallback, CommandFilter::Markovian); + } + } else { + allChoices = getUnlabeledChoices(*this->state, stateToIdCallback); + allLabeledChoices = getLabeledChoices(*this->state, stateToIdCallback); + } for (auto& choice : allLabeledChoices) { - allChoices.push_back(std::move(choice)); + allChoices.push_back(std::move(choice)); } + std::size_t totalNumberOfChoices = allChoices.size(); // If there is not a single choice, we return immediately, because the state has no behavior (other than @@ -407,7 +422,7 @@ namespace storm { } template - boost::optional>>> PrismNextStateGenerator::getActiveCommandsByActionIndex(uint_fast64_t const& actionIndex) { + boost::optional>>> PrismNextStateGenerator::getActiveCommandsByActionIndex(uint_fast64_t const& actionIndex, CommandFilter const& commandFilter) { boost::optional>>> result((std::vector>>())); // Iterate over all modules. @@ -432,6 +447,12 @@ namespace storm { // Look up commands by their indices and add them if the guard evaluates to true in the given state. for (uint_fast64_t commandIndex : commandIndices) { storm::prism::Command const& command = module.getCommand(commandIndex); + if (commandFilter != CommandFilter::All) { + STORM_LOG_ASSERT(commandFilter == CommandFilter::Markovian || commandFilter == CommandFilter::Probabilistic, "Unexpected command filter."); + if ((commandFilter == CommandFilter::Markovian) != command.isMarkovian()) { + continue; + } + } if (this->evaluator->asBool(command.getGuardExpression())) { commands.push_back(command); } @@ -451,7 +472,7 @@ namespace storm { } template - std::vector> PrismNextStateGenerator::getUnlabeledChoices(CompressedState const& state, StateToIdCallback stateToIdCallback) { + std::vector> PrismNextStateGenerator::getUnlabeledChoices(CompressedState const& state, StateToIdCallback stateToIdCallback, CommandFilter const& commandFilter) { std::vector> result; // Iterate over all modules. @@ -465,6 +486,13 @@ namespace storm { // Only consider unlabeled commands. if (command.isLabeled()) continue; + if (commandFilter != CommandFilter::All) { + STORM_LOG_ASSERT(commandFilter == CommandFilter::Markovian || commandFilter == CommandFilter::Probabilistic, "Unexpected command filter."); + if ((commandFilter == CommandFilter::Markovian) != command.isMarkovian()) { + continue; + } + } + // Skip the command, if it is not enabled. if (!this->evaluator->asBool(command.getGuardExpression())) { continue; @@ -541,11 +569,11 @@ namespace storm { } template - std::vector> PrismNextStateGenerator::getLabeledChoices(CompressedState const& state, StateToIdCallback stateToIdCallback) { + std::vector> PrismNextStateGenerator::getLabeledChoices(CompressedState const& state, StateToIdCallback stateToIdCallback, CommandFilter const& commandFilter) { std::vector> result; for (uint_fast64_t actionIndex : program.getSynchronizingActionIndices()) { - boost::optional>>> optionalActiveCommandLists = getActiveCommandsByActionIndex(actionIndex); + boost::optional>>> optionalActiveCommandLists = getActiveCommandsByActionIndex(actionIndex, commandFilter); // Only process this action label, if there is at least one feasible solution. if (optionalActiveCommandLists) { diff --git a/src/storm/generator/PrismNextStateGenerator.h b/src/storm/generator/PrismNextStateGenerator.h index 73f2fd247..41be2912d 100644 --- a/src/storm/generator/PrismNextStateGenerator.h +++ b/src/storm/generator/PrismNextStateGenerator.h @@ -22,7 +22,8 @@ namespace storm { public: typedef typename NextStateGenerator::StateToIdCallback StateToIdCallback; typedef boost::container::flat_set CommandSet; - + enum class CommandFilter {All, Markovian, Probabilistic}; + PrismNextStateGenerator(storm::prism::Program const& program, NextStateGeneratorOptions const& options = NextStateGeneratorOptions()); virtual ModelType getModelType() const override; @@ -75,7 +76,7 @@ namespace storm { * @param actionIndex The index of the action label to select. * @return A list of lists of active commands or nothing. */ - boost::optional>>> getActiveCommandsByActionIndex(uint_fast64_t const& actionIndex); + boost::optional>>> getActiveCommandsByActionIndex(uint_fast64_t const& actionIndex, CommandFilter const& commandFilter = CommandFilter::All); /*! * Retrieves all unlabeled choices possible from the given state. @@ -83,7 +84,7 @@ namespace storm { * @param state The state for which to retrieve the unlabeled choices. * @return The unlabeled choices of the state. */ - std::vector> getUnlabeledChoices(CompressedState const& state, StateToIdCallback stateToIdCallback); + std::vector> getUnlabeledChoices(CompressedState const& state, StateToIdCallback stateToIdCallback, CommandFilter const& commandFilter = CommandFilter::All); /*! * Retrieves all labeled choices possible from the given state. @@ -91,7 +92,7 @@ namespace storm { * @param state The state for which to retrieve the unlabeled choices. * @return The labeled choices of the state. */ - std::vector> getLabeledChoices(CompressedState const& state, StateToIdCallback stateToIdCallback); + std::vector> getLabeledChoices(CompressedState const& state, StateToIdCallback stateToIdCallback, CommandFilter const& commandFilter = CommandFilter::All); /*! * A recursive helper function to generate a synchronziing distribution.