diff --git a/src/storm/api/builder.h b/src/storm/api/builder.h index ad39362df..f1520aed4 100644 --- a/src/storm/api/builder.h +++ b/src/storm/api/builder.h @@ -110,7 +110,7 @@ namespace storm { template std::shared_ptr> buildSparseModel(storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas, bool jit = false, bool doctor = false) { - storm::builder::BuilderOptions options(formulas); + storm::builder::BuilderOptions options(formulas, model); return buildSparseModel(model, options, jit, doctor); } diff --git a/src/storm/builder/BuilderOptions.cpp b/src/storm/builder/BuilderOptions.cpp index 791bc661a..50eb412e3 100644 --- a/src/storm/builder/BuilderOptions.cpp +++ b/src/storm/builder/BuilderOptions.cpp @@ -1,7 +1,7 @@ #include "storm/builder/BuilderOptions.h" #include "storm/logic/Formulas.h" -#include "storm/logic/FragmentSpecification.h" +#include "storm/logic/LiftableTransitionRewardsVisitor.h" #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/BuildSettings.h" @@ -42,15 +42,15 @@ namespace storm { // Intentionally left empty. } - BuilderOptions::BuilderOptions(storm::logic::Formula const& formula) : BuilderOptions() { - this->preserveFormula(formula); + BuilderOptions::BuilderOptions(storm::logic::Formula const& formula, storm::storage::SymbolicModelDescription const& modelDescription) : BuilderOptions() { + this->preserveFormula(formula, modelDescription); this->setTerminalStatesFromFormula(formula); } - BuilderOptions::BuilderOptions(std::vector> const& formulas) : BuilderOptions() { + BuilderOptions::BuilderOptions(std::vector> const& formulas, storm::storage::SymbolicModelDescription const& modelDescription) : BuilderOptions() { if (!formulas.empty()) { for (auto const& formula : formulas) { - this->preserveFormula(*formula); + this->preserveFormula(*formula, modelDescription); } if (formulas.size() == 1) { this->setTerminalStatesFromFormula(*formulas.front()); @@ -65,7 +65,7 @@ namespace storm { showProgressDelay = generalSettings.getShowProgressDelay(); } - void BuilderOptions::preserveFormula(storm::logic::Formula const& formula) { + void BuilderOptions::preserveFormula(storm::logic::Formula const& formula, storm::storage::SymbolicModelDescription const& modelDescription) { // If we already had terminal states, we need to erase them. if (hasTerminalStates()) { clearTerminalStates(); @@ -89,9 +89,7 @@ namespace storm { addLabel(formula->getExpression()); } - storm::logic::FragmentSpecification transitionRewardScalingFragment = storm::logic::csl().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setLongRunAverageOperatorsAllowed(true).setMultiObjectiveFormulasAllowed(true).setTotalRewardFormulasAllowed(true).setStepBoundedCumulativeRewardFormulasAllowed(true).setTimeBoundedCumulativeRewardFormulasAllowed(true); - scaleAndLiftTransitionRewards = scaleAndLiftTransitionRewards && formula.isInFragment(transitionRewardScalingFragment); - + scaleAndLiftTransitionRewards = scaleAndLiftTransitionRewards && storm::logic::LiftableTransitionRewardsVisitor(modelDescription).areTransitionRewardsLiftable(formula); } void BuilderOptions::setTerminalStatesFromFormula(storm::logic::Formula const& formula) { diff --git a/src/storm/builder/BuilderOptions.h b/src/storm/builder/BuilderOptions.h index d0982fa85..c23a053f9 100644 --- a/src/storm/builder/BuilderOptions.h +++ b/src/storm/builder/BuilderOptions.h @@ -8,6 +8,7 @@ #include #include "storm/storage/expressions/Expression.h" +#include "storm/storage/SymbolicModelDescription.h" namespace storm { namespace expressions { @@ -54,7 +55,7 @@ namespace storm { * * @param formula The formula based on which to choose the building options. */ - BuilderOptions(storm::logic::Formula const& formula); + BuilderOptions(storm::logic::Formula const& formula, storm::storage::SymbolicModelDescription const& modelDescription = storm::storage::SymbolicModelDescription()); /*! * Creates an object representing the suggested building options assuming that the given formulas are @@ -62,7 +63,7 @@ namespace storm { * * @param formula Thes formula based on which to choose the building options. */ - BuilderOptions(std::vector> const& formulas); + BuilderOptions(std::vector> const& formulas, storm::storage::SymbolicModelDescription const& modelDescription = storm::storage::SymbolicModelDescription()); /*! * Changes the options in a way that ensures that the given formula can be checked on the model once it @@ -70,7 +71,7 @@ namespace storm { * * @param formula The formula that is to be ''preserved''. */ - void preserveFormula(storm::logic::Formula const& formula); + void preserveFormula(storm::logic::Formula const& formula, storm::storage::SymbolicModelDescription const& modelDescription = storm::storage::SymbolicModelDescription()); /*! * Analyzes the given formula and sets an expression for the states states of the model that can be diff --git a/src/storm/logic/LiftableTransitionRewardsVisitor.cpp b/src/storm/logic/LiftableTransitionRewardsVisitor.cpp new file mode 100644 index 000000000..5be907ad9 --- /dev/null +++ b/src/storm/logic/LiftableTransitionRewardsVisitor.cpp @@ -0,0 +1,133 @@ +#include "storm/logic/LiftableTransitionRewardsVisitor.h" + +#include "storm/logic/Formulas.h" +#include "storm/storage/jani/traverser/RewardModelInformation.h" + +namespace storm { + namespace logic { + + LiftableTransitionRewardsVisitor::LiftableTransitionRewardsVisitor(storm::storage::SymbolicModelDescription const& symbolicModelDescription) : symbolicModelDescription(symbolicModelDescription) { + // Intentionally left empty. + } + + bool LiftableTransitionRewardsVisitor::areTransitionRewardsLiftable(Formula const& f) const { + return boost::any_cast(f.accept(*this, boost::any())); + } + + boost::any LiftableTransitionRewardsVisitor::visit(AtomicExpressionFormula const&, boost::any const&) const { + return true; + } + + boost::any LiftableTransitionRewardsVisitor::visit(AtomicLabelFormula const&, boost::any const&) const { + return true; + } + + boost::any LiftableTransitionRewardsVisitor::visit(BinaryBooleanStateFormula const&, boost::any const&) const { + return true; + } + + boost::any LiftableTransitionRewardsVisitor::visit(BooleanLiteralFormula const&, boost::any const&) const { + return true; + } + + boost::any LiftableTransitionRewardsVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const { + for (unsigned i = 0; i < f.getDimension(); ++i) { + if (f.getTimeBoundReference(i).isRewardBound() && rewardModelHasTransitionRewards(f.getTimeBoundReference(i).getRewardName())) { + return false; + } + } + + bool result = true; + if (f.hasMultiDimensionalSubformulas()) { + for (unsigned i = 0; i < f.getDimension(); ++i) { + result = result && boost::any_cast(f.getLeftSubformula(i).accept(*this, data)); + result = result && boost::any_cast(f.getRightSubformula(i).accept(*this, data)); + } + } else { + result = result && boost::any_cast(f.getLeftSubformula().accept(*this, data)); + result = result && boost::any_cast(f.getRightSubformula().accept(*this, data)); + } + return result; + } + + boost::any LiftableTransitionRewardsVisitor::visit(ConditionalFormula const& f, boost::any const& data) const { + return !f.isConditionalRewardFormula() && boost::any_cast(f.getSubformula().accept(*this, data)) && boost::any_cast(f.getConditionFormula().accept(*this, data)); + } + + boost::any LiftableTransitionRewardsVisitor::visit(CumulativeRewardFormula const& f, boost::any const&) const { + for (unsigned i = 0; i < f.getDimension(); ++i) { + if (f.getTimeBoundReference(i).isRewardBound() && rewardModelHasTransitionRewards(f.getTimeBoundReference(i).getRewardName())) { + return false; + } + } + return true; + } + + boost::any LiftableTransitionRewardsVisitor::visit(EventuallyFormula const& f, boost::any const& data) const { + return f.getSubformula().accept(*this, data); + } + + boost::any LiftableTransitionRewardsVisitor::visit(TimeOperatorFormula const& f, boost::any const& data) const { + return f.getSubformula().accept(*this, data); + } + + boost::any LiftableTransitionRewardsVisitor::visit(GloballyFormula const& f, boost::any const& data) const { + return f.getSubformula().accept(*this, data); + } + + boost::any LiftableTransitionRewardsVisitor::visit(InstantaneousRewardFormula const&, boost::any const&) const { + return true; + } + + boost::any LiftableTransitionRewardsVisitor::visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const { + return f.getSubformula().accept(*this, data); + } + + boost::any LiftableTransitionRewardsVisitor::visit(LongRunAverageRewardFormula const&, boost::any const&) const { + return true; + } + + boost::any LiftableTransitionRewardsVisitor::visit(MultiObjectiveFormula const& f, boost::any const& data) const { + bool result = true; + for (auto const& subF : f.getSubformulas()){ + result = result && boost::any_cast(subF->accept(*this, data)); + } + return result; + } + + boost::any LiftableTransitionRewardsVisitor::visit(NextFormula const& f, boost::any const& data) const { + return boost::any_cast(f.getSubformula().accept(*this, data)); + } + + boost::any LiftableTransitionRewardsVisitor::visit(ProbabilityOperatorFormula const& f, boost::any const& data) const { + return f.getSubformula().accept(*this, data); + } + + boost::any LiftableTransitionRewardsVisitor::visit(RewardOperatorFormula const& f, boost::any const& data) const { + return boost::any_cast(f.getSubformula().accept(*this, data)); + } + + boost::any LiftableTransitionRewardsVisitor::visit(TotalRewardFormula const&, boost::any const&) const { + return true; + } + + boost::any LiftableTransitionRewardsVisitor::visit(UnaryBooleanStateFormula const& f, boost::any const& data) const { + return f.getSubformula().accept(*this, data); + } + + boost::any LiftableTransitionRewardsVisitor::visit(UntilFormula const& f, boost::any const& data) const { + return boost::any_cast(f.getLeftSubformula().accept(*this, data)) && boost::any_cast(f.getRightSubformula().accept(*this)); + } + + bool LiftableTransitionRewardsVisitor::rewardModelHasTransitionRewards(std::string const& rewardModelName) const { + if (symbolicModelDescription.isJaniModel()) { + return storm::jani::RewardModelInformation(symbolicModelDescription.asJaniModel(), rewardModelName).hasTransitionRewards(); + } else if (symbolicModelDescription.isPrismProgram()) { + return symbolicModelDescription.asPrismProgram().getRewardModel(rewardModelName).hasTransitionRewards(); + } else { + // No model given + return false; + } + } + } +} diff --git a/src/storm/logic/LiftableTransitionRewardsVisitor.h b/src/storm/logic/LiftableTransitionRewardsVisitor.h new file mode 100644 index 000000000..9147ea3c7 --- /dev/null +++ b/src/storm/logic/LiftableTransitionRewardsVisitor.h @@ -0,0 +1,48 @@ +#pragma once + +#include "storm/logic/FormulaVisitor.h" +#include "storm/logic/FormulaInformation.h" +#include "storm/storage/SymbolicModelDescription.h" + +namespace storm { + + namespace logic { + + class LiftableTransitionRewardsVisitor : public FormulaVisitor { + public: + + LiftableTransitionRewardsVisitor(storm::storage::SymbolicModelDescription const& symbolicModelDescription = storm::storage::SymbolicModelDescription()); + + /*! + * Returns true, when lifting transition rewards to action rewards (by scaling with the transition probability) preserves the given formula + */ + bool areTransitionRewardsLiftable(Formula const& f) const; + + virtual boost::any visit(AtomicExpressionFormula const& f, boost::any const& data) const override; + virtual boost::any visit(AtomicLabelFormula const& f, boost::any const& data) const override; + virtual boost::any visit(BinaryBooleanStateFormula const& f, boost::any const& data) const override; + virtual boost::any visit(BooleanLiteralFormula const& f, boost::any const& data) const override; + virtual boost::any visit(BoundedUntilFormula const& f, boost::any const& data) const override; + virtual boost::any visit(ConditionalFormula const& f, boost::any const& data) const override; + virtual boost::any visit(CumulativeRewardFormula const& f, boost::any const& data) const override; + virtual boost::any visit(EventuallyFormula const& f, boost::any const& data) const override; + virtual boost::any visit(TimeOperatorFormula const& f, boost::any const& data) const override; + virtual boost::any visit(GloballyFormula const& f, boost::any const& data) const override; + virtual boost::any visit(InstantaneousRewardFormula const& f, boost::any const& data) const override; + virtual boost::any visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const override; + virtual boost::any visit(LongRunAverageRewardFormula const& f, boost::any const& data) const override; + virtual boost::any visit(MultiObjectiveFormula const& f, boost::any const& data) const override; + virtual boost::any visit(NextFormula const& f, boost::any const& data) const override; + virtual boost::any visit(ProbabilityOperatorFormula const& f, boost::any const& data) const override; + virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const override; + virtual boost::any visit(TotalRewardFormula const& f, boost::any const& data) const override; + virtual boost::any visit(UnaryBooleanStateFormula const& f, boost::any const& data) const override; + virtual boost::any visit(UntilFormula const& f, boost::any const& data) const override; + + private: + storm::storage::SymbolicModelDescription const& symbolicModelDescription; + bool rewardModelHasTransitionRewards(std::string const& rewardModelName) const; + }; + + } +}