From 9e54ce4e8b938ad764536686364c0865cffed587 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Wed, 19 Feb 2020 15:29:37 +0100 Subject: [PATCH] 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 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 - DdJaniModelBuilder::Options::Options(bool buildAllLabels, bool buildAllRewardModels) : buildAllLabels(buildAllLabels), buildAllRewardModels(buildAllRewardModels), rewardModelsToBuild(), constantDefinitions(), terminalStates(), negatedTerminalStates() { + DdJaniModelBuilder::Options::Options(bool buildAllLabels, bool buildAllRewardModels) : buildAllLabels(buildAllLabels), buildAllRewardModels(buildAllRewardModels), rewardModelsToBuild(), constantDefinitions() { // Intentionally left empty. } template - DdJaniModelBuilder::Options::Options(storm::logic::Formula const& formula) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), terminalStates(), negatedTerminalStates() { + DdJaniModelBuilder::Options::Options(storm::logic::Formula const& formula) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions() { this->preserveFormula(formula); this->setTerminalStatesFromFormula(formula); } template - DdJaniModelBuilder::Options::Options(std::vector> const& formulas) : buildAllLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), terminalStates(), negatedTerminalStates() { + DdJaniModelBuilder::Options::Options(std::vector> 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 void DdJaniModelBuilder::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 void DdJaniModelBuilder::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 @@ -939,13 +913,14 @@ namespace storm { boost::optional 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::Bdd postprocessSystem(storm::jani::Model const& model, ComposerResult& system, CompositionVariables const& variables, typename DdJaniModelBuilder::Options const& options) { + storm::dd::Bdd postprocessSystem(storm::jani::Model const& model, ComposerResult& system, CompositionVariables const& variables, typename DdJaniModelBuilder::Options const& options, std::map 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 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 constantsSubstitution = model.getConstantsSubstitution(); - - storm::dd::Bdd 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 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(); - return terminalStatesBdd; } - return variables.manager->getBddZero(); + return terminalStatesBdd; } template @@ -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 terminalStates = postprocessSystem(preparedModel, system, variables, options); + storm::dd::Bdd terminalStates = postprocessSystem(preparedModel, system, variables, options, labelsToExpressionMap); // Start creating the model components. ModelComponents 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> 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 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 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 - DdPrismModelBuilder::Options::Options() : buildAllRewardModels(false), rewardModelsToBuild(), buildAllLabels(false), labelsToBuild(), terminalStates(), negatedTerminalStates() { + DdPrismModelBuilder::Options::Options() : buildAllRewardModels(false), rewardModelsToBuild(), buildAllLabels(false), labelsToBuild() { // Intentionally left empty. } template - DdPrismModelBuilder::Options::Options(storm::logic::Formula const& formula) : buildAllRewardModels(false), rewardModelsToBuild(), buildAllLabels(false), labelsToBuild(std::set()), terminalStates(), negatedTerminalStates() { + DdPrismModelBuilder::Options::Options(storm::logic::Formula const& formula) : buildAllRewardModels(false), rewardModelsToBuild(), buildAllLabels(false), labelsToBuild(std::set()) { this->preserveFormula(formula); this->setTerminalStatesFromFormula(formula); } template - DdPrismModelBuilder::Options::Options(std::vector> const& formulas) : buildAllRewardModels(false), rewardModelsToBuild(), buildAllLabels(false), labelsToBuild(), terminalStates(), negatedTerminalStates() { + DdPrismModelBuilder::Options::Options(std::vector> const& formulas) : buildAllRewardModels(false), rewardModelsToBuild(), buildAllLabels(false), labelsToBuild() { for (auto const& formula : formulas) { this->preserveFormula(*formula); } @@ -563,12 +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. - 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 void DdPrismModelBuilder::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 @@ -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 terminalStatesBdd = generationInfo.manager->getBddZero(); - if (options.terminalStates || options.negatedTerminalStates) { - std::map constantsSubstitution = program.getConstantsSubstitution(); - - if (options.terminalStates) { - storm::expressions::Expression terminalExpression; - if (options.terminalStates.get().type() == typeid(storm::expressions::Expression)) { - terminalExpression = boost::get(options.terminalStates.get()); - } else { - std::string const& labelName = boost::get(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(options.negatedTerminalStates.get()); - } else { - std::string const& labelName = boost::get(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(); } 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> 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> 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> 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 const& terminalExpressionCallback, std::function 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 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 +#include +#include + +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 const& terminalExpressionCallback, std::function const& terminalLabelCallback); + + + struct TerminalStates { + std::vector terminalExpressions; // if one of these is true, we can stop exploration + std::vector negatedTerminalExpressions; // if one of these is false, we can stop exploration + std::vector terminalLabels; // if a state has one of these labels, we can stop exploration + std::vector 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 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