diff --git a/src/storm/logic/BoundedUntilFormula.cpp b/src/storm/logic/BoundedUntilFormula.cpp index 8ef7be0a9..e07d05b55 100644 --- a/src/storm/logic/BoundedUntilFormula.cpp +++ b/src/storm/logic/BoundedUntilFormula.cpp @@ -278,14 +278,19 @@ namespace storm { out << " U"; if (this->isMultiDimensional()) { - out << "["; + out << "^{"; } - for(unsigned i = 0; i < this->getDimension(); ++i) { + for (unsigned i = 0; i < this->getDimension(); ++i) { if (i > 0) { out << ","; } if (this->getTimeBoundReference(i).isRewardBound()) { - out << "{\"" << this->getTimeBoundReference(i).getRewardName() << "\"}"; + out << "rew{\"" << this->getTimeBoundReference(i).getRewardName() << "\"}"; + } else if (this->getTimeBoundReference(i).isStepBound()) { + out << "steps"; + //} else if (this->getTimeBoundReference(i).isStepBound()) + // Note: the 'time' keyword is optional. + // out << "time"; } if (this->hasLowerBound(i)) { if (this->hasUpperBound(i)) { @@ -321,7 +326,7 @@ namespace storm { out << " "; } if (this->isMultiDimensional()) { - out << "]"; + out << "}"; } this->getRightSubformula().writeToStream(out); diff --git a/src/storm/logic/CumulativeRewardFormula.cpp b/src/storm/logic/CumulativeRewardFormula.cpp index cae9590a6..dd0eeb994 100644 --- a/src/storm/logic/CumulativeRewardFormula.cpp +++ b/src/storm/logic/CumulativeRewardFormula.cpp @@ -9,10 +9,16 @@ namespace storm { namespace logic { - CumulativeRewardFormula::CumulativeRewardFormula(TimeBound const& bound, TimeBoundReference const& timeBoundReference) : timeBoundReference(timeBoundReference), bound(bound) { + CumulativeRewardFormula::CumulativeRewardFormula(TimeBound const& bound, TimeBoundReference const& timeBoundReference) : timeBoundReferences({timeBoundReference}), bounds({bound}) { // Intentionally left empty. } + CumulativeRewardFormula::CumulativeRewardFormula(std::vector const& bounds, std::vector const& timeBoundReferences) : timeBoundReferences(timeBoundReferences), bounds(bounds) { + + STORM_LOG_ASSERT(this->timeBoundReferences.size() == this->bounds.size(), "Number of time bounds and number of time bound references does not match."); + STORM_LOG_ASSERT(!this->timeBoundReferences.empty(), "No time bounds given."); + } + bool CumulativeRewardFormula::isCumulativeRewardFormula() const { return true; } @@ -21,74 +27,95 @@ namespace storm { return true; } + bool CumulativeRewardFormula::isMultiDimensional() const { + return getDimension() > 1; + } + + unsigned CumulativeRewardFormula::getDimension() const { + return timeBoundReferences.size(); + } + boost::any CumulativeRewardFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const { return visitor.visit(*this, data); } void CumulativeRewardFormula::gatherReferencedRewardModels(std::set& referencedRewardModels) const { - if (this->isRewardBounded()) { - referencedRewardModels.insert(this->getTimeBoundReference().getRewardName()); + for (unsigned i = 0; i < this->getDimension(); ++i) { + if (getTimeBoundReference(i).isRewardBound()) { + referencedRewardModels.insert(this->getTimeBoundReference(i).getRewardName()); + } } } - TimeBoundType CumulativeRewardFormula::getTimeBoundType() const { - return timeBoundReference.getType(); - } - TimeBoundReference const& CumulativeRewardFormula::getTimeBoundReference() const { - return timeBoundReference; + STORM_LOG_ASSERT(!isMultiDimensional(), "Cumulative Reward Formula is multi-dimensional."); + return getTimeBoundReference(0); } - bool CumulativeRewardFormula::isStepBounded() const { - return getTimeBoundType() == TimeBoundType::Steps; + TimeBoundReference const& CumulativeRewardFormula::getTimeBoundReference(unsigned i) const { + return timeBoundReferences.at(i); } - - bool CumulativeRewardFormula::isTimeBounded() const { - return getTimeBoundType() == TimeBoundType::Time; + + bool CumulativeRewardFormula::isBoundStrict() const { + STORM_LOG_ASSERT(!isMultiDimensional(), "Cumulative Reward Formula is multi-dimensional."); + return isBoundStrict(0); } - bool CumulativeRewardFormula::isRewardBounded() const { - return getTimeBoundType() == TimeBoundType::Reward; + bool CumulativeRewardFormula::isBoundStrict(unsigned i) const { + return bounds.at(i).isStrict(); } - bool CumulativeRewardFormula::isBoundStrict() const { - return bound.isStrict(); + bool CumulativeRewardFormula::hasIntegerBound() const { + STORM_LOG_ASSERT(!isMultiDimensional(), "Cumulative Reward Formula is multi-dimensional."); + return hasIntegerBound(0); } - bool CumulativeRewardFormula::hasIntegerBound() const { - return bound.getBound().hasIntegerType(); + bool CumulativeRewardFormula::hasIntegerBound(unsigned i) const { + return bounds.at(i).getBound().hasIntegerType(); } storm::expressions::Expression const& CumulativeRewardFormula::getBound() const { - return bound.getBound(); + STORM_LOG_ASSERT(!isMultiDimensional(), "Cumulative Reward Formula is multi-dimensional."); + return getBound(0); + } + + storm::expressions::Expression const& CumulativeRewardFormula::getBound(unsigned i) const { + return bounds.at(i).getBound(); + } + + template + ValueType CumulativeRewardFormula::getBound() const { + STORM_LOG_ASSERT(!isMultiDimensional(), "Cumulative Reward Formula is multi-dimensional."); + return getBound(0); } template <> - double CumulativeRewardFormula::getBound() const { - checkNoVariablesInBound(bound.getBound()); - double value = bound.getBound().evaluateAsDouble(); - STORM_LOG_THROW(value >= 0, storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number."); + double CumulativeRewardFormula::getBound(unsigned i) const { + checkNoVariablesInBound(bounds.at(i).getBound()); + double value = bounds.at(i).getBound().evaluateAsDouble(); + STORM_LOG_THROW(value >= 0.0, storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number."); return value; } template <> - storm::RationalNumber CumulativeRewardFormula::getBound() const { - checkNoVariablesInBound(bound.getBound()); - storm::RationalNumber value = bound.getBound().evaluateAsRational(); + storm::RationalNumber CumulativeRewardFormula::getBound(unsigned i) const { + checkNoVariablesInBound(bounds.at(i).getBound()); + storm::RationalNumber value = bounds.at(i).getBound().evaluateAsRational(); STORM_LOG_THROW(value >= storm::utility::zero(), storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number."); return value; } template <> - uint64_t CumulativeRewardFormula::getBound() const { - checkNoVariablesInBound(bound.getBound()); - uint64_t value = bound.getBound().evaluateAsInt(); + uint64_t CumulativeRewardFormula::getBound(unsigned i) const { + checkNoVariablesInBound(bounds.at(i).getBound()); + uint64_t value = bounds.at(i).getBound().evaluateAsInt(); STORM_LOG_THROW(value >= 0, storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number."); return value; } template <> double CumulativeRewardFormula::getNonStrictBound() const { + STORM_LOG_ASSERT(!isMultiDimensional(), "Cumulative Reward Formula is multi-dimensional."); double bound = getBound(); STORM_LOG_THROW(bound > 0, storm::exceptions::InvalidPropertyException, "Cannot retrieve non-strict bound from strict zero-bound."); return bound; @@ -96,6 +123,7 @@ namespace storm { template <> uint64_t CumulativeRewardFormula::getNonStrictBound() const { + STORM_LOG_ASSERT(!isMultiDimensional(), "Cumulative Reward Formula is multi-dimensional."); int_fast64_t bound = getBound(); if (isBoundStrict()) { STORM_LOG_THROW(bound > 0, storm::exceptions::InvalidPropertyException, "Cannot retrieve non-strict bound from strict zero-bound."); @@ -109,13 +137,43 @@ namespace storm { STORM_LOG_THROW(!bound.containsVariables(), storm::exceptions::InvalidOperationException, "Cannot evaluate time-bound '" << bound << "' as it contains undefined constants."); } + std::shared_ptr CumulativeRewardFormula::restrictToDimension(unsigned i) const { + return std::make_shared(bounds.at(i), getTimeBoundReference(i)); + } + std::ostream& CumulativeRewardFormula::writeToStream(std::ostream& out) const { out << "C"; - if(getTimeBoundReference().isRewardBound()) { - out << "{\"" << getTimeBoundReference().getRewardName() << "\"}"; - } - out << "<=" << this->getBound(); + if (this->isMultiDimensional()) { + out << "^{"; + } + for (unsigned i = 0; i < this->getDimension(); ++i) { + if (i > 0) { + out << ","; + } + if (this->getTimeBoundReference(i).isRewardBound()) { + out << "rew{\"" << this->getTimeBoundReference(i).getRewardName() << "\"}"; + } else if (this->getTimeBoundReference(i).isStepBound()) { + out << "steps"; + //} else if (this->getTimeBoundReference(i).isStepBound()) + // Note: the 'time' keyword is optional. + // out << "time"; + } + if (this->isBoundStrict(i)) { + out << "<"; + } else { + out << "<="; + } + out << this->getBound(i); + } + if (this->isMultiDimensional()) { + out << "}"; + } return out; } + + template uint64_t CumulativeRewardFormula::getBound() const; + template double CumulativeRewardFormula::getBound() const; + template storm::RationalNumber CumulativeRewardFormula::getBound() const; + } } diff --git a/src/storm/logic/CumulativeRewardFormula.h b/src/storm/logic/CumulativeRewardFormula.h index e7f5a60c1..e40370b07 100644 --- a/src/storm/logic/CumulativeRewardFormula.h +++ b/src/storm/logic/CumulativeRewardFormula.h @@ -11,43 +11,49 @@ namespace storm { class CumulativeRewardFormula : public PathFormula { public: CumulativeRewardFormula(TimeBound const& bound, TimeBoundReference const& timeBoundReference = TimeBoundReference(TimeBoundType::Time)); + CumulativeRewardFormula(std::vector const& bounds, std::vector const& timeBoundReferences); - virtual ~CumulativeRewardFormula() { - // Intentionally left empty. - } + virtual ~CumulativeRewardFormula() = default; virtual bool isCumulativeRewardFormula() const override; virtual bool isRewardPathFormula() const override; + bool isMultiDimensional() const; + unsigned getDimension() const; + virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override; virtual void gatherReferencedRewardModels(std::set& referencedRewardModels) const override; virtual std::ostream& writeToStream(std::ostream& out) const override; - TimeBoundType getTimeBoundType() const; TimeBoundReference const& getTimeBoundReference() const; - - bool isStepBounded() const; - bool isTimeBounded() const; - bool isRewardBounded() const; + TimeBoundReference const& getTimeBoundReference(unsigned i) const; bool isBoundStrict() const; + bool isBoundStrict(unsigned i) const; bool hasIntegerBound() const; + bool hasIntegerBound(unsigned i) const; storm::expressions::Expression const& getBound() const; + storm::expressions::Expression const& getBound(unsigned i) const; template ValueType getBound() const; + template + ValueType getBound(unsigned i) const; + template ValueType getNonStrictBound() const; + std::shared_ptr restrictToDimension(unsigned i) const; + private: static void checkNoVariablesInBound(storm::expressions::Expression const& bound); - TimeBoundReference timeBoundReference; - TimeBound bound; + std::vector timeBoundReferences; + std::vector bounds; }; } } diff --git a/src/storm/logic/FormulaInformationVisitor.cpp b/src/storm/logic/FormulaInformationVisitor.cpp index 8c25686a9..0aab5e04e 100644 --- a/src/storm/logic/FormulaInformationVisitor.cpp +++ b/src/storm/logic/FormulaInformationVisitor.cpp @@ -28,18 +28,18 @@ namespace storm { boost::any FormulaInformationVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const { FormulaInformation result; result.setContainsBoundedUntilFormula(true); + for (unsigned i = 0; i < f.getDimension(); ++i) { + if (f.getTimeBoundReference(i).isRewardBound()) { + result.setContainsRewardBoundedFormula(true); + } + } + if (f.hasMultiDimensionalSubformulas()) { - for (unsigned i = 0; i < f.getDimension(); ++i){ - if (f.getTimeBoundReference(i).isRewardBound()) { - result.setContainsRewardBoundedFormula(true); - } + for (unsigned i = 0; i < f.getDimension(); ++i) { result.join(boost::any_cast(f.getLeftSubformula(i).accept(*this, data))); result.join(boost::any_cast(f.getRightSubformula(i).accept(*this, data))); } } else { - if (f.getTimeBoundReference().isRewardBound()) { - result.setContainsRewardBoundedFormula(true); - } result.join(boost::any_cast(f.getLeftSubformula().accept(*this, data))); result.join(boost::any_cast(f.getRightSubformula().accept(*this, data))); } @@ -53,8 +53,10 @@ namespace storm { boost::any FormulaInformationVisitor::visit(CumulativeRewardFormula const& f, boost::any const&) const { FormulaInformation result; result.setContainsCumulativeRewardFormula(true); - if (f.getTimeBoundReference().isRewardBound()) { - result.setContainsRewardBoundedFormula(true); + for (unsigned i = 0; i < f.getDimension(); ++i) { + if (f.getTimeBoundReference(i).isRewardBound()) { + result.setContainsRewardBoundedFormula(true); + } } return result; } diff --git a/src/storm/logic/FragmentChecker.cpp b/src/storm/logic/FragmentChecker.cpp index 53f707aa3..24ad016c8 100644 --- a/src/storm/logic/FragmentChecker.cpp +++ b/src/storm/logic/FragmentChecker.cpp @@ -117,14 +117,17 @@ namespace storm { InheritedInformation const& inherited = boost::any_cast(data); bool result = inherited.getSpecification().areCumulativeRewardFormulasAllowed(); - auto const& tbr = f.getTimeBoundReference(); - if (tbr.isStepBound()) { - result = result && inherited.getSpecification().areStepBoundedCumulativeRewardFormulasAllowed(); - } else if(tbr.isTimeBound()) { - result = result && inherited.getSpecification().areTimeBoundedCumulativeRewardFormulasAllowed(); - } else { - assert(tbr.isRewardBound()); - result = result && inherited.getSpecification().areRewardBoundedCumulativeRewardFormulasAllowed(); + result = result && (!f.isMultiDimensional() || inherited.getSpecification().areMultiDimensionalCumulativeRewardFormulasAllowed()); + for (uint64_t i = 0; i < f.getDimension(); ++i) { + auto tbr = f.getTimeBoundReference(i); + if (tbr.isStepBound()) { + result = result && inherited.getSpecification().areStepBoundedCumulativeRewardFormulasAllowed(); + } else if(tbr.isTimeBound()) { + result = result && inherited.getSpecification().areTimeBoundedCumulativeRewardFormulasAllowed(); + } else { + assert(tbr.isRewardBound()); + result = result && inherited.getSpecification().areRewardBoundedCumulativeRewardFormulasAllowed(); + } } return result; } diff --git a/src/storm/logic/FragmentSpecification.cpp b/src/storm/logic/FragmentSpecification.cpp index b08c0d927..cdcfc6ecd 100644 --- a/src/storm/logic/FragmentSpecification.cpp +++ b/src/storm/logic/FragmentSpecification.cpp @@ -152,6 +152,7 @@ namespace storm { stepBoundedCumulativeRewardFormulas = false; timeBoundedCumulativeRewardFormulas = false; rewardBoundedCumulativeRewardFormulas = false; + multiDimensionalCumulativeRewardFormulas = false; varianceAsMeasureType = false; qualitativeOperatorResults = true; @@ -481,6 +482,15 @@ namespace storm { return *this; } + bool FragmentSpecification::areMultiDimensionalCumulativeRewardFormulasAllowed() const { + return this->multiDimensionalCumulativeRewardFormulas; + } + + FragmentSpecification& FragmentSpecification::setMultiDimensionalCumulativeRewardFormulasAllowed(bool newValue) { + this->multiDimensionalCumulativeRewardFormulas = newValue; + return *this; + } + FragmentSpecification& FragmentSpecification::setOperatorsAllowed(bool newValue) { this->setProbabilityOperatorsAllowed(newValue); this->setRewardOperatorsAllowed(newValue); diff --git a/src/storm/logic/FragmentSpecification.h b/src/storm/logic/FragmentSpecification.h index fbd3434e9..d90ebd5fb 100644 --- a/src/storm/logic/FragmentSpecification.h +++ b/src/storm/logic/FragmentSpecification.h @@ -106,6 +106,9 @@ namespace storm { bool areRewardBoundedUntilFormulasAllowed() const; FragmentSpecification& setRewardBoundedUntilFormulasAllowed(bool newValue); + bool areMultiDimensionalBoundedUntilFormulasAllowed() const; + FragmentSpecification& setMultiDimensionalBoundedUntilFormulasAllowed(bool newValue); + bool areStepBoundedCumulativeRewardFormulasAllowed() const; FragmentSpecification& setStepBoundedCumulativeRewardFormulasAllowed(bool newValue); @@ -115,8 +118,8 @@ namespace storm { bool areRewardBoundedCumulativeRewardFormulasAllowed() const; FragmentSpecification& setRewardBoundedCumulativeRewardFormulasAllowed(bool newValue); - bool areMultiDimensionalBoundedUntilFormulasAllowed() const; - FragmentSpecification& setMultiDimensionalBoundedUntilFormulasAllowed(bool newValue); + bool areMultiDimensionalCumulativeRewardFormulasAllowed() const; + FragmentSpecification& setMultiDimensionalCumulativeRewardFormulasAllowed(bool newValue); bool isVarianceMeasureTypeAllowed() const; FragmentSpecification& setVarianceMeasureTypeAllowed(bool newValue); @@ -181,10 +184,11 @@ namespace storm { bool stepBoundedUntilFormulas; bool timeBoundedUntilFormulas; bool rewardBoundedUntilFormulas; + bool multiDimensionalBoundedUntilFormulas; bool stepBoundedCumulativeRewardFormulas; bool timeBoundedCumulativeRewardFormulas; bool rewardBoundedCumulativeRewardFormulas; - bool multiDimensionalBoundedUntilFormulas; + bool multiDimensionalCumulativeRewardFormulas; bool varianceAsMeasureType; bool quantitativeOperatorResults; bool qualitativeOperatorResults; diff --git a/src/storm/logic/VariableSubstitutionVisitor.cpp b/src/storm/logic/VariableSubstitutionVisitor.cpp index 47be93b36..7fae8498c 100644 --- a/src/storm/logic/VariableSubstitutionVisitor.cpp +++ b/src/storm/logic/VariableSubstitutionVisitor.cpp @@ -65,7 +65,13 @@ namespace storm { } boost::any VariableSubstitutionVisitor::visit(CumulativeRewardFormula const& f, boost::any const&) const { - return std::static_pointer_cast(std::make_shared(storm::logic::TimeBound(f.isBoundStrict(), f.getBound().substitute(substitution)), f.getTimeBoundReference())); + std::vector bounds; + std::vector timeBoundReferences; + for (uint64_t i = 0; i < f.getDimension(); ++i) { + bounds.emplace_back(TimeBound(f.isBoundStrict(i), f.getBound(i).substitute(substitution))); + timeBoundReferences.push_back(f.getTimeBoundReference(i)); + } + return std::static_pointer_cast(std::make_shared(bounds, timeBoundReferences)); } boost::any VariableSubstitutionVisitor::visit(InstantaneousRewardFormula const& f, boost::any const&) const { diff --git a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp index 5519e5b55..3972f3728 100644 --- a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp +++ b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp @@ -352,13 +352,18 @@ namespace storm { void SparseMultiObjectivePreprocessor::preprocessCumulativeRewardFormula(storm::logic::CumulativeRewardFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data, boost::optional const& optionalRewardModelName) { STORM_LOG_THROW(data.originalModel.isOfType(storm::models::ModelType::Mdp), storm::exceptions::InvalidPropertyException, "Cumulative reward formulas are not supported for the given model type."); - storm::logic::TimeBound bound(formula.isBoundStrict(), formula.getBound()); - storm::logic::TimeBoundReference tbr(formula.getTimeBoundReference()); - auto cumulativeRewardFormula = std::make_shared(bound, tbr); + auto cumulativeRewardFormula = std::make_shared(formula); data.objectives.back()->formula = std::make_shared(cumulativeRewardFormula, *optionalRewardModelName, opInfo); - data.upperResultBoundObjectives.set(data.objectives.size() - 1, true); - if (tbr.isRewardBound()) { + bool onlyRewardBounds = true; + for (uint64_t i = 0; i < cumulativeRewardFormula->getDimension(); ++i) { + if (!cumulativeRewardFormula->getTimeBoundReference(i).isRewardBound()) { + onlyRewardBounds = false; + break; + } + } + if (onlyRewardBounds) { data.finiteRewardCheckObjectives.set(data.objectives.size() - 1, true); + data.upperResultBoundObjectives.set(data.objectives.size() - 1, true); } } @@ -513,7 +518,6 @@ namespace storm { } else { result.rewardLessInfinityEStates = allStates; } - } template diff --git a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorResult.h b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorResult.h index fee7adf5f..6c8a43390 100644 --- a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorResult.h +++ b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorResult.h @@ -50,10 +50,19 @@ namespace storm { } bool containsOnlyTrivialObjectives() const { + // Trivial objectives are either total reward formulas or single-dimensional step or time bounded cumulative reward formulas for (auto const& obj : objectives) { - if (!(obj.formula->isRewardOperatorFormula() && (obj.formula->getSubformula().isTotalRewardFormula() || (obj.formula->getSubformula().isCumulativeRewardFormula() && !obj.formula->getSubformula().asCumulativeRewardFormula().getTimeBoundReference().isRewardBound())))) { - return false; + if (obj.formula->isRewardOperatorFormula() && obj.formula->getSubformula().isTotalRewardFormula()) { + continue; } + if (obj.formula->isRewardOperatorFormula() && obj.formula->getSubformula().isCumulativeRewardFormula()) { + auto const& subf = obj.formula->getSubformula().asCumulativeRewardFormula(); + if (!subf.isMultiDimensional() && (subf.getTimeBoundReference().isTimeBound() || subf.getTimeBoundReference().isStepBound())) { + continue; + } + } + // Reaching this point means that the objective is considered as non-trivial + return false; } return true; } diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp index 3fedd3bac..8597fdc42 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp @@ -48,7 +48,7 @@ namespace storm { } } } else { - STORM_LOG_THROW(formula.getSubformula().isCumulativeRewardFormula() && formula.getSubformula().asCumulativeRewardFormula().isTimeBounded(), storm::exceptions::UnexpectedException, "Unexpected type of sub-formula: " << formula.getSubformula()); + STORM_LOG_THROW(formula.getSubformula().isCumulativeRewardFormula() && formula.getSubformula().asCumulativeRewardFormula().getTimeBoundReference().isTimeBound(), storm::exceptions::UnexpectedException, "Unexpected type of sub-formula: " << formula.getSubformula()); STORM_LOG_THROW(!rewModel.hasStateRewards(), storm::exceptions::InvalidPropertyException, "Found state rewards for time bounded objective " << this->objectives[objIndex].originalFormula << ". This is not supported."); STORM_LOG_WARN_COND(this->objectives[objIndex].originalFormula->isProbabilityOperatorFormula() && this->objectives[objIndex].originalFormula->asProbabilityOperatorFormula().getSubformula().isBoundedUntilFormula(), "Objective " << this->objectives[objIndex].originalFormula << " was simplified to a cumulative reward formula. Correctness of the algorithm is unknown for this type of property."); } diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/ProductModel.cpp b/src/storm/modelchecker/multiobjective/rewardbounded/ProductModel.cpp index bd545c124..e3cacb0fe 100644 --- a/src/storm/modelchecker/multiobjective/rewardbounded/ProductModel.cpp +++ b/src/storm/modelchecker/multiobjective/rewardbounded/ProductModel.cpp @@ -406,8 +406,12 @@ namespace storm { STORM_LOG_THROW(!rewModel.hasTransitionRewards(), storm::exceptions::NotSupportedException, "Reward model has transition rewards which is not expected."); bool rewardCollectedInEpoch = true; if (formula.getSubformula().isCumulativeRewardFormula()) { - assert(objectiveDimensions[objIndex].getNumberOfSetBits() == 1); - rewardCollectedInEpoch = !epochManager.isBottomDimensionEpochClass(epochClass, *objectiveDimensions[objIndex].begin()); + for (auto const& dim : objectiveDimensions[objIndex]) { + if (epochManager.isBottomDimensionEpochClass(epochClass, dim)) { + rewardCollectedInEpoch = false; + break; + } + } } else { STORM_LOG_THROW(formula.getSubformula().isTotalRewardFormula(), storm::exceptions::UnexpectedException, "Unexpected type of formula " << formula); } diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index bd1ef4f4b..8d7fc1b8c 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -43,14 +43,14 @@ namespace storm { template bool SparseMdpPrctlModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - if(formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true).setRewardBoundedCumulativeRewardFormulasAllowed(true).setMultiDimensionalBoundedUntilFormulasAllowed(true))) { + if(formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true).setRewardBoundedCumulativeRewardFormulasAllowed(true).setMultiDimensionalBoundedUntilFormulasAllowed(true).setMultiDimensionalCumulativeRewardFormulasAllowed(true))) { return true; } else { // Check whether we consider a multi-objective formula // For multi-objective model checking, each initial state requires an individual scheduler (in contrast to single-objective model checking). Let's exclude multiple initial states. if (this->getModel().getInitialStates().getNumberOfSetBits() > 1) return false; if (!checkTask.isOnlyInitialStatesRelevantSet()) return false; - return formula.isInFragment(storm::logic::multiObjective().setCumulativeRewardFormulasAllowed(true).setTimeBoundedCumulativeRewardFormulasAllowed(true).setStepBoundedCumulativeRewardFormulasAllowed(true).setRewardBoundedCumulativeRewardFormulasAllowed(true).setTimeBoundedUntilFormulasAllowed(true).setStepBoundedUntilFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true).setMultiDimensionalBoundedUntilFormulasAllowed(true)); + return formula.isInFragment(storm::logic::multiObjective().setCumulativeRewardFormulasAllowed(true).setTimeBoundedCumulativeRewardFormulasAllowed(true).setStepBoundedCumulativeRewardFormulasAllowed(true).setRewardBoundedCumulativeRewardFormulasAllowed(true).setTimeBoundedUntilFormulasAllowed(true).setStepBoundedUntilFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true).setMultiDimensionalBoundedUntilFormulasAllowed(true).setMultiDimensionalCumulativeRewardFormulasAllowed(true)); } } diff --git a/src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.cpp b/src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.cpp index 93a9afd02..ec599fd37 100644 --- a/src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.cpp +++ b/src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.cpp @@ -108,25 +108,27 @@ namespace storm { } } else if (formula.isRewardOperatorFormula() && formula.getSubformula().isCumulativeRewardFormula()) { auto const& subformula = formula.getSubformula().asCumulativeRewardFormula(); - Dimension dimension; - dimension.formula = formula.getSubformula().asSharedPointer(); - dimension.objectiveIndex = objIndex; - dimension.isUpperBounded = true; - if (subformula.getTimeBoundReference().isTimeBound() || subformula.getTimeBoundReference().isStepBound()) { - dimensionWiseEpochSteps.push_back(std::vector(model.getNumberOfChoices(), 1)); - dimension.scalingFactor = storm::utility::one(); - } else { - STORM_LOG_ASSERT(subformula.getTimeBoundReference().isRewardBound(), "Unexpected type of time bound."); - std::string const& rewardName = subformula.getTimeBoundReference().getRewardName(); - STORM_LOG_THROW(this->model.hasRewardModel(rewardName), storm::exceptions::IllegalArgumentException, "No reward model with name '" << rewardName << "' found."); - auto const& rewardModel = this->model.getRewardModel(rewardName); - STORM_LOG_THROW(!rewardModel.hasTransitionRewards(), storm::exceptions::NotSupportedException, "Transition rewards are currently not supported as reward bounds."); - std::vector actionRewards = rewardModel.getTotalRewardVector(this->model.getTransitionMatrix()); - auto discretizedRewardsAndFactor = storm::utility::vector::toIntegralVector(actionRewards); - dimensionWiseEpochSteps.push_back(std::move(discretizedRewardsAndFactor.first)); - dimension.scalingFactor = std::move(discretizedRewardsAndFactor.second); + for (uint64_t dim = 0; dim < subformula.getDimension(); ++dim) { + Dimension dimension; + dimension.formula = subformula.restrictToDimension(dim); + dimension.objectiveIndex = objIndex; + dimension.isUpperBounded = true; + if (subformula.getTimeBoundReference(dim).isTimeBound() || subformula.getTimeBoundReference(dim).isStepBound()) { + dimensionWiseEpochSteps.push_back(std::vector(model.getNumberOfChoices(), 1)); + dimension.scalingFactor = storm::utility::one(); + } else { + STORM_LOG_ASSERT(subformula.getTimeBoundReference(dim).isRewardBound(), "Unexpected type of time bound."); + std::string const& rewardName = subformula.getTimeBoundReference(dim).getRewardName(); + STORM_LOG_THROW(this->model.hasRewardModel(rewardName), storm::exceptions::IllegalArgumentException, "No reward model with name '" << rewardName << "' found."); + auto const& rewardModel = this->model.getRewardModel(rewardName); + STORM_LOG_THROW(!rewardModel.hasTransitionRewards(), storm::exceptions::NotSupportedException, "Transition rewards are currently not supported as reward bounds."); + std::vector actionRewards = rewardModel.getTotalRewardVector(this->model.getTransitionMatrix()); + auto discretizedRewardsAndFactor = storm::utility::vector::toIntegralVector(actionRewards); + dimensionWiseEpochSteps.push_back(std::move(discretizedRewardsAndFactor.first)); + dimension.scalingFactor = std::move(discretizedRewardsAndFactor.second); + } + dimensions.emplace_back(std::move(dimension)); } - dimensions.emplace_back(std::move(dimension)); } } @@ -135,27 +137,26 @@ namespace storm { uint64_t dim = 0; for (uint64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { storm::storage::BitVector objDimensions(dimensions.size(), false); + uint64_t objDimensionCount = 0; + bool objDimensionsCanBeSatisfiedIndividually = false; if (objectives[objIndex].formula->isProbabilityOperatorFormula() && objectives[objIndex].formula->getSubformula().isBoundedUntilFormula()) { - auto const& boundedUntilFormula = objectives[objIndex].formula->getSubformula().asBoundedUntilFormula(); - for (uint64_t currDim = dim; currDim < dim + boundedUntilFormula.getDimension(); ++currDim ) { - objDimensions.set(currDim); - } - for (uint64_t currDim = dim; currDim < dim + boundedUntilFormula.getDimension(); ++currDim ) { - if (!boundedUntilFormula.hasMultiDimensionalSubformulas() || dimensions[currDim].isUpperBounded) { - dimensions[currDim].dependentDimensions = objDimensions; - } else { - dimensions[currDim].dependentDimensions = storm::storage::BitVector(dimensions.size(), false); - dimensions[currDim].dependentDimensions.set(currDim, true); - } - // std::cout << "dimension " << currDim << " has depDims: " << dimensions[currDim].dependentDimensions << std::endl; - } - dim += boundedUntilFormula.getDimension(); + objDimensionCount = objectives[objIndex].formula->getSubformula().asBoundedUntilFormula().getDimension(); + objDimensionsCanBeSatisfiedIndividually = objectives[objIndex].formula->getSubformula().asBoundedUntilFormula().hasMultiDimensionalSubformulas(); } else if (objectives[objIndex].formula->isRewardOperatorFormula() && objectives[objIndex].formula->getSubformula().isCumulativeRewardFormula()) { - objDimensions.set(dim, true); - dimensions[dim].dependentDimensions = objDimensions; - ++dim; + objDimensionCount = objectives[objIndex].formula->getSubformula().asCumulativeRewardFormula().getDimension(); } - + for (uint64_t currDim = dim; currDim < dim + objDimensionCount; ++currDim ) { + objDimensions.set(currDim); + } + for (uint64_t currDim = dim; currDim < dim + objDimensionCount; ++currDim ) { + if (!objDimensionsCanBeSatisfiedIndividually || dimensions[currDim].isUpperBounded) { + dimensions[currDim].dependentDimensions = objDimensions; + } else { + dimensions[currDim].dependentDimensions = storm::storage::BitVector(dimensions.size(), false); + dimensions[currDim].dependentDimensions.set(currDim, true); + } + } + dim += objDimensionCount; objectiveDimensions.push_back(std::move(objDimensions)); } assert(dim == dimensions.size()); @@ -210,6 +211,7 @@ namespace storm { isStrict = dimFormula.asBoundedUntilFormula().isLowerBoundStrict(); } } else if (dimFormula.isCumulativeRewardFormula()) { + assert(!dimFormula.asCumulativeRewardFormula().isMultiDimensional()); bound = dimFormula.asCumulativeRewardFormula().getBound(); isStrict = dimFormula.asCumulativeRewardFormula().isBoundStrict(); } @@ -562,29 +564,35 @@ namespace storm { if (objective.formula->getSubformula().isCumulativeRewardFormula()) { // Try to get an upper bound by computing the maximal reward achievable within one epoch step auto const& cumulativeRewardFormula = objective.formula->getSubformula().asCumulativeRewardFormula(); - ValueType rewardBound = cumulativeRewardFormula.template getBound(); - if (cumulativeRewardFormula.getTimeBoundReference().isRewardBound()) { - auto const& costModel = this->model.getRewardModel(cumulativeRewardFormula.getTimeBoundReference().getRewardName()); - if (!costModel.hasTransitionRewards()) { - auto actionCosts = costModel.getTotalRewardVector(this->model.getTransitionMatrix()); - ValueType largestRewardPerCost = storm::utility::zero(); - bool isFinite = true; - for (auto rewIt = actionRewards.begin(), costIt = actionCosts.begin(); rewIt != actionRewards.end(); ++rewIt, ++costIt) { - if (!storm::utility::isZero(*rewIt)) { - if (storm::utility::isZero(*costIt)) { - isFinite = false; - break; + for (uint64_t objDim = 0; objDim < cumulativeRewardFormula.getDimension(); ++objDim) { + boost::optional resBound; + ValueType rewardBound = cumulativeRewardFormula.template getBound(objDim); + if (cumulativeRewardFormula.getTimeBoundReference(objDim).isRewardBound()) { + auto const& costModel = this->model.getRewardModel(cumulativeRewardFormula.getTimeBoundReference(objDim).getRewardName()); + if (!costModel.hasTransitionRewards()) { + auto actionCosts = costModel.getTotalRewardVector(this->model.getTransitionMatrix()); + ValueType largestRewardPerCost = storm::utility::zero(); + bool isFinite = true; + for (auto rewIt = actionRewards.begin(), costIt = actionCosts.begin(); rewIt != actionRewards.end(); ++rewIt, ++costIt) { + if (!storm::utility::isZero(*rewIt)) { + if (storm::utility::isZero(*costIt)) { + isFinite = false; + break; + } + ValueType rewardPerCost = *rewIt / *costIt; + largestRewardPerCost = std::max(largestRewardPerCost, rewardPerCost); } - ValueType rewardPerCost = *rewIt / *costIt; - largestRewardPerCost = std::max(largestRewardPerCost, rewardPerCost); + } + if (isFinite) { + resBound = largestRewardPerCost * rewardBound; } } - if (isFinite) { - objective.upperResultBound = largestRewardPerCost * rewardBound; - } + } else { + resBound = (*std::max_element(actionRewards.begin(), actionRewards.end())) * rewardBound; + } + if (resBound && (!objective.upperResultBound || objective.upperResultBound.get() > resBound.get())) { + objective.upperResultBound = resBound; } - } else { - objective.upperResultBound = (*std::max_element(actionRewards.begin(), actionRewards.end())) * rewardBound; } // If we could not find an upper bound, try to get an upper bound for the unbounded case diff --git a/src/storm/parser/FormulaParserGrammar.cpp b/src/storm/parser/FormulaParserGrammar.cpp index 35fe2bc39..b37e1775c 100644 --- a/src/storm/parser/FormulaParserGrammar.cpp +++ b/src/storm/parser/FormulaParserGrammar.cpp @@ -259,7 +259,7 @@ namespace storm { bounds.push_back(std::get<1>(timeBound).get()); timeBoundReferences.emplace_back(*std::get<2>(timeBound)); } - return std::shared_ptr(new storm::logic::CumulativeRewardFormula(bounds.front(), timeBoundReferences.front())); + return std::shared_ptr(new storm::logic::CumulativeRewardFormula(bounds, timeBoundReferences)); } std::shared_ptr FormulaParserGrammar::createTotalRewardFormula() const { diff --git a/src/storm/parser/FormulaParserGrammar.h b/src/storm/parser/FormulaParserGrammar.h index d0046bbee..dd9a3a06f 100644 --- a/src/storm/parser/FormulaParserGrammar.h +++ b/src/storm/parser/FormulaParserGrammar.h @@ -183,6 +183,7 @@ namespace storm { qi::rule, Skipper> timeBoundReference; qi::rule, boost::optional, std::shared_ptr>(), qi::locals, Skipper> timeBound; + qi::rule, boost::optional, std::shared_ptr>>(), qi::locals, Skipper> timeBounds; qi::rule(), Skipper> rewardPathFormula; qi::rule(), qi::locals, Skipper> cumulativeRewardFormula;