From 9e54ce4e8b938ad764536686364c0865cffed587 Mon Sep 17 00:00:00 2001 From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de> Date: Wed, 19 Feb 2020 15:29:37 +0100 Subject: [PATCH 1/3] Improved detection of terminal states for Dd engine. Also reduced code duplication. --- src/storm/builder/BuilderOptions.cpp | 56 +------------ src/storm/builder/DdJaniModelBuilder.cpp | 86 +++++++------------- src/storm/builder/DdJaniModelBuilder.h | 8 +- src/storm/builder/DdPrismModelBuilder.cpp | 90 +++------------------ src/storm/builder/DdPrismModelBuilder.h | 10 +-- src/storm/builder/TerminalStatesGetter.cpp | 94 ++++++++++++++++++++++ src/storm/builder/TerminalStatesGetter.h | 53 ++++++++++++ 7 files changed, 202 insertions(+), 195 deletions(-) create mode 100644 src/storm/builder/TerminalStatesGetter.cpp create mode 100644 src/storm/builder/TerminalStatesGetter.h diff --git a/src/storm/builder/BuilderOptions.cpp b/src/storm/builder/BuilderOptions.cpp index 9a5b4737c..2224efe11 100644 --- a/src/storm/builder/BuilderOptions.cpp +++ b/src/storm/builder/BuilderOptions.cpp @@ -1,5 +1,7 @@ #include "storm/builder/BuilderOptions.h" +#include "storm/builder/TerminalStatesGetter.h" + #include "storm/logic/Formulas.h" #include "storm/logic/LiftableTransitionRewardsVisitor.h" @@ -95,58 +97,8 @@ namespace storm { } void BuilderOptions::setTerminalStatesFromFormula(storm::logic::Formula const& formula) { - if (formula.isAtomicExpressionFormula()) { - addTerminalExpression(formula.asAtomicExpressionFormula().getExpression(), true); - } else if (formula.isAtomicLabelFormula()) { - addTerminalLabel(formula.asAtomicLabelFormula().getLabel(), true); - } else if (formula.isEventuallyFormula()) { - storm::logic::Formula const& sub = formula.asEventuallyFormula().getSubformula(); - if (sub.isAtomicExpressionFormula() || sub.isAtomicLabelFormula()) { - this->setTerminalStatesFromFormula(sub); - } - } else if (formula.isUntilFormula()) { - storm::logic::Formula const& right = formula.asUntilFormula().getRightSubformula(); - if (right.isAtomicExpressionFormula() || right.isAtomicLabelFormula()) { - this->setTerminalStatesFromFormula(right); - } - storm::logic::Formula const& left = formula.asUntilFormula().getLeftSubformula(); - if (left.isAtomicExpressionFormula()) { - addTerminalExpression(left.asAtomicExpressionFormula().getExpression(), false); - } else if (left.isAtomicLabelFormula()) { - addTerminalLabel(left.asAtomicLabelFormula().getLabel(), false); - } - } else if (formula.isBoundedUntilFormula()) { - storm::logic::BoundedUntilFormula const& boundedUntil = formula.asBoundedUntilFormula(); - bool hasLowerBound = false; - for (uint64_t i = 0; i < boundedUntil.getDimension(); ++i) { - if (boundedUntil.hasLowerBound(i) && (boundedUntil.getLowerBound(i).containsVariables() || !storm::utility::isZero(boundedUntil.getLowerBound(i).evaluateAsRational()))) { - hasLowerBound = true; - break; - } - } - if (!hasLowerBound) { - storm::logic::Formula const& right = boundedUntil.getRightSubformula(); - if (right.isAtomicExpressionFormula() || right.isAtomicLabelFormula()) { - this->setTerminalStatesFromFormula(right); - } - } - storm::logic::Formula const& left = boundedUntil.getLeftSubformula(); - if (left.isAtomicExpressionFormula()) { - addTerminalExpression(left.asAtomicExpressionFormula().getExpression(), false); - } else if (left.isAtomicLabelFormula()) { - addTerminalLabel(left.asAtomicLabelFormula().getLabel(), false); - } - } else if (formula.isProbabilityOperatorFormula()) { - storm::logic::Formula const& sub = formula.asProbabilityOperatorFormula().getSubformula(); - if (sub.isEventuallyFormula() || sub.isUntilFormula() || sub.isBoundedUntilFormula()) { - this->setTerminalStatesFromFormula(sub); - } - } else if (formula.isRewardOperatorFormula() || formula.isTimeOperatorFormula()) { - storm::logic::Formula const& sub = formula.asOperatorFormula().getSubformula(); - if (sub.isEventuallyFormula()) { - this->setTerminalStatesFromFormula(sub); - } - } + getTerminalStatesFromFormula(formula, [this](storm::expressions::Expression const& expr, bool inverted){ this->addTerminalExpression(expr, inverted);} + , [this](std::string const& label, bool inverted){ this->addTerminalLabel(label, inverted);}); } std::set<std::string> const& BuilderOptions::getRewardModelNames() const { diff --git a/src/storm/builder/DdJaniModelBuilder.cpp b/src/storm/builder/DdJaniModelBuilder.cpp index 5940e4ac3..ff52955ee 100644 --- a/src/storm/builder/DdJaniModelBuilder.cpp +++ b/src/storm/builder/DdJaniModelBuilder.cpp @@ -46,18 +46,18 @@ namespace storm { namespace builder { template <storm::dd::DdType Type, typename ValueType> - DdJaniModelBuilder<Type, ValueType>::Options::Options(bool buildAllLabels, bool buildAllRewardModels) : buildAllLabels(buildAllLabels), buildAllRewardModels(buildAllRewardModels), rewardModelsToBuild(), constantDefinitions(), terminalStates(), negatedTerminalStates() { + DdJaniModelBuilder<Type, ValueType>::Options::Options(bool buildAllLabels, bool buildAllRewardModels) : buildAllLabels(buildAllLabels), buildAllRewardModels(buildAllRewardModels), rewardModelsToBuild(), constantDefinitions() { // Intentionally left empty. } template <storm::dd::DdType Type, typename ValueType> - DdJaniModelBuilder<Type, ValueType>::Options::Options(storm::logic::Formula const& formula) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), terminalStates(), negatedTerminalStates() { + DdJaniModelBuilder<Type, ValueType>::Options::Options(storm::logic::Formula const& formula) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions() { this->preserveFormula(formula); this->setTerminalStatesFromFormula(formula); } template <storm::dd::DdType Type, typename ValueType> - DdJaniModelBuilder<Type, ValueType>::Options::Options(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) : buildAllLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), terminalStates(), negatedTerminalStates() { + DdJaniModelBuilder<Type, ValueType>::Options::Options(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) : buildAllLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions() { if (!formulas.empty()) { for (auto const& formula : formulas) { this->preserveFormula(*formula); @@ -71,12 +71,7 @@ namespace storm { template <storm::dd::DdType Type, typename ValueType> void DdJaniModelBuilder<Type, ValueType>::Options::preserveFormula(storm::logic::Formula const& formula) { // If we already had terminal states, we need to erase them. - if (terminalStates) { - terminalStates.reset(); - } - if (negatedTerminalStates) { - negatedTerminalStates.reset(); - } + terminalStates = storm::builder::TerminalStates(); // If we are not required to build all reward models, we determine the reward models we need to build. if (!buildAllRewardModels) { @@ -93,28 +88,7 @@ namespace storm { template <storm::dd::DdType Type, typename ValueType> void DdJaniModelBuilder<Type, ValueType>::Options::setTerminalStatesFromFormula(storm::logic::Formula const& formula) { - if (formula.isAtomicExpressionFormula()) { - terminalStates = formula.asAtomicExpressionFormula().getExpression(); - } else if (formula.isEventuallyFormula()) { - storm::logic::Formula const& sub = formula.asEventuallyFormula().getSubformula(); - if (sub.isAtomicExpressionFormula() || sub.isAtomicLabelFormula()) { - this->setTerminalStatesFromFormula(sub); - } - } else if (formula.isUntilFormula()) { - storm::logic::Formula const& right = formula.asUntilFormula().getRightSubformula(); - if (right.isAtomicExpressionFormula() || right.isAtomicLabelFormula()) { - this->setTerminalStatesFromFormula(right); - } - storm::logic::Formula const& left = formula.asUntilFormula().getLeftSubformula(); - if (left.isAtomicExpressionFormula()) { - negatedTerminalStates = left.asAtomicExpressionFormula().getExpression(); - } - } else if (formula.isProbabilityOperatorFormula()) { - storm::logic::Formula const& sub = formula.asProbabilityOperatorFormula().getSubformula(); - if (sub.isEventuallyFormula() || sub.isUntilFormula()) { - this->setTerminalStatesFromFormula(sub); - } - } + terminalStates = getTerminalStatesFromFormula(formula); } template <storm::dd::DdType Type, typename ValueType> @@ -939,13 +913,14 @@ namespace storm { boost::optional<uint64_t> previousActionPosition = synchVector.getPositionOfPrecedingParticipatingAction(subcompositionIndex); STORM_LOG_ASSERT(previousActionPosition, "Inconsistent information about synchronization vector."); AutomatonDd const& previousAutomatonDd = subautomata[previousActionPosition.get()]; - auto precedingActionIt = previousAutomatonDd.actions.find(ActionIdentification(actionInformation.getActionIndex(synchVector.getInput(previousActionPosition.get())), synchronizationVectorIndex, isCtmc)); + auto precedingActionIndex = actionInformation.getActionIndex(synchVector.getInput(previousActionPosition.get())); + auto precedingActionIt = previousAutomatonDd.actions.find(ActionIdentification(precedingActionIndex, synchronizationVectorIndex, isCtmc)); uint64_t highestLocalNondeterminismVariable = 0; if (precedingActionIt != previousAutomatonDd.actions.end()) { highestLocalNondeterminismVariable = precedingActionIt->second.getHighestLocalNondeterminismVariable(); } else { - STORM_LOG_WARN("Subcomposition does not have action that is mentioned in parallel composition."); + STORM_LOG_WARN("Subcomposition does not have action" << actionInformation.getActionName(precedingActionIndex) << " that is mentioned in parallel composition."); } actionInstantiations[actionIndex].emplace_back(actionIndex, synchronizationVectorIndex, highestLocalNondeterminismVariable, isCtmc); } @@ -1870,7 +1845,7 @@ namespace storm { } template <storm::dd::DdType Type, typename ValueType> - storm::dd::Bdd<Type> postprocessSystem(storm::jani::Model const& model, ComposerResult<Type, ValueType>& system, CompositionVariables<Type, ValueType> const& variables, typename DdJaniModelBuilder<Type, ValueType>::Options const& options) { + storm::dd::Bdd<Type> postprocessSystem(storm::jani::Model const& model, ComposerResult<Type, ValueType>& system, CompositionVariables<Type, ValueType> const& variables, typename DdJaniModelBuilder<Type, ValueType>::Options const& options, std::map<std::string, storm::expressions::Expression> const& labelsToExpressionMap) { // For DTMCs, we normalize each row to 1 (to account for non-determinism). if (model.getModelType() == storm::jani::ModelType::DTMC) { storm::dd::Add<Type, ValueType> stateToNumberOfChoices = system.transitions.sumAbstract(variables.columnMetaVariables); @@ -1883,25 +1858,23 @@ namespace storm { } // If we were asked to treat some states as terminal states, we cut away their transitions now. - if (options.terminalStates || options.negatedTerminalStates) { - std::map<storm::expressions::Variable, storm::expressions::Expression> constantsSubstitution = model.getConstantsSubstitution(); - - storm::dd::Bdd<Type> terminalStatesBdd = variables.manager->getBddZero(); - if (options.terminalStates) { - storm::expressions::Expression terminalExpression = options.terminalStates.get().substitute(constantsSubstitution); - STORM_LOG_TRACE("Making the states satisfying " << terminalExpression << " terminal."); - terminalStatesBdd = variables.rowExpressionAdapter->translateExpression(terminalExpression).toBdd(); - } - if (options.negatedTerminalStates) { - storm::expressions::Expression negatedTerminalExpression = options.negatedTerminalStates.get().substitute(constantsSubstitution); - STORM_LOG_TRACE("Making the states *not* satisfying " << negatedTerminalExpression << " terminal."); - terminalStatesBdd |= !variables.rowExpressionAdapter->translateExpression(negatedTerminalExpression).toBdd(); - } - + storm::dd::Bdd<Type> terminalStatesBdd = variables.manager->getBddZero(); + if (!options.terminalStates.empty()) { + storm::expressions::Expression terminalExpression = options.terminalStates.asExpression([&model, &labelsToExpressionMap](std::string const& labelName) { + auto exprIt = labelsToExpressionMap.find(labelName); + if (exprIt != labelsToExpressionMap.end()) { + return exprIt->second; + } else { + STORM_LOG_THROW(labelName == "init" || labelName == "deadlock", storm::exceptions::InvalidArgumentException, "Terminal states refer to illegal label '" << labelName << "'."); + // If the label name is "init" we can abort 'exploration' directly at the initial state. If it is deadlock, we do not have to abort. + return model.getExpressionManager().boolean(labelName == "init"); + } + }); + terminalExpression = terminalExpression.substitute(model.getConstantsSubstitution()); + terminalStatesBdd = variables.rowExpressionAdapter->translateExpression(terminalExpression).toBdd(); system.transitions *= (!terminalStatesBdd).template toAdd<ValueType>(); - return terminalStatesBdd; } - return variables.manager->getBddZero(); + return terminalStatesBdd; } template <storm::dd::DdType Type, typename ValueType> @@ -2095,12 +2068,18 @@ namespace storm { // Postprocess the variables in place. postprocessVariables(preparedModel.getModelType(), system, variables); + // Build the label to expressions mapping. + auto labelsToExpressionMap = buildLabelExpressions(preparedModel, variables, options); + // Postprocess the system in place and get the states that were terminal (i.e. whose transitions were cut off). - storm::dd::Bdd<Type> terminalStates = postprocessSystem(preparedModel, system, variables, options); + storm::dd::Bdd<Type> terminalStates = postprocessSystem(preparedModel, system, variables, options, labelsToExpressionMap); // Start creating the model components. ModelComponents<Type, ValueType> modelComponents; + // Set the label expressions + modelComponents.labelToExpressionMap = std::move(labelsToExpressionMap); + // Build initial states. modelComponents.initialStates = computeInitialStates(preparedModel, variables); @@ -2128,9 +2107,6 @@ namespace storm { // Build the reward models. modelComponents.rewardModels = buildRewardModels(reachableStatesAdd, modelComponents.transitionMatrix, preparedModel.getModelType(), variables, system, rewardVariables); - // Build the label to expressions mapping. - modelComponents.labelToExpressionMap = buildLabelExpressions(preparedModel, variables, options); - // Finally, create the model. return createModel(preparedModel.getModelType(), variables, modelComponents); } diff --git a/src/storm/builder/DdJaniModelBuilder.h b/src/storm/builder/DdJaniModelBuilder.h index 371b52557..9dfe6f232 100644 --- a/src/storm/builder/DdJaniModelBuilder.h +++ b/src/storm/builder/DdJaniModelBuilder.h @@ -5,6 +5,7 @@ #include "storm/storage/dd/DdType.h" #include "storm/logic/Formula.h" +#include "storm/builder/TerminalStatesGetter.h" namespace storm { @@ -96,13 +97,10 @@ namespace storm { // An optional mapping that, if given, contains defining expressions for undefined constants. boost::optional<std::map<storm::expressions::Variable, storm::expressions::Expression>> constantDefinitions; - // An optional expression or label that (a subset of) characterizes the terminal states of the model. + // An optional set of expression or labels that characterizes (a subset of) the terminal states of the model. // If this is set, the outgoing transitions of these states are replaced with a self-loop. - boost::optional<storm::expressions::Expression> terminalStates; + storm::builder::TerminalStates terminalStates; - // An optional expression or label whose negation characterizes (a subset of) the terminal states of the - // model. If this is set, the outgoing transitions of these states are replaced with a self-loop. - boost::optional<storm::expressions::Expression> negatedTerminalStates; }; /*! diff --git a/src/storm/builder/DdPrismModelBuilder.cpp b/src/storm/builder/DdPrismModelBuilder.cpp index 1a25bdaa2..0e5a05c9a 100644 --- a/src/storm/builder/DdPrismModelBuilder.cpp +++ b/src/storm/builder/DdPrismModelBuilder.cpp @@ -540,18 +540,18 @@ namespace storm { }; template <storm::dd::DdType Type, typename ValueType> - DdPrismModelBuilder<Type, ValueType>::Options::Options() : buildAllRewardModels(false), rewardModelsToBuild(), buildAllLabels(false), labelsToBuild(), terminalStates(), negatedTerminalStates() { + DdPrismModelBuilder<Type, ValueType>::Options::Options() : buildAllRewardModels(false), rewardModelsToBuild(), buildAllLabels(false), labelsToBuild() { // Intentionally left empty. } template <storm::dd::DdType Type, typename ValueType> - DdPrismModelBuilder<Type, ValueType>::Options::Options(storm::logic::Formula const& formula) : buildAllRewardModels(false), rewardModelsToBuild(), buildAllLabels(false), labelsToBuild(std::set<std::string>()), terminalStates(), negatedTerminalStates() { + DdPrismModelBuilder<Type, ValueType>::Options::Options(storm::logic::Formula const& formula) : buildAllRewardModels(false), rewardModelsToBuild(), buildAllLabels(false), labelsToBuild(std::set<std::string>()) { this->preserveFormula(formula); this->setTerminalStatesFromFormula(formula); } template <storm::dd::DdType Type, typename ValueType> - DdPrismModelBuilder<Type, ValueType>::Options::Options(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) : buildAllRewardModels(false), rewardModelsToBuild(), buildAllLabels(false), labelsToBuild(), terminalStates(), negatedTerminalStates() { + DdPrismModelBuilder<Type, ValueType>::Options::Options(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) : buildAllRewardModels(false), rewardModelsToBuild(), buildAllLabels(false), labelsToBuild() { for (auto const& formula : formulas) { this->preserveFormula(*formula); } @@ -563,12 +563,7 @@ namespace storm { template <storm::dd::DdType Type, typename ValueType> void DdPrismModelBuilder<Type, ValueType>::Options::preserveFormula(storm::logic::Formula const& formula) { // If we already had terminal states, we need to erase them. - if (terminalStates) { - terminalStates.reset(); - } - if (negatedTerminalStates) { - negatedTerminalStates.reset(); - } + terminalStates = storm::builder::TerminalStates(); // If we are not required to build all reward models, we determine the reward models we need to build. if (!buildAllRewardModels) { @@ -588,32 +583,7 @@ namespace storm { template <storm::dd::DdType Type, typename ValueType> void DdPrismModelBuilder<Type, ValueType>::Options::setTerminalStatesFromFormula(storm::logic::Formula const& formula) { - if (formula.isAtomicExpressionFormula()) { - terminalStates = formula.asAtomicExpressionFormula().getExpression(); - } else if (formula.isAtomicLabelFormula()) { - terminalStates = formula.asAtomicLabelFormula().getLabel(); - } else if (formula.isEventuallyFormula()) { - storm::logic::Formula const& sub = formula.asEventuallyFormula().getSubformula(); - if (sub.isAtomicExpressionFormula() || sub.isAtomicLabelFormula()) { - this->setTerminalStatesFromFormula(sub); - } - } else if (formula.isUntilFormula()) { - storm::logic::Formula const& right = formula.asUntilFormula().getRightSubformula(); - if (right.isAtomicExpressionFormula() || right.isAtomicLabelFormula()) { - this->setTerminalStatesFromFormula(right); - } - storm::logic::Formula const& left = formula.asUntilFormula().getLeftSubformula(); - if (left.isAtomicExpressionFormula()) { - negatedTerminalStates = left.asAtomicExpressionFormula().getExpression(); - } else if (left.isAtomicLabelFormula()) { - negatedTerminalStates = left.asAtomicLabelFormula().getLabel(); - } - } else if (formula.isProbabilityOperatorFormula()) { - storm::logic::Formula const& sub = formula.asProbabilityOperatorFormula().getSubformula(); - if (sub.isEventuallyFormula() || sub.isUntilFormula()) { - this->setTerminalStatesFromFormula(sub); - } - } + terminalStates = getTerminalStatesFromFormula(formula); } template <storm::dd::DdType Type, typename ValueType> @@ -1351,52 +1321,18 @@ namespace storm { // If we were asked to treat some states as terminal states, we cut away their transitions now. storm::dd::Bdd<Type> terminalStatesBdd = generationInfo.manager->getBddZero(); - if (options.terminalStates || options.negatedTerminalStates) { - std::map<storm::expressions::Variable, storm::expressions::Expression> constantsSubstitution = program.getConstantsSubstitution(); - - if (options.terminalStates) { - storm::expressions::Expression terminalExpression; - if (options.terminalStates.get().type() == typeid(storm::expressions::Expression)) { - terminalExpression = boost::get<storm::expressions::Expression>(options.terminalStates.get()); - } else { - std::string const& labelName = boost::get<std::string>(options.terminalStates.get()); + if (!options.terminalStates.empty()) { + storm::expressions::Expression terminalExpression = options.terminalStates.asExpression([&program](std::string const& labelName) { if (program.hasLabel(labelName)) { - terminalExpression = program.getLabelExpression(labelName); + return program.getLabelExpression(labelName); } else { STORM_LOG_THROW(labelName == "init" || labelName == "deadlock", storm::exceptions::InvalidArgumentException, "Terminal states refer to illegal label '" << labelName << "'."); + // If the label name is "init" we can abort 'exploration' directly at the initial state. If it is deadlock, we do not have to abort. + return program.getManager().boolean(labelName == "init"); } - } - - if (terminalExpression.isInitialized()) { - // If the expression refers to constants of the model, we need to substitute them. - terminalExpression = terminalExpression.substitute(constantsSubstitution); - - STORM_LOG_TRACE("Making the states satisfying " << terminalExpression << " terminal."); - terminalStatesBdd = generationInfo.rowExpressionAdapter->translateExpression(terminalExpression).toBdd(); - } - } - if (options.negatedTerminalStates) { - storm::expressions::Expression negatedTerminalExpression; - if (options.negatedTerminalStates.get().type() == typeid(storm::expressions::Expression)) { - negatedTerminalExpression = boost::get<storm::expressions::Expression>(options.negatedTerminalStates.get()); - } else { - std::string const& labelName = boost::get<std::string>(options.negatedTerminalStates.get()); - if (program.hasLabel(labelName)) { - negatedTerminalExpression = program.getLabelExpression(labelName); - } else { - STORM_LOG_THROW(labelName == "init" || labelName == "deadlock", storm::exceptions::InvalidArgumentException, "Terminal states refer to illegal label '" << labelName << "'."); - } - } - - if (negatedTerminalExpression.isInitialized()) { - // If the expression refers to constants of the model, we need to substitute them. - negatedTerminalExpression = negatedTerminalExpression.substitute(constantsSubstitution); - - STORM_LOG_TRACE("Making the states *not* satisfying " << negatedTerminalExpression << " terminal."); - terminalStatesBdd |= !generationInfo.rowExpressionAdapter->translateExpression(negatedTerminalExpression).toBdd(); - } - } - + }); + terminalExpression = terminalExpression.substitute(program.getConstantsSubstitution()); + terminalStatesBdd = generationInfo.rowExpressionAdapter->translateExpression(terminalExpression).toBdd(); transitionMatrix *= (!terminalStatesBdd).template toAdd<ValueType>(); } diff --git a/src/storm/builder/DdPrismModelBuilder.h b/src/storm/builder/DdPrismModelBuilder.h index fb357a6c8..a529f0656 100644 --- a/src/storm/builder/DdPrismModelBuilder.h +++ b/src/storm/builder/DdPrismModelBuilder.h @@ -7,6 +7,8 @@ #include "storm/storage/prism/Program.h" +#include "storm/builder/TerminalStatesGetter.h" + #include "storm/logic/Formulas.h" #include "storm/adapters/AddExpressionAdapter.h" #include "storm/utility/macros.h" @@ -81,13 +83,9 @@ namespace storm { // An optional set of labels that, if given, restricts the labels that are built. boost::optional<std::set<std::string>> labelsToBuild; - // An optional expression or label that (a subset of) characterizes the terminal states of the model. + // An optional set of expression or labels that characterizes (a subset of) the terminal states of the model. // If this is set, the outgoing transitions of these states are replaced with a self-loop. - boost::optional<boost::variant<storm::expressions::Expression, std::string>> terminalStates; - - // An optional expression or label whose negation characterizes (a subset of) the terminal states of the - // model. If this is set, the outgoing transitions of these states are replaced with a self-loop. - boost::optional<boost::variant<storm::expressions::Expression, std::string>> negatedTerminalStates; + storm::builder::TerminalStates terminalStates; }; /*! diff --git a/src/storm/builder/TerminalStatesGetter.cpp b/src/storm/builder/TerminalStatesGetter.cpp new file mode 100644 index 000000000..11a4ccb85 --- /dev/null +++ b/src/storm/builder/TerminalStatesGetter.cpp @@ -0,0 +1,94 @@ +#include "storm/builder/TerminalStatesGetter.h" + +#include "storm/storage/expressions/Expression.h" +#include "storm/logic/Formulas.h" + +namespace storm { + namespace builder { + void getTerminalStatesFromFormula(storm::logic::Formula const& formula, std::function<void(storm::expressions::Expression const&, bool)> const& terminalExpressionCallback, std::function<void(std::string const&, bool)> const& terminalLabelCallback) { + if (formula.isAtomicExpressionFormula()) { + terminalExpressionCallback(formula.asAtomicExpressionFormula().getExpression(), true); + } else if (formula.isAtomicLabelFormula()) { + terminalLabelCallback(formula.asAtomicLabelFormula().getLabel(), true); + } else if (formula.isEventuallyFormula()) { + storm::logic::Formula const& sub = formula.asEventuallyFormula().getSubformula(); + if (sub.isAtomicExpressionFormula() || sub.isAtomicLabelFormula()) { + getTerminalStatesFromFormula(sub, terminalExpressionCallback, terminalLabelCallback); + } + } else if (formula.isUntilFormula()) { + storm::logic::Formula const& right = formula.asUntilFormula().getRightSubformula(); + if (right.isAtomicExpressionFormula() || right.isAtomicLabelFormula()) { + getTerminalStatesFromFormula(right, terminalExpressionCallback, terminalLabelCallback); + } + storm::logic::Formula const& left = formula.asUntilFormula().getLeftSubformula(); + if (left.isAtomicExpressionFormula()) { + terminalExpressionCallback(left.asAtomicExpressionFormula().getExpression(), false); + } else if (left.isAtomicLabelFormula()) { + terminalLabelCallback(left.asAtomicLabelFormula().getLabel(), false); + } + } else if (formula.isBoundedUntilFormula()) { + storm::logic::BoundedUntilFormula const& boundedUntil = formula.asBoundedUntilFormula(); + bool hasLowerBound = false; + for (uint64_t i = 0; i < boundedUntil.getDimension(); ++i) { + if (boundedUntil.hasLowerBound(i) && (boundedUntil.getLowerBound(i).containsVariables() || !storm::utility::isZero(boundedUntil.getLowerBound(i).evaluateAsRational()))) { + hasLowerBound = true; + break; + } + } + if (!hasLowerBound) { + storm::logic::Formula const& right = boundedUntil.getRightSubformula(); + if (right.isAtomicExpressionFormula() || right.isAtomicLabelFormula()) { + getTerminalStatesFromFormula(right, terminalExpressionCallback, terminalLabelCallback); + } + } + storm::logic::Formula const& left = boundedUntil.getLeftSubformula(); + if (left.isAtomicExpressionFormula()) { + terminalExpressionCallback(left.asAtomicExpressionFormula().getExpression(), false); + } else if (left.isAtomicLabelFormula()) { + terminalLabelCallback(left.asAtomicLabelFormula().getLabel(), false); + } + } else if (formula.isProbabilityOperatorFormula()) { + storm::logic::Formula const& sub = formula.asProbabilityOperatorFormula().getSubformula(); + if (sub.isEventuallyFormula() || sub.isUntilFormula() || sub.isBoundedUntilFormula()) { + getTerminalStatesFromFormula(sub, terminalExpressionCallback, terminalLabelCallback); + } + } else if (formula.isRewardOperatorFormula() || formula.isTimeOperatorFormula()) { + storm::logic::Formula const& sub = formula.asOperatorFormula().getSubformula(); + if (sub.isEventuallyFormula()) { + getTerminalStatesFromFormula(sub, terminalExpressionCallback, terminalLabelCallback); + } + } + } + + bool TerminalStates::empty() const { + return terminalExpressions.empty() && negatedTerminalExpressions.empty() && terminalLabels.empty() && negatedTerminalLabels.empty(); + } + + storm::expressions::Expression TerminalStates::asExpression(std::function<storm::expressions::Expression(std::string const&)> const& labelToExpressionMap) const { + auto allTerminalExpressions = terminalExpressions; + for (auto const& e : negatedTerminalExpressions) { + allTerminalExpressions.push_back(!e); + } + for (auto const& l : terminalLabels) { + allTerminalExpressions.push_back(labelToExpressionMap(l)); + } + for (auto const& l : negatedTerminalLabels) { + allTerminalExpressions.push_back(!labelToExpressionMap(l)); + } + STORM_LOG_ASSERT(!allTerminalExpressions.empty(), "Unable to convert empty terminal state set to expression"); + return storm::expressions::disjunction(allTerminalExpressions); + } + + TerminalStates getTerminalStatesFromFormula(storm::logic::Formula const& formula) { + TerminalStates result; + getTerminalStatesFromFormula(formula, [&result](storm::expressions::Expression const& expr, bool inverted){ if(inverted) { result.terminalExpressions.push_back(expr);} else {result.negatedTerminalExpressions.push_back(expr);} }, + [&result](std::string const& label, bool inverted){ if(inverted) { result.terminalLabels.push_back(label);} else {result.negatedTerminalLabels.push_back(label);} }); + return result; + } + + + + + + } +} \ No newline at end of file diff --git a/src/storm/builder/TerminalStatesGetter.h b/src/storm/builder/TerminalStatesGetter.h new file mode 100644 index 000000000..c9eb2c6c0 --- /dev/null +++ b/src/storm/builder/TerminalStatesGetter.h @@ -0,0 +1,53 @@ +#pragma once + +#include <functional> +#include <string> +#include <vector> + +namespace storm { + + namespace expressions { + class Expression; + } + namespace logic { + class Formula; + } + + namespace builder { + + /*! + * Traverses the formula. If an expression (or label) is found such that checking the formula does not require further exploration from a state + * satisfying (or violating) the expression (or label), the corresponding callback function is called. + * @param formula The formula to analyzed + * @param terminalExpressionCallback called on terminal expressions. The corresponding flag indicates whether exploration can stop from states satisfying (true) or violating (false) the expression + * @param terminalLabelCallback called on terminal labels. The corresponding flag indicates whether exploration can stop from states having (true) or not having (false) the label + */ + void getTerminalStatesFromFormula(storm::logic::Formula const& formula, std::function<void(storm::expressions::Expression const&, bool)> const& terminalExpressionCallback, std::function<void(std::string const&, bool)> const& terminalLabelCallback); + + + struct TerminalStates { + std::vector<storm::expressions::Expression> terminalExpressions; // if one of these is true, we can stop exploration + std::vector<storm::expressions::Expression> negatedTerminalExpressions; // if one of these is false, we can stop exploration + std::vector<std::string> terminalLabels; // if a state has one of these labels, we can stop exploration + std::vector<std::string> negatedTerminalLabels; // if a state does not have all of these labels, we can stop exploration + + /*! + * True if no terminal states are specified + */ + bool empty() const; + + /*! + * Returns an expression that evaluates to true only if the exploration can stop at the corresponding state + * Should only be called if this is not empty. + */ + storm::expressions::Expression asExpression(std::function<storm::expressions::Expression(std::string const&)> const& labelToExpressionMap) const; + }; + + /*! + * Traverses the formula. If an expression (or label) is found such that checking the formula does not require further exploration from a state + * satisfying (or violating) the expression (or label), it is inserted into the returned struct. + */ + TerminalStates getTerminalStatesFromFormula(storm::logic::Formula const& formula); + + } +} \ No newline at end of file From ba6f0c0e877af75d8ed4a967bcbc8edac46ac855 Mon Sep 17 00:00:00 2001 From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de> Date: Thu, 20 Feb 2020 12:01:55 +0100 Subject: [PATCH 2/3] BuildSettings: Added the possiblities to build a model with choiceorigins and without max. progress assumption. --- CHANGELOG.md | 2 ++ src/storm-cli-utilities/model-handling.h | 13 +++++++++---- src/storm/api/builder.h | 4 +++- src/storm/builder/TerminalStatesGetter.cpp | 7 +++++++ src/storm/builder/TerminalStatesGetter.h | 5 +++++ src/storm/settings/modules/BuildSettings.cpp | 12 ++++++++++++ src/storm/settings/modules/BuildSettings.h | 13 +++++++++++-- 7 files changed, 49 insertions(+), 7 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 3a5c36231..df9f29923 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -9,6 +9,8 @@ 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`). +- 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 - `storm-pomdp`: Various fixes that prevented usage. diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index a49d244e5..b35b9f0d3 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -260,7 +260,8 @@ namespace storm { template <storm::dd::DdType DdType, typename ValueType> std::shared_ptr<storm::models::ModelBase> buildModelDd(SymbolicInput const& input) { - return storm::api::buildSymbolicModel<DdType, ValueType>(input.model.get(), createFormulasToRespect(input.properties), storm::settings::getModule<storm::settings::modules::BuildSettings>().isBuildFullModelSet()); + auto buildSettings = storm::settings::getModule<storm::settings::modules::BuildSettings>(); + return storm::api::buildSymbolicModel<DdType, ValueType>(input.model.get(), createFormulasToRespect(input.properties), buildSettings.isBuildFullModelSet(), !buildSettings.isApplyNoMaximumProgressAssumptionSet()); } template <typename ValueType> @@ -268,19 +269,23 @@ namespace storm { storm::builder::BuilderOptions options(createFormulasToRespect(input.properties), input.model.get()); options.setBuildChoiceLabels(buildSettings.isBuildChoiceLabelsSet()); options.setBuildStateValuations(buildSettings.isBuildStateValuationsSet()); - bool buildChoiceOrigins = false; + bool buildChoiceOrigins = buildSettings.isBuildChoiceOriginsSet(); if (storm::settings::manager().hasModule(storm::settings::modules::CounterexampleGeneratorSettings::moduleName)) { auto counterexampleGeneratorSettings = storm::settings::getModule<storm::settings::modules::CounterexampleGeneratorSettings>(); if (counterexampleGeneratorSettings.isCounterexampleSet()) { - buildChoiceOrigins = counterexampleGeneratorSettings.isMinimalCommandSetGenerationSet(); + buildChoiceOrigins |= counterexampleGeneratorSettings.isMinimalCommandSetGenerationSet(); } - options.setBuildChoiceOrigins(buildChoiceOrigins); } + options.setBuildChoiceOrigins(buildChoiceOrigins); if (input.model->getModelType() == storm::storage::SymbolicModelDescription::ModelType::POMDP) { options.setBuildChoiceOrigins(true); options.setBuildChoiceLabels(true); } + if (buildSettings.isApplyNoMaximumProgressAssumptionSet()) { + options.setApplyMaximalProgressAssumption(false); + } + options.setAddOutOfBoundsState(buildSettings.isBuildOutOfBoundsStateSet()); if (buildSettings.isBuildFullModelSet()) { options.clearTerminalStates(); diff --git a/src/storm/api/builder.h b/src/storm/api/builder.h index 0df66c7ff..6be939496 100644 --- a/src/storm/api/builder.h +++ b/src/storm/api/builder.h @@ -43,7 +43,7 @@ namespace storm { } template<storm::dd::DdType LibraryType, typename ValueType> - std::shared_ptr<storm::models::symbolic::Model<LibraryType, ValueType>> buildSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool buildFullModel = false) { + std::shared_ptr<storm::models::symbolic::Model<LibraryType, ValueType>> buildSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool buildFullModel = false, bool applyMaximumProgress = true) { if (model.isPrismProgram()) { typename storm::builder::DdPrismModelBuilder<LibraryType, ValueType>::Options options; options = typename storm::builder::DdPrismModelBuilder<LibraryType, ValueType>::Options(formulas); @@ -51,6 +51,7 @@ namespace storm { if (buildFullModel) { options.buildAllLabels = true; options.buildAllRewardModels = true; + options.terminalStates.clear(); } storm::builder::DdPrismModelBuilder<LibraryType, ValueType> builder; @@ -63,6 +64,7 @@ namespace storm { if (buildFullModel) { options.buildAllLabels = true; options.buildAllRewardModels = true; + options.terminalStates.clear(); } storm::builder::DdJaniModelBuilder<LibraryType, ValueType> builder; diff --git a/src/storm/builder/TerminalStatesGetter.cpp b/src/storm/builder/TerminalStatesGetter.cpp index 11a4ccb85..16779b8d9 100644 --- a/src/storm/builder/TerminalStatesGetter.cpp +++ b/src/storm/builder/TerminalStatesGetter.cpp @@ -60,6 +60,13 @@ namespace storm { } } + void TerminalStates::clear() { + terminalExpressions.clear(); + negatedTerminalExpressions.clear(); + terminalLabels.clear(); + negatedTerminalLabels.clear(); + } + bool TerminalStates::empty() const { return terminalExpressions.empty() && negatedTerminalExpressions.empty() && terminalLabels.empty() && negatedTerminalLabels.empty(); } diff --git a/src/storm/builder/TerminalStatesGetter.h b/src/storm/builder/TerminalStatesGetter.h index c9eb2c6c0..f41413f28 100644 --- a/src/storm/builder/TerminalStatesGetter.h +++ b/src/storm/builder/TerminalStatesGetter.h @@ -31,6 +31,11 @@ namespace storm { std::vector<std::string> terminalLabels; // if a state has one of these labels, we can stop exploration std::vector<std::string> negatedTerminalLabels; // if a state does not have all of these labels, we can stop exploration + /*! + * Clears all terminal states. After calling this, empty() holds. + */ + void clear(); + /*! * True if no terminal states are specified */ diff --git a/src/storm/settings/modules/BuildSettings.cpp b/src/storm/settings/modules/BuildSettings.cpp index 3ebc6d109..b460d7ba6 100644 --- a/src/storm/settings/modules/BuildSettings.cpp +++ b/src/storm/settings/modules/BuildSettings.cpp @@ -29,7 +29,9 @@ namespace storm { const std::string dontFixDeadlockOptionShortName = "ndl"; const std::string noBuildOptionName = "nobuild"; const std::string fullModelBuildOptionName = "buildfull"; + const std::string applyNoMaxProgAssumptionOptionName = "nomaxprog"; const std::string buildChoiceLabelOptionName = "buildchoicelab"; + const std::string buildChoiceOriginsOptionName = "buildchoiceorig"; const std::string buildStateValuationsOptionName = "buildstateval"; const std::string buildOutOfBoundsStateOptionName = "buildoutofboundsstate"; const std::string bitsForUnboundedVariablesOptionName = "int-bits"; @@ -40,7 +42,9 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, dontFixDeadlockOptionName, false, "If the model contains deadlock states, they need to be fixed by setting this option.").setShortName(dontFixDeadlockOptionShortName).setIsAdvanced().build()); this->addOption(storm::settings::OptionBuilder(moduleName, jitOptionName, false, "If set, the model is built using the JIT model builder.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, fullModelBuildOptionName, false, "If set, include all rewards and labels.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, applyNoMaxProgAssumptionOptionName, false, "If set, the maximum progress assumption is not applied while building the model (relevant for MAs)").setIsAdvanced().build()); this->addOption(storm::settings::OptionBuilder(moduleName, buildChoiceLabelOptionName, false, "If set, also build the choice labels").setIsAdvanced().build()); + this->addOption(storm::settings::OptionBuilder(moduleName, buildChoiceOriginsOptionName, false, "If set, also build information that for each choice indicates the part(s) of the input that yielded the choice.").setIsAdvanced().build()); this->addOption(storm::settings::OptionBuilder(moduleName, buildStateValuationsOptionName, false, "If set, also build the state valuations").setIsAdvanced().build()); this->addOption(storm::settings::OptionBuilder(moduleName, noBuildOptionName, false, "If set, do not build the model.").setIsAdvanced().build()); @@ -81,9 +85,17 @@ namespace storm { return this->getOption(noBuildOptionName).getHasOptionBeenSet(); } + bool BuildSettings::isApplyNoMaximumProgressAssumptionSet() const { + return this->getOption(applyNoMaxProgAssumptionOptionName).getHasOptionBeenSet(); + } + bool BuildSettings::isBuildChoiceLabelsSet() const { return this->getOption(buildChoiceLabelOptionName).getHasOptionBeenSet(); } + + bool BuildSettings::isBuildChoiceOriginsSet() const { + return this->getOption(buildChoiceOriginsOptionName).getHasOptionBeenSet(); + } bool BuildSettings::isBuildStateValuationsSet() const { return this->getOption(buildStateValuationsOptionName).getHasOptionBeenSet(); diff --git a/src/storm/settings/modules/BuildSettings.h b/src/storm/settings/modules/BuildSettings.h index b80424c7f..274f42da1 100644 --- a/src/storm/settings/modules/BuildSettings.h +++ b/src/storm/settings/modules/BuildSettings.h @@ -78,12 +78,21 @@ namespace storm { * @return true iff the full model should be build. */ bool isBuildFullModelSet() const; - + + /*! + * Retrieves whether the maximum progress assumption is to be applied when building the model + */ + bool isApplyNoMaximumProgressAssumptionSet() const; + /*! * Retrieves whether the choice labels should be build - * @return */ bool isBuildChoiceLabelsSet() const; + + /*! + * Retrieves whether the choice origins should be build + */ + bool isBuildChoiceOriginsSet() const; /*! * Retrieves whether the choice labels should be build From f7e2ff08437977187421d92dffbebce3490caea1 Mon Sep 17 00:00:00 2001 From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de> Date: Thu, 20 Feb 2020 12:02:32 +0100 Subject: [PATCH 3/3] 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<LibraryType, ValueType>::Options options; options = typename storm::builder::DdPrismModelBuilder<LibraryType, ValueType>::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<LibraryType, ValueType>::Options options; - options = typename storm::builder::DdJaniModelBuilder<LibraryType, ValueType>::Options(formulas); + typename storm::builder::DdJaniModelBuilder<LibraryType, ValueType>::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<LibraryType, ValueType> builder; @@ -73,12 +74,12 @@ namespace storm { } template<> - inline std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD, storm::RationalNumber>> buildSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool buildFullModel) { + inline std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD, storm::RationalNumber>> buildSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool, bool) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "CUDD does not support rational numbers."); } template<> - inline std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD, storm::RationalFunction>> buildSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool buildFullModel) { + inline std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD, storm::RationalFunction>> buildSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> 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 <storm::dd::DdType Type, typename ValueType> - DdJaniModelBuilder<Type, ValueType>::Options::Options(bool buildAllLabels, bool buildAllRewardModels) : buildAllLabels(buildAllLabels), buildAllRewardModels(buildAllRewardModels), rewardModelsToBuild(), constantDefinitions() { + DdJaniModelBuilder<Type, ValueType>::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 <storm::dd::DdType Type, typename ValueType> void DdJaniModelBuilder<Type, ValueType>::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<Type> const& condition) { + guard &= condition; + storm::dd::Add<Type, ValueType> conditionAdd = condition.template toAdd<ValueType>(); + 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<Type> guard; - // A DD that represents the transitions of this edge. + // A DD that represents the transitions of this action. storm::dd::Add<Type, ValueType> transitions; // A mapping from transient variables to their assignments. @@ -787,11 +800,12 @@ namespace storm { std::pair<uint64_t, uint64_t> localNondeterminismVariables; }; - CombinedEdgesSystemComposer(storm::jani::Model const& model, storm::jani::CompositionInformation const& actionInformation, CompositionVariables<Type, ValueType> const& variables, std::vector<storm::expressions::Variable> const& transientVariables) : SystemComposer<Type, ValueType>(model, variables, transientVariables), actionInformation(actionInformation) { + CombinedEdgesSystemComposer(storm::jani::Model const& model, storm::jani::CompositionInformation const& actionInformation, CompositionVariables<Type, ValueType> const& variables, std::vector<storm::expressions::Variable> const& transientVariables, bool applyMaximumProgress) : SystemComposer<Type, ValueType>(model, variables, transientVariables), actionInformation(actionInformation), applyMaximumProgress(applyMaximumProgress) { // Intentionally left empty. } storm::jani::CompositionInformation const& actionInformation; + bool applyMaximumProgress; ComposerResult<Type, ValueType> 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<AutomatonDd> const& subautomata, std::vector<storm::jani::SynchronizationVector> const& synchronizationVectors) { AutomatonDd result(this->variables.manager->template getAddOne<ValueType>()); + // Disjunction of all guards of non-markovian actions (only required for maximum progress assumption. + storm::dd::Bdd<Type> nonMarkovianActionGuards = this->variables.manager->getBddZero(); + // Build the results of the synchronization vectors. std::unordered_map<ActionIdentification, std::vector<ActionDd>, ActionIdentificationHash> actions; for (uint64_t synchronizationVectorIndex = 0; synchronizationVectorIndex < synchronizationVectors.size(); ++synchronizationVectorIndex) { @@ -943,6 +960,11 @@ namespace storm { boost::optional<ActionDd> 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<storm::expressions::Variable> rewardVariables = selectRewardVariables<Type, ValueType>(preparedModel, options); // Create a builder to compose and build the model. - CombinedEdgesSystemComposer<Type, ValueType> composer(preparedModel, actionInformation, variables, rewardVariables); + bool applyMaximumProgress = options.applyMaximumProgressAssumption && model.getModelType() == storm::jani::ModelType::MA; + CombinedEdgesSystemComposer<Type, ValueType> composer(preparedModel, actionInformation, variables, rewardVariables, applyMaximumProgress); ComposerResult<Type, ValueType> 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 <code>preserveFormula</code>. @@ -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<std::string> 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<std::string> labelNames; + // A list of reward models to be build in case not all reward models are to be build. std::set<std::string> 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 <storm::dd::DdType Type, typename ValueType> void DdPrismModelBuilder<Type, ValueType>::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) {