From 23686a0f09fd15379ba7cfb9ebaf4f641637831a Mon Sep 17 00:00:00 2001 From: TimQu Date: Fri, 13 Oct 2017 00:41:24 +0200 Subject: [PATCH] reward bounded cumulative reward formulas + fixes for dimensions that do not need memory --- src/storm/logic/CumulativeRewardFormula.cpp | 30 ++++++++-- src/storm/logic/CumulativeRewardFormula.h | 11 +++- src/storm/logic/FormulaInformationVisitor.cpp | 15 ++++- src/storm/logic/FragmentChecker.cpp | 15 ++++- src/storm/logic/FragmentSpecification.cpp | 33 ++++++++++ src/storm/logic/FragmentSpecification.h | 12 ++++ .../logic/VariableSubstitutionVisitor.cpp | 2 +- .../SparseMultiObjectivePreprocessor.cpp | 27 +++++++-- .../SparseMultiObjectivePreprocessorResult.h | 4 +- .../constraintbased/SparseCbQuery.cpp | 2 +- .../pcaa/PcaaWeightVectorChecker.cpp | 3 +- ...dpRewardBoundedPcaaWeightVectorChecker.cpp | 3 + .../pcaa/SparsePcaaWeightVectorChecker.cpp | 3 +- .../rewardbounded/MemoryStateManager.cpp | 21 ++++++- .../rewardbounded/MemoryStateManager.h | 7 ++- .../MultiDimensionalRewardUnfolding.cpp | 36 +++++++---- .../MultiDimensionalRewardUnfolding.h | 2 +- .../rewardbounded/ProductModel.cpp | 60 ++++++++++++------- .../prctl/SparseMdpPrctlModelChecker.cpp | 26 ++++++-- .../prctl/helper/SparseMdpPrctlHelper.cpp | 11 ++-- .../prctl/helper/SparseMdpPrctlHelper.h | 2 +- src/storm/parser/FormulaParserGrammar.cpp | 15 +++-- src/storm/parser/FormulaParserGrammar.h | 2 +- src/storm/parser/JaniParser.cpp | 8 +-- 24 files changed, 267 insertions(+), 83 deletions(-) diff --git a/src/storm/logic/CumulativeRewardFormula.cpp b/src/storm/logic/CumulativeRewardFormula.cpp index 36c82856c..a78c9b274 100644 --- a/src/storm/logic/CumulativeRewardFormula.cpp +++ b/src/storm/logic/CumulativeRewardFormula.cpp @@ -8,7 +8,7 @@ namespace storm { namespace logic { - CumulativeRewardFormula::CumulativeRewardFormula(TimeBound const& bound, TimeBoundType const& timeBoundType) : timeBoundType(timeBoundType), bound(bound) { + CumulativeRewardFormula::CumulativeRewardFormula(TimeBound const& bound, TimeBoundReference const& timeBoundReference) : timeBoundReference(timeBoundReference), bound(bound) { // Intentionally left empty. } @@ -24,16 +24,30 @@ namespace storm { return visitor.visit(*this, data); } - TimeBoundType const& CumulativeRewardFormula::getTimeBoundType() const { - return timeBoundType; + void CumulativeRewardFormula::gatherReferencedRewardModels(std::set& referencedRewardModels) const { + if (this->isRewardBounded()) { + referencedRewardModels.insert(this->getTimeBoundReference().getRewardName()); + } + } + + TimeBoundType CumulativeRewardFormula::getTimeBoundType() const { + return timeBoundReference.getType(); + } + + TimeBoundReference const& CumulativeRewardFormula::getTimeBoundReference() const { + return timeBoundReference; } bool CumulativeRewardFormula::isStepBounded() const { - return timeBoundType == TimeBoundType::Steps; + return getTimeBoundType() == TimeBoundType::Steps; } bool CumulativeRewardFormula::isTimeBounded() const { - return timeBoundType == TimeBoundType::Time; + return getTimeBoundType() == TimeBoundType::Time; + } + + bool CumulativeRewardFormula::isRewardBounded() const { + return getTimeBoundType() == TimeBoundType::Reward; } bool CumulativeRewardFormula::isBoundStrict() const { @@ -87,7 +101,11 @@ namespace storm { } std::ostream& CumulativeRewardFormula::writeToStream(std::ostream& out) const { - out << "C<=" << this->getBound(); + out << "C"; + if(getTimeBoundReference().isRewardBound()) { + out << "{\"" << getTimeBoundReference().getRewardName() << "\"}"; + } + out << "<=" << this->getBound(); return out; } } diff --git a/src/storm/logic/CumulativeRewardFormula.h b/src/storm/logic/CumulativeRewardFormula.h index fce825271..e7f5a60c1 100644 --- a/src/storm/logic/CumulativeRewardFormula.h +++ b/src/storm/logic/CumulativeRewardFormula.h @@ -10,7 +10,7 @@ namespace storm { namespace logic { class CumulativeRewardFormula : public PathFormula { public: - CumulativeRewardFormula(TimeBound const& bound, TimeBoundType const& timeBoundType = TimeBoundType::Time); + CumulativeRewardFormula(TimeBound const& bound, TimeBoundReference const& timeBoundReference = TimeBoundReference(TimeBoundType::Time)); virtual ~CumulativeRewardFormula() { // Intentionally left empty. @@ -21,11 +21,16 @@ namespace storm { 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 const& getTimeBoundType() const; + TimeBoundType getTimeBoundType() const; + TimeBoundReference const& getTimeBoundReference() const; + bool isStepBounded() const; bool isTimeBounded() const; + bool isRewardBounded() const; bool isBoundStrict() const; bool hasIntegerBound() const; @@ -41,7 +46,7 @@ namespace storm { private: static void checkNoVariablesInBound(storm::expressions::Expression const& bound); - TimeBoundType timeBoundType; + TimeBoundReference timeBoundReference; TimeBound bound; }; } diff --git a/src/storm/logic/FormulaInformationVisitor.cpp b/src/storm/logic/FormulaInformationVisitor.cpp index 08cd7ffaf..8c25686a9 100644 --- a/src/storm/logic/FormulaInformationVisitor.cpp +++ b/src/storm/logic/FormulaInformationVisitor.cpp @@ -30,10 +30,16 @@ namespace storm { result.setContainsBoundedUntilFormula(true); if (f.hasMultiDimensionalSubformulas()) { for (unsigned i = 0; i < f.getDimension(); ++i){ + if (f.getTimeBoundReference(i).isRewardBound()) { + result.setContainsRewardBoundedFormula(true); + } 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))); } @@ -44,8 +50,13 @@ namespace storm { return boost::any_cast(f.getSubformula().accept(*this, data)).join(boost::any_cast(f.getConditionFormula().accept(*this))); } - boost::any FormulaInformationVisitor::visit(CumulativeRewardFormula const&, boost::any const&) const { - return FormulaInformation(); + boost::any FormulaInformationVisitor::visit(CumulativeRewardFormula const& f, boost::any const&) const { + FormulaInformation result; + result.setContainsCumulativeRewardFormula(true); + if (f.getTimeBoundReference().isRewardBound()) { + result.setContainsRewardBoundedFormula(true); + } + return result; } boost::any FormulaInformationVisitor::visit(EventuallyFormula const& f, boost::any const& data) const { diff --git a/src/storm/logic/FragmentChecker.cpp b/src/storm/logic/FragmentChecker.cpp index 59514a884..53f707aa3 100644 --- a/src/storm/logic/FragmentChecker.cpp +++ b/src/storm/logic/FragmentChecker.cpp @@ -113,9 +113,20 @@ namespace storm { return result; } - boost::any FragmentChecker::visit(CumulativeRewardFormula const&, boost::any const& data) const { + boost::any FragmentChecker::visit(CumulativeRewardFormula const& f, boost::any const& data) const { InheritedInformation const& inherited = boost::any_cast(data); - return inherited.getSpecification().areCumulativeRewardFormulasAllowed(); + + 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(); + } + return result; } boost::any FragmentChecker::visit(EventuallyFormula const& f, boost::any const& data) const { diff --git a/src/storm/logic/FragmentSpecification.cpp b/src/storm/logic/FragmentSpecification.cpp index 9af898490..b08c0d927 100644 --- a/src/storm/logic/FragmentSpecification.cpp +++ b/src/storm/logic/FragmentSpecification.cpp @@ -60,6 +60,8 @@ namespace storm { prctl.setInstantaneousFormulasAllowed(true); prctl.setReachabilityRewardFormulasAllowed(true); prctl.setLongRunAverageOperatorsAllowed(true); + prctl.setStepBoundedCumulativeRewardFormulasAllowed(true); + prctl.setTimeBoundedCumulativeRewardFormulasAllowed(true); return prctl; } @@ -80,6 +82,7 @@ namespace storm { csrl.setInstantaneousFormulasAllowed(true); csrl.setReachabilityRewardFormulasAllowed(true); csrl.setLongRunAverageOperatorsAllowed(true); + csrl.setTimeBoundedCumulativeRewardFormulasAllowed(true); return csrl; } @@ -146,6 +149,9 @@ namespace storm { timeBoundedUntilFormulas = false; rewardBoundedUntilFormulas = false; multiDimensionalBoundedUntilFormulas = false; + stepBoundedCumulativeRewardFormulas = false; + timeBoundedCumulativeRewardFormulas = false; + rewardBoundedCumulativeRewardFormulas = false; varianceAsMeasureType = false; qualitativeOperatorResults = true; @@ -448,6 +454,33 @@ namespace storm { return *this; } + bool FragmentSpecification::areStepBoundedCumulativeRewardFormulasAllowed() const { + return this->stepBoundedCumulativeRewardFormulas; + } + + FragmentSpecification& FragmentSpecification::setStepBoundedCumulativeRewardFormulasAllowed(bool newValue) { + this->stepBoundedCumulativeRewardFormulas = newValue; + return *this; + } + + bool FragmentSpecification::areTimeBoundedCumulativeRewardFormulasAllowed() const { + return this->timeBoundedCumulativeRewardFormulas; + } + + FragmentSpecification& FragmentSpecification::setTimeBoundedCumulativeRewardFormulasAllowed(bool newValue) { + this->timeBoundedCumulativeRewardFormulas = newValue; + return *this; + } + + bool FragmentSpecification::areRewardBoundedCumulativeRewardFormulasAllowed() const { + return this->rewardBoundedCumulativeRewardFormulas; + } + + FragmentSpecification& FragmentSpecification::setRewardBoundedCumulativeRewardFormulasAllowed(bool newValue) { + this->rewardBoundedCumulativeRewardFormulas = 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 338907872..fbd3434e9 100644 --- a/src/storm/logic/FragmentSpecification.h +++ b/src/storm/logic/FragmentSpecification.h @@ -106,6 +106,15 @@ namespace storm { bool areRewardBoundedUntilFormulasAllowed() const; FragmentSpecification& setRewardBoundedUntilFormulasAllowed(bool newValue); + bool areStepBoundedCumulativeRewardFormulasAllowed() const; + FragmentSpecification& setStepBoundedCumulativeRewardFormulasAllowed(bool newValue); + + bool areTimeBoundedCumulativeRewardFormulasAllowed() const; + FragmentSpecification& setTimeBoundedCumulativeRewardFormulasAllowed(bool newValue); + + bool areRewardBoundedCumulativeRewardFormulasAllowed() const; + FragmentSpecification& setRewardBoundedCumulativeRewardFormulasAllowed(bool newValue); + bool areMultiDimensionalBoundedUntilFormulasAllowed() const; FragmentSpecification& setMultiDimensionalBoundedUntilFormulasAllowed(bool newValue); @@ -172,6 +181,9 @@ namespace storm { bool stepBoundedUntilFormulas; bool timeBoundedUntilFormulas; bool rewardBoundedUntilFormulas; + bool stepBoundedCumulativeRewardFormulas; + bool timeBoundedCumulativeRewardFormulas; + bool rewardBoundedCumulativeRewardFormulas; bool multiDimensionalBoundedUntilFormulas; bool varianceAsMeasureType; bool quantitativeOperatorResults; diff --git a/src/storm/logic/VariableSubstitutionVisitor.cpp b/src/storm/logic/VariableSubstitutionVisitor.cpp index 316bff867..47be93b36 100644 --- a/src/storm/logic/VariableSubstitutionVisitor.cpp +++ b/src/storm/logic/VariableSubstitutionVisitor.cpp @@ -65,7 +65,7 @@ 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.getTimeBoundType())); + return std::static_pointer_cast(std::make_shared(storm::logic::TimeBound(f.isBoundStrict(), f.getBound().substitute(substitution)), f.getTimeBoundReference())); } 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 cb9948b37..efe9fdf7d 100644 --- a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp +++ b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp @@ -285,7 +285,7 @@ namespace storm { } else { STORM_LOG_THROW(!data.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton) || formula.getTimeBoundReference().isTimeBound(), storm::exceptions::InvalidPropertyException, "Bounded until formulas for Markov Automata are only allowed when time bounds are considered."); storm::logic::TimeBound bound(formula.isUpperBoundStrict(), formula.getUpperBound()); - subformula = std::make_shared(bound, formula.getTimeBoundReference().getType()); + subformula = std::make_shared(bound, formula.getTimeBoundReference()); } preprocessUntilFormula(storm::logic::UntilFormula(formula.getLeftSubformula().asSharedPointer(), formula.getRightSubformula().asSharedPointer()), opInfo, data, subformula); } else { @@ -349,8 +349,13 @@ namespace storm { 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()); - auto cumulativeRewardFormula = std::make_shared(bound, storm::logic::TimeBoundType::Steps); + storm::logic::TimeBoundReference tbr(formula.getTimeBoundReference()); + auto cumulativeRewardFormula = std::make_shared(bound, tbr); data.objectives.back()->formula = std::make_shared(cumulativeRewardFormula, *optionalRewardModelName, opInfo); + data.upperResultBoundObjectives.set(data.objectives.size() - 1, true); + if (tbr.isRewardBound()) { + data.finiteRewardCheckObjectives.set(data.objectives.size() - 1, true); + } } template @@ -466,10 +471,19 @@ namespace storm { for (auto const& objIndex : finiteRewardCheckObjectives) { STORM_LOG_ASSERT(result.objectives[objIndex].formula->isRewardOperatorFormula(), "Objective needs to be checked for finite reward but has no reward operator."); auto const& rewModel = result.preprocessedModel->getRewardModel(result.objectives[objIndex].formula->asRewardOperatorFormula().getRewardModelName()); + auto unrelevantChoices = rewModel.getChoicesWithZeroReward(transitions); + // For (upper) reward bounded cumulative reward formulas, we do not need to consider the choices where boundReward is collected. + if (result.objectives[objIndex].formula->getSubformula().isCumulativeRewardFormula()) { + auto const& timeBoundReference = result.objectives[objIndex].formula->getSubformula().asCumulativeRewardFormula().getTimeBoundReference(); + // Only reward bounded formulas need a finiteness check + assert(timeBoundReference.isRewardBound()); + auto const& rewModelOfBound = result.preprocessedModel->getRewardModel(timeBoundReference.getRewardName()); + unrelevantChoices |= ~rewModelOfBound.getChoicesWithZeroReward(transitions); + } if (storm::solver::minimize(result.objectives[objIndex].formula->getOptimalityType())) { - minRewardsToCheck &= rewModel.getChoicesWithZeroReward(transitions); + minRewardsToCheck &= unrelevantChoices; } else { - maxRewardsToCheck &= rewModel.getChoicesWithZeroReward(transitions); + maxRewardsToCheck &= unrelevantChoices; } } maxRewardsToCheck.complement(); @@ -500,7 +514,9 @@ namespace storm { template boost::optional SparseMultiObjectivePreprocessor::computeUpperResultBound(ReturnType const& result, uint64_t objIndex, storm::storage::SparseMatrix const& backwardTransitions) { - if (result.objectives[objIndex].formula->isRewardOperatorFormula() && result.objectives[objIndex].formula->getSubformula().isTotalRewardFormula()) { + if (result.objectives[objIndex].formula->isRewardOperatorFormula() && (result.objectives[objIndex].formula->getSubformula().isTotalRewardFormula() || result.objectives[objIndex].formula->getSubformula().isCumulativeRewardFormula())) { + // TODO: Consider cumulative reward formulas less naively + // TODO: We have to eliminate ECs here to treat zero-reward ECs auto const& transitions = result.preprocessedModel->getTransitionMatrix(); auto const& rewModel = result.preprocessedModel->getRewardModel(result.objectives[objIndex].formula->asRewardOperatorFormula().getRewardModelName()); storm::storage::BitVector allStates(result.preprocessedModel->getNumberOfStates(), true); @@ -528,7 +544,6 @@ namespace storm { storm::modelchecker::helper::BaierUpperRewardBoundsComputer baier(submatrix, rewards, rew0StateProbs); return baier.computeUpperBound(); } - } diff --git a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorResult.h b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorResult.h index 91b509847..fee7adf5f 100644 --- a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorResult.h +++ b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorResult.h @@ -49,9 +49,9 @@ namespace storm { // Intentionally left empty } - bool containsOnlyRewardObjectives() const { + bool containsOnlyTrivialObjectives() const { for (auto const& obj : objectives) { - if (!(obj.formula->isRewardOperatorFormula() && (obj.formula->getSubformula().isTotalRewardFormula() || obj.formula->getSubformula().isCumulativeRewardFormula()))) { + if (!(obj.formula->isRewardOperatorFormula() && (obj.formula->getSubformula().isTotalRewardFormula() || (obj.formula->getSubformula().isCumulativeRewardFormula() && !obj.formula->getSubformula().asCumulativeRewardFormula().getTimeBoundReference().isRewardBound())))) { return false; } } diff --git a/src/storm/modelchecker/multiobjective/constraintbased/SparseCbQuery.cpp b/src/storm/modelchecker/multiobjective/constraintbased/SparseCbQuery.cpp index 942684376..1494f5281 100644 --- a/src/storm/modelchecker/multiobjective/constraintbased/SparseCbQuery.cpp +++ b/src/storm/modelchecker/multiobjective/constraintbased/SparseCbQuery.cpp @@ -25,7 +25,7 @@ namespace storm { STORM_LOG_THROW(preprocessorResult.rewardFinitenessType != SparseMultiObjectivePreprocessorResult::RewardFinitenessType::Infinite, storm::exceptions::NotSupportedException, "There is no Pareto optimal scheduler that yields finite reward for all objectives. This is not supported."); STORM_LOG_THROW(preprocessorResult.rewardLessInfinityEStates, storm::exceptions::UnexpectedException, "The set of states with reward < infinity for some scheduler has not been computed during preprocessing."); - STORM_LOG_THROW(preprocessorResult.containsOnlyRewardObjectives(), storm::exceptions::NotSupportedException, "At least one objective was not reduced to an expected (total or cumulative) reward objective during preprocessing. This is not supported by the considered weight vector checker."); + STORM_LOG_THROW(preprocessorResult.containsOnlyTrivialObjectives(), storm::exceptions::NotSupportedException, "At least one objective was not reduced to an expected (total or cumulative) reward objective during preprocessing. This is not supported by the considered weight vector checker."); STORM_LOG_THROW(preprocessorResult.preprocessedModel->getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::NotSupportedException, "The model has multiple initial states."); // Build a subsystem of the preprocessor result model that discards states that yield infinite reward for all schedulers. diff --git a/src/storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.cpp index d26b67b54..b15b6aad6 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.cpp @@ -54,9 +54,10 @@ namespace storm { template template>::value, int>::type> std::unique_ptr> WeightVectorCheckerFactory::create(SparseMultiObjectivePreprocessorResult const& preprocessorResult) { - if (preprocessorResult.containsOnlyRewardObjectives()) { + if (preprocessorResult.containsOnlyTrivialObjectives()) { return std::make_unique>(preprocessorResult); } else { + STORM_LOG_DEBUG("Query contains reward bounded formula"); return std::make_unique>(preprocessorResult); } } diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp index 8dcfb1f5b..385c72b1e 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp @@ -38,6 +38,8 @@ namespace storm { template void SparseMdpRewardBoundedPcaaWeightVectorChecker::check(std::vector const& weightVector) { + STORM_LOG_DEBUG("Analyzing weight vector " << storm::utility::vector::toString(weightVector)); + ++numChecks; // In case we want to export the cdf, we will collect the corresponding data @@ -183,6 +185,7 @@ namespace storm { } assert(x.size() == choices.size()); auto req = cachedData.linEqSolver->getRequirements(); + cachedData.linEqSolver->clearBounds(); if (obj.lowerResultBound) { req.clearLowerBounds(); cachedData.linEqSolver->setLowerBound(*obj.lowerResultBound); diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp index bd9045794..d9e3e95ff 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp @@ -32,7 +32,7 @@ namespace storm { STORM_LOG_THROW(preprocessorResult.rewardFinitenessType != SparseMultiObjectivePreprocessorResult::RewardFinitenessType::Infinite, storm::exceptions::NotSupportedException, "There is no Pareto optimal scheduler that yields finite reward for all objectives. This is not supported."); STORM_LOG_THROW(preprocessorResult.rewardLessInfinityEStates, storm::exceptions::UnexpectedException, "The set of states with reward < infinity for some scheduler has not been computed during preprocessing."); - STORM_LOG_THROW(preprocessorResult.containsOnlyRewardObjectives(), storm::exceptions::NotSupportedException, "At least one objective was not reduced to an expected (total or cumulative) reward objective during preprocessing. This is not supported by the considered weight vector checker."); + STORM_LOG_THROW(preprocessorResult.containsOnlyTrivialObjectives(), storm::exceptions::NotSupportedException, "At least one objective was not reduced to an expected (total or cumulative) reward objective during preprocessing. This is not supported by the considered weight vector checker."); STORM_LOG_THROW(preprocessorResult.preprocessedModel->getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::NotSupportedException, "The model has multiple initial states."); } @@ -264,6 +264,7 @@ namespace storm { // Now solve the resulting equation system. std::unique_ptr> solver = linearEquationSolverFactory.create(std::move(submatrix)); auto req = solver->getRequirements(); + solver->clearBounds(); if (obj.lowerResultBound) { req.clearLowerBounds(); solver->setLowerBound(*obj.lowerResultBound); diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/MemoryStateManager.cpp b/src/storm/modelchecker/multiobjective/rewardbounded/MemoryStateManager.cpp index df1411ea7..2ef2be3b7 100644 --- a/src/storm/modelchecker/multiobjective/rewardbounded/MemoryStateManager.cpp +++ b/src/storm/modelchecker/multiobjective/rewardbounded/MemoryStateManager.cpp @@ -8,7 +8,7 @@ namespace storm { namespace modelchecker { namespace multiobjective { - MemoryStateManager::MemoryStateManager(uint64_t dimensionCount) : dimensionCount(dimensionCount), dimensionBitMask(1ull), relevantBitsMask((1ull << dimensionCount) - 1), stateCount(dimensionBitMask << dimensionCount) { + MemoryStateManager::MemoryStateManager(uint64_t dimensionCount) : dimensionCount(dimensionCount), dimensionBitMask(1ull), relevantBitsMask((1ull << dimensionCount) - 1), stateCount(dimensionBitMask << dimensionCount), dimensionsWithoutMemoryMask(0), upperMemoryStateBound(stateCount) { STORM_LOG_THROW(dimensionCount > 0, storm::exceptions::IllegalArgumentException, "Invoked MemoryStateManager with zero dimension count."); STORM_LOG_THROW(dimensionCount <= 64, storm::exceptions::IllegalArgumentException, "Invoked MemoryStateManager with too many dimensions."); } @@ -21,6 +21,19 @@ namespace storm { return stateCount; } + MemoryStateManager::MemoryState const& MemoryStateManager::getUpperMemoryStateBound() const { + return upperMemoryStateBound; + } + + void MemoryStateManager::setDimensionWithoutMemory(uint64_t dimension) { + STORM_LOG_ASSERT(dimensionCount > 0, "Invoked MemoryStateManager with zero dimension count."); + STORM_LOG_ASSERT(dimension < dimensionCount, "Tried to set a dimension that is larger then the number of considered dimensions"); + if (((dimensionBitMask << dimension) & dimensionsWithoutMemoryMask) == 0) { + stateCount = (stateCount >> 1); + } + dimensionsWithoutMemoryMask |= (dimensionBitMask << dimension); + } + MemoryStateManager::MemoryState MemoryStateManager::getInitialMemoryState() const { STORM_LOG_ASSERT(dimensionCount > 0, "Invoked MemoryStateManager with zero dimension count."); return relevantBitsMask; @@ -28,18 +41,19 @@ namespace storm { bool MemoryStateManager::isRelevantDimension(MemoryState const& state, uint64_t dimension) const { STORM_LOG_ASSERT(dimensionCount > 0, "Invoked MemoryStateManager with zero dimension count."); + STORM_LOG_ASSERT((state & dimensionsWithoutMemoryMask) == dimensionsWithoutMemoryMask, "Invalid memory state found."); return (state & (dimensionBitMask << dimension)) != 0; } void MemoryStateManager::setRelevantDimension(MemoryState& state, uint64_t dimension, bool value) const { STORM_LOG_ASSERT(dimensionCount > 0, "Invoked MemoryStateManager with zero dimension count."); STORM_LOG_ASSERT(dimension < dimensionCount, "Tried to set a dimension that is larger then the number of considered dimensions"); + STORM_LOG_ASSERT(((dimensionBitMask << dimension) & dimensionsWithoutMemoryMask) == 0, "Tried to change a memory state for a dimension but the dimension is assumed to have no memory."); if (value) { state |= (dimensionBitMask << dimension); } else { state &= ~(dimensionBitMask << dimension); } - assert(state < getMemoryStateCount()); } void MemoryStateManager::setRelevantDimensions(MemoryState& state, storm::storage::BitVector const& dimensions, bool value) const { @@ -47,14 +61,15 @@ namespace storm { STORM_LOG_ASSERT(dimensions.size() == dimensionCount, "Invalid size of given bitset."); if (value) { for (auto const& d : dimensions) { + STORM_LOG_ASSERT(((dimensionBitMask << d) & dimensionsWithoutMemoryMask) == 0, "Tried to set a dimension to 'relevant'-memory state but the dimension is assumed to have no memory."); state |= (dimensionBitMask << d); } } else { for (auto const& d : dimensions) { + STORM_LOG_ASSERT(((dimensionBitMask << d) & dimensionsWithoutMemoryMask) == 0, "Tried to set a dimension to 'unrelevant'-memory state but the dimension is assumed to have no memory."); state &= ~(dimensionBitMask << d); } } - assert(state < getMemoryStateCount()); } std::string MemoryStateManager::toString(MemoryState const& state) const { diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/MemoryStateManager.h b/src/storm/modelchecker/multiobjective/rewardbounded/MemoryStateManager.h index db3ef06ad..98d97684b 100644 --- a/src/storm/modelchecker/multiobjective/rewardbounded/MemoryStateManager.h +++ b/src/storm/modelchecker/multiobjective/rewardbounded/MemoryStateManager.h @@ -18,8 +18,11 @@ namespace storm { MemoryStateManager(uint64_t dimensionCount); + void setDimensionWithoutMemory(uint64_t dimension); + uint64_t const& getDimensionCount() const; uint64_t const& getMemoryStateCount() const; + MemoryState const& getUpperMemoryStateBound() const; // is larger then every valid memory state m, i.e., m < getUpperMemoryStateBound() holds for all m MemoryState getInitialMemoryState() const; bool isRelevantDimension(MemoryState const& state, uint64_t dimension) const; @@ -32,7 +35,9 @@ namespace storm { uint64_t const dimensionCount; uint64_t const dimensionBitMask; uint64_t const relevantBitsMask; - uint64_t const stateCount; + uint64_t stateCount; + uint64_t dimensionsWithoutMemoryMask; + MemoryState const upperMemoryStateBound; }; } diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp index 2925c33d4..248d1ee8b 100644 --- a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp +++ b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp @@ -26,15 +26,20 @@ namespace storm { } template - MultiDimensionalRewardUnfolding::MultiDimensionalRewardUnfolding(storm::models::sparse::Mdp const& model, std::shared_ptr objectiveFormula) : model(model) { + MultiDimensionalRewardUnfolding::MultiDimensionalRewardUnfolding(storm::models::sparse::Mdp const& model, std::shared_ptr objectiveFormula) : model(model) { STORM_LOG_THROW(objectiveFormula->hasOptimalityType(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); - if (objectiveFormula->getSubformula().isMultiObjectiveFormula()) { - for (auto const& subFormula : objectiveFormula->getSubformula().asMultiObjectiveFormula().getSubformulas()) { - STORM_LOG_THROW(subFormula->isBoundedUntilFormula(), storm::exceptions::InvalidPropertyException, "Formula " << objectiveFormula << " is not supported. Invalid subformula " << *subFormula << "."); + if (objectiveFormula->isProbabilityOperatorFormula()) { + if (objectiveFormula->getSubformula().isMultiObjectiveFormula()) { + for (auto const& subFormula : objectiveFormula->getSubformula().asMultiObjectiveFormula().getSubformulas()) { + STORM_LOG_THROW(subFormula->isBoundedUntilFormula(), storm::exceptions::InvalidPropertyException, "Formula " << objectiveFormula << " is not supported. Invalid subformula " << *subFormula << "."); + } + } else { + STORM_LOG_THROW(objectiveFormula->getSubformula().isBoundedUntilFormula(), storm::exceptions::InvalidPropertyException, "Formula " << objectiveFormula << " is not supported. Invalid subformula " << objectiveFormula->getSubformula() << "."); } } else { - STORM_LOG_THROW(objectiveFormula->getSubformula().isBoundedUntilFormula(), storm::exceptions::InvalidPropertyException, "Formula " << objectiveFormula << " is not supported. Invalid subformula " << objectiveFormula->getSubformula() << "."); + STORM_LOG_THROW(objectiveFormula->isRewardOperatorFormula() && objectiveFormula->getSubformula().isCumulativeRewardFormula(), storm::exceptions::InvalidPropertyException, "Formula " << objectiveFormula << " is not supported."); + } // Build an objective from the formula. @@ -42,8 +47,6 @@ namespace storm { objective.formula = objectiveFormula; objective.originalFormula = objective.formula; objective.considersComplementaryEvent = false; - objective.lowerResultBound = storm::utility::zero(); - objective.upperResultBound = storm::utility::one(); objectives.push_back(std::move(objective)); initialize(); @@ -103,13 +106,26 @@ namespace storm { dimensions.emplace_back(std::move(dimension)); } } 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; - dimension.scalingFactor = storm::utility::one(); + 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); + } dimensions.emplace_back(std::move(dimension)); - dimensionWiseEpochSteps.push_back(std::vector(model.getNumberOfChoices(), 1)); } } @@ -265,7 +281,7 @@ namespace storm { template typename MultiDimensionalRewardUnfolding::EpochModel& MultiDimensionalRewardUnfolding::setCurrentEpoch(Epoch const& epoch) { - // std::cout << "Setting model for epoch " << epochManager.toString(epoch) << std::endl; + STORM_LOG_DEBUG("Setting model for epoch " << epochManager.toString(epoch)); // Check if we need to update the current epoch class if (!currentEpoch || !epochManager.compareEpochClass(epoch, currentEpoch.get())) { diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h index 03f4afcd6..ea30c7923 100644 --- a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h +++ b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h @@ -44,7 +44,7 @@ namespace storm { * */ MultiDimensionalRewardUnfolding(storm::models::sparse::Mdp const& model, std::vector> const& objectives); - MultiDimensionalRewardUnfolding(storm::models::sparse::Mdp const& model, std::shared_ptr objectiveFormula); + MultiDimensionalRewardUnfolding(storm::models::sparse::Mdp const& model, std::shared_ptr objectiveFormula); ~MultiDimensionalRewardUnfolding() { std::cout << "Unfolding statistics: " << std::endl; diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/ProductModel.cpp b/src/storm/modelchecker/multiobjective/rewardbounded/ProductModel.cpp index f5e8409f9..bd545c124 100644 --- a/src/storm/modelchecker/multiobjective/rewardbounded/ProductModel.cpp +++ b/src/storm/modelchecker/multiobjective/rewardbounded/ProductModel.cpp @@ -20,6 +20,12 @@ namespace storm { template ProductModel::ProductModel(storm::models::sparse::Mdp const& model, std::vector> const& objectives, std::vector> const& dimensions, std::vector const& objectiveDimensions, EpochManager const& epochManager, std::vector const& originalModelSteps) : dimensions(dimensions), objectiveDimensions(objectiveDimensions), epochManager(epochManager), memoryStateManager(dimensions.size()) { + for (uint64_t dim = 0; dim < dimensions.size(); ++dim) { + if (!dimensions[dim].memoryLabel) { + memoryStateManager.setDimensionWithoutMemory(dim); + } + } + storm::storage::MemoryStructure memory = computeMemoryStructure(model, objectives); assert(memoryStateManager.getMemoryStateCount() == memory.getNumberOfStates()); std::vector memoryStateMap = computeMemoryStateMap(memory); @@ -30,18 +36,19 @@ namespace storm { product = productBuilder.build()->template as>(); uint64_t numModelStates = productBuilder.getOriginalModel().getNumberOfStates(); + MemoryState upperMemStateBound = memoryStateManager.getUpperMemoryStateBound(); uint64_t numMemoryStates = memoryStateManager.getMemoryStateCount(); uint64_t numProductStates = getProduct().getNumberOfStates(); // Compute a mappings from product states to model/memory states and back - modelMemoryToProductStateMap.resize(numMemoryStates * numModelStates, std::numeric_limits::max()); + modelMemoryToProductStateMap.resize(upperMemStateBound * numModelStates, std::numeric_limits::max()); productToModelStateMap.resize(numProductStates, std::numeric_limits::max()); productToMemoryStateMap.resize(numProductStates, std::numeric_limits::max()); for (uint64_t modelState = 0; modelState < numModelStates; ++modelState) { for (uint64_t memoryStateIndex = 0; memoryStateIndex < numMemoryStates; ++memoryStateIndex) { if (productBuilder.isStateReachable(modelState, memoryStateIndex)) { uint64_t productState = productBuilder.getResultState(modelState, memoryStateIndex); - modelMemoryToProductStateMap[modelState * numMemoryStates + memoryStateMap[memoryStateIndex]] = productState; + modelMemoryToProductStateMap[modelState * upperMemStateBound + memoryStateMap[memoryStateIndex]] = productState; productToModelStateMap[productState] = modelState; productToMemoryStateMap[productState] = memoryStateMap[memoryStateIndex]; } @@ -190,10 +197,12 @@ namespace storm { MemoryState memState = memoryStateManager.getInitialMemoryState(); std::set stateLabels = memory.getStateLabeling().getLabelsOfState(memStateIndex); for (uint64_t dim = 0; dim < epochManager.getDimensionCount(); ++dim) { - if (dimensions[dim].memoryLabel && stateLabels.find(dimensions[dim].memoryLabel.get()) != stateLabels.end()) { - memoryStateManager.setRelevantDimension(memState, dim, true); - } else { - memoryStateManager.setRelevantDimension(memState, dim, false); + if (dimensions[dim].memoryLabel) { + if (stateLabels.find(dimensions[dim].memoryLabel.get()) != stateLabels.end()) { + memoryStateManager.setRelevantDimension(memState, dim, true); + } else { + memoryStateManager.setRelevantDimension(memState, dim, false); + } } } result.push_back(std::move(memState)); @@ -204,7 +213,7 @@ namespace storm { template void ProductModel::setReachableProductStates(storm::storage::SparseModelMemoryProduct& productBuilder, std::vector const& originalModelSteps, std::vector const& memoryStateMap) const { - std::vector inverseMemoryStateMap(memoryStateMap.size(), std::numeric_limits::max()); + std::vector inverseMemoryStateMap(memoryStateManager.getUpperMemoryStateBound(), std::numeric_limits::max()); for (uint64_t memStateIndex = 0; memStateIndex < memoryStateMap.size(); ++memStateIndex) { inverseMemoryStateMap[memoryStateMap[memStateIndex]] = memStateIndex; } @@ -213,14 +222,17 @@ namespace storm { auto const& model = productBuilder.getOriginalModel(); auto const& modelTransitions = model.getTransitionMatrix(); - std::vector reachableStates(memoryStateManager.getMemoryStateCount(), storm::storage::BitVector(model.getNumberOfStates(), false)); + std::vector reachableProductStates(memoryStateManager.getUpperMemoryStateBound()); + for (auto const& memState : memoryStateMap) { + reachableProductStates[memState] = storm::storage::BitVector(model.getNumberOfStates(), false); + } // Initialize the reachable states with the initial states EpochClass initEpochClass = epochManager.getEpochClass(epochManager.getZeroEpoch()); auto memStateIt = memory.getInitialMemoryStates().begin(); for (auto const& initState : model.getInitialStates()) { uint64_t transformedMemoryState = transformMemoryState(memoryStateMap[*memStateIt], initEpochClass, memoryStateManager.getInitialMemoryState()); - reachableStates[transformedMemoryState].set(initState, true); + reachableProductStates[transformedMemoryState].set(initState, true); ++memStateIt; } assert(memStateIt == memory.getInitialMemoryStates().end()); @@ -238,7 +250,7 @@ namespace storm { // Find the remaining set of reachable states via DFS. std::vector> dfsStack; for (MemoryState const& memState : memoryStateMap) { - for (auto const& modelState : reachableStates[memState]) { + for (auto const& modelState : reachableProductStates[memState]) { dfsStack.emplace_back(modelState, memState); } } @@ -255,8 +267,8 @@ namespace storm { MemoryState successorMemoryState = memoryStateMap[memory.getSuccessorMemoryState(currentMemoryStateIndex, transitionIt - modelTransitions.begin())]; successorMemoryState = transformMemoryState(successorMemoryState, epochClass, currentMemoryState); - if (!reachableStates[successorMemoryState].get(transitionIt->getColumn())) { - reachableStates[successorMemoryState].set(transitionIt->getColumn(), true); + if (!reachableProductStates[successorMemoryState].get(transitionIt->getColumn())) { + reachableProductStates[successorMemoryState].set(transitionIt->getColumn(), true); dfsStack.emplace_back(transitionIt->getColumn(), successorMemoryState); } } @@ -265,7 +277,7 @@ namespace storm { } for (uint64_t memStateIndex = 0; memStateIndex < memoryStateManager.getMemoryStateCount(); ++memStateIndex) { - for (auto const& modelState : reachableStates[memoryStateMap[memStateIndex]]) { + for (auto const& modelState : reachableProductStates[memoryStateMap[memStateIndex]]) { productBuilder.addReachableState(modelState, memStateIndex); } } @@ -283,13 +295,13 @@ namespace storm { template bool ProductModel::productStateExists(uint64_t const& modelState, MemoryState const& memoryState) const { - return modelMemoryToProductStateMap[modelState * memoryStateManager.getMemoryStateCount() + memoryState] < getProduct().getNumberOfStates(); + return modelMemoryToProductStateMap[modelState * memoryStateManager.getUpperMemoryStateBound() + memoryState] < getProduct().getNumberOfStates(); } template uint64_t ProductModel::getProductState(uint64_t const& modelState, MemoryState const& memoryState) const { STORM_LOG_ASSERT(productStateExists(modelState, memoryState), "Tried to obtain a state in the model-memory-product that does not exist"); - return modelMemoryToProductStateMap[modelState * memoryStateManager.getMemoryStateCount() + memoryState]; + return modelMemoryToProductStateMap[modelState * memoryStateManager.getUpperMemoryStateBound() + memoryState]; } template @@ -560,14 +572,16 @@ namespace storm { for (auto const& objDimensions : objectiveDimensions) { for (auto const& dim : objDimensions) { auto const& dimension = dimensions[dim]; - bool dimUpperBounded = dimension.isUpperBounded; - bool dimBottom = epochManager.isBottomDimensionEpochClass(epochClass, dim); - if (dimUpperBounded && dimBottom && memoryStateManager.isRelevantDimension(predecessorMemoryState, dim)) { - STORM_LOG_ASSERT(objDimensions == dimension.dependentDimensions, "Unexpected set of dependent dimensions"); - memoryStateManager.setRelevantDimensions(memoryStatePrime, objDimensions, false); - break; - } else if (!dimUpperBounded && !dimBottom && memoryStateManager.isRelevantDimension(predecessorMemoryState, dim)) { - memoryStateManager.setRelevantDimensions(memoryStatePrime, dimension.dependentDimensions, true); + if (dimension.memoryLabel) { + bool dimUpperBounded = dimension.isUpperBounded; + bool dimBottom = epochManager.isBottomDimensionEpochClass(epochClass, dim); + if (dimUpperBounded && dimBottom && memoryStateManager.isRelevantDimension(predecessorMemoryState, dim)) { + STORM_LOG_ASSERT(objDimensions == dimension.dependentDimensions, "Unexpected set of dependent dimensions"); + memoryStateManager.setRelevantDimensions(memoryStatePrime, objDimensions, false); + break; + } else if (!dimUpperBounded && !dimBottom && memoryStateManager.isRelevantDimension(predecessorMemoryState, dim)) { + memoryStateManager.setRelevantDimensions(memoryStatePrime, dimension.dependentDimensions, true); + } } } } diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index 4f59fdd01..2733044c5 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).setMultiDimensionalBoundedUntilFormulasAllowed(true))) { + if(formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true).setRewardBoundedCumulativeRewardFormulasAllowed(true).setMultiDimensionalBoundedUntilFormulasAllowed(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).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)); } } @@ -67,7 +67,7 @@ namespace storm { } auto formula = std::make_shared(checkTask.getFormula().asSharedPointer(), opInfo); storm::modelchecker::multiobjective::MultiDimensionalRewardUnfolding rewardUnfolding(this->getModel(), formula); - auto numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeNonTrivialBoundedUntilProbabilities(checkTask.getOptimizationDirection(), rewardUnfolding, this->getModel().getInitialStates(), *minMaxLinearEquationSolverFactory); + auto numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeRewardBoundedValues(checkTask.getOptimizationDirection(), rewardUnfolding, this->getModel().getInitialStates(), *minMaxLinearEquationSolverFactory, storm::utility::one()); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } else { STORM_LOG_THROW(!pathFormula.hasLowerBound() && pathFormula.hasUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have single upper time bound."); @@ -137,9 +137,23 @@ namespace storm { std::unique_ptr SparseMdpPrctlModelChecker::computeCumulativeRewards(storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); - STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); - std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeCumulativeRewards(storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getNonStrictBound(), *minMaxLinearEquationSolverFactory); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + if (rewardPathFormula.getTimeBoundReference().isRewardBound()) { + STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidOperationException, "Checking reward bounded cumulative reward formulas can only be done for the initial states of the model."); + STORM_LOG_WARN_COND(!checkTask.isQualitativeSet(), "Checking reward bounded until formulas is not optimized w.r.t. qualitative queries"); + storm::logic::OperatorInformation opInfo(checkTask.getOptimizationDirection()); + if (checkTask.isBoundSet()) { + opInfo.bound = checkTask.getBound(); + } + auto formula = std::make_shared(checkTask.getFormula().asSharedPointer(), checkTask.getRewardModel(), opInfo); + storm::modelchecker::multiobjective::MultiDimensionalRewardUnfolding rewardUnfolding(this->getModel(), formula); + auto numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeRewardBoundedValues(checkTask.getOptimizationDirection(), rewardUnfolding, this->getModel().getInitialStates(), *minMaxLinearEquationSolverFactory); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + } else { + + STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); + std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeCumulativeRewards(storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getNonStrictBound(), *minMaxLinearEquationSolverFactory); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + } } template diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index d3a37de46..46f54671a 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -77,7 +77,7 @@ namespace storm { } template - std::map SparseMdpPrctlHelper::computeNonTrivialBoundedUntilProbabilities(OptimizationDirection dir, storm::modelchecker::multiobjective::MultiDimensionalRewardUnfolding& rewardUnfolding, storm::storage::BitVector const& initialStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + std::map SparseMdpPrctlHelper::computeRewardBoundedValues(OptimizationDirection dir, storm::modelchecker::multiobjective::MultiDimensionalRewardUnfolding& rewardUnfolding, storm::storage::BitVector const& initialStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, boost::optional const& upperBound) { auto initEpoch = rewardUnfolding.getStartEpoch(); auto epochOrder = rewardUnfolding.getEpochComputationOrder(initEpoch); @@ -93,11 +93,14 @@ namespace storm { minMaxSolver->setOptimizationDirection(dir); minMaxSolver->setCachingEnabled(true); minMaxSolver->setTrackScheduler(true); - minMaxSolver->setLowerBound(storm::utility::zero()); - minMaxSolver->setUpperBound(storm::utility::one()); auto req = minMaxSolver->getRequirements(storm::solver::EquationSystemType::StochasticShortestPath, dir); + minMaxSolver->setLowerBound(storm::utility::zero()); + req.clearLowerBounds(); + if (upperBound) { + minMaxSolver->setUpperBound(upperBound.get()); + req.clearUpperBounds(); + } req.clearNoEndComponents(); - req.clearBounds(); STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "A solver requirement is not satisfied."); minMaxSolver->setRequirementsChecked(); } else { diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h index 7a14384f8..568526216 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h @@ -36,7 +36,7 @@ namespace storm { public: static std::vector computeStepBoundedUntilProbabilities(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint = ModelCheckerHint()); - static std::map computeNonTrivialBoundedUntilProbabilities(OptimizationDirection dir, storm::modelchecker::multiobjective::MultiDimensionalRewardUnfolding& rewardUnfolding, storm::storage::BitVector const& initialStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + static std::map computeRewardBoundedValues(OptimizationDirection dir, storm::modelchecker::multiobjective::MultiDimensionalRewardUnfolding& rewardUnfolding, storm::storage::BitVector const& initialStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, boost::optional const& upperBound = boost::none); static std::vector computeNextProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& nextStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); diff --git a/src/storm/parser/FormulaParserGrammar.cpp b/src/storm/parser/FormulaParserGrammar.cpp index 449d8fc48..36a3de44e 100644 --- a/src/storm/parser/FormulaParserGrammar.cpp +++ b/src/storm/parser/FormulaParserGrammar.cpp @@ -26,7 +26,7 @@ namespace storm { instantaneousRewardFormula = (qi::lit("I=") > expressionParser)[qi::_val = phoenix::bind(&FormulaParserGrammar::createInstantaneousRewardFormula, phoenix::ref(*this), qi::_1)]; instantaneousRewardFormula.name("instantaneous reward formula"); - cumulativeRewardFormula = ((qi::lit("C<=")[qi::_a = false] | qi::lit("C<")[qi::_a = true]) > expressionParser)[qi::_val = phoenix::bind(&FormulaParserGrammar::createCumulativeRewardFormula, phoenix::ref(*this), qi::_1, qi::_a)]; + cumulativeRewardFormula = (qi::lit("C") >> timeBound)[qi::_val = phoenix::bind(&FormulaParserGrammar::createCumulativeRewardFormula, phoenix::ref(*this), qi::_1)]; cumulativeRewardFormula.name("cumulative reward formula"); totalRewardFormula = (qi::lit("C"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createTotalRewardFormula, phoenix::ref(*this))]; @@ -60,7 +60,6 @@ namespace storm { notStateFormula.name("negation formula"); eventuallyFormula = (qi::lit("F") >> -(timeBound % qi::lit(",")) >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createEventuallyFormula, phoenix::ref(*this), qi::_1, qi::_r1, qi::_2)]; - // eventuallyFormula = (qi::lit("F") >> -timeBound >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createEventuallyFormula, phoenix::ref(*this), qi::_1, qi::_r1, qi::_2)]; eventuallyFormula.name("eventually formula"); globallyFormula = (qi::lit("G") >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createGloballyFormula, phoenix::ref(*this), qi::_1)]; @@ -237,8 +236,16 @@ namespace storm { return std::shared_ptr(new storm::logic::InstantaneousRewardFormula(timeBound)); } - std::shared_ptr FormulaParserGrammar::createCumulativeRewardFormula(storm::expressions::Expression const& timeBound, bool strict) const { - return std::shared_ptr(new storm::logic::CumulativeRewardFormula(storm::logic::TimeBound(strict, timeBound))); + std::shared_ptr FormulaParserGrammar::createCumulativeRewardFormula(std::tuple, boost::optional, boost::optional> const& timeBound) const { + STORM_LOG_THROW(!std::get<0>(timeBound), storm::exceptions::WrongFormatException, "Cumulative reward formulas with lower time bound are not allowed."); + STORM_LOG_THROW(std::get<1>(timeBound), storm::exceptions::WrongFormatException, "Cumulative reward formulas require an upper bound."); + if (std::get<2>(timeBound)) { + storm::logic::TimeBoundReference tbr(std::get<2>(timeBound).get()); + return std::shared_ptr(new storm::logic::CumulativeRewardFormula(std::get<1>(timeBound).get(), tbr)); + } else { + storm::logic::TimeBoundReference tbr(storm::logic::TimeBoundType::Time); + return std::shared_ptr(new storm::logic::CumulativeRewardFormula(std::get<1>(timeBound).get(), tbr)); + } } std::shared_ptr FormulaParserGrammar::createTotalRewardFormula() const { diff --git a/src/storm/parser/FormulaParserGrammar.h b/src/storm/parser/FormulaParserGrammar.h index df26f1ca0..aa344a19b 100644 --- a/src/storm/parser/FormulaParserGrammar.h +++ b/src/storm/parser/FormulaParserGrammar.h @@ -203,7 +203,7 @@ namespace storm { // Methods that actually create the expression objects. std::shared_ptr createInstantaneousRewardFormula(storm::expressions::Expression const& timeBound) const; - std::shared_ptr createCumulativeRewardFormula(storm::expressions::Expression const& timeBound, bool strict) const; + std::shared_ptr createCumulativeRewardFormula(std::tuple, boost::optional, boost::optional> const& timeBound) const; std::shared_ptr createTotalRewardFormula() const; std::shared_ptr createLongRunAverageRewardFormula() const; std::shared_ptr createAtomicExpressionFormula(storm::expressions::Expression const& expression) const; diff --git a/src/storm/parser/JaniParser.cpp b/src/storm/parser/JaniParser.cpp index 009b9b3eb..3de6bb2cc 100644 --- a/src/storm/parser/JaniParser.cpp +++ b/src/storm/parser/JaniParser.cpp @@ -273,7 +273,7 @@ namespace storm { } else { if (rewExpr.isVariable()) { std::string rewardName = rewExpr.getVariables().begin()->getName(); - return std::make_shared(std::make_shared(storm::logic::TimeBound(false, stepInstantExpr), storm::logic::TimeBoundType::Steps), rewardName, opInfo); + return std::make_shared(std::make_shared(storm::logic::TimeBound(false, stepInstantExpr), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Steps)), rewardName, opInfo); } else { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Only simple reward expressions are currently supported"); } @@ -294,7 +294,7 @@ namespace storm { } else { if (rewExpr.isVariable()) { std::string rewardName = rewExpr.getVariables().begin()->getName(); - return std::make_shared(std::make_shared(storm::logic::TimeBound(false, timeInstantExpr), storm::logic::TimeBoundType::Time), rewardName, opInfo); + return std::make_shared(std::make_shared(storm::logic::TimeBound(false, timeInstantExpr), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Time)), rewardName, opInfo); } else { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Only simple reward expressions are currently supported"); } @@ -619,7 +619,7 @@ namespace storm { initVal = expressionManager->rational(defaultRationalInitialValue); } else { initVal = parseExpression(variableStructure.at("initial-value"), "Initial value for variable " + name + " (scope: " + scopeDescription + ") ", globalVars, constants, localVars); - STORM_LOG_THROW(initVal.get().hasRationalType(), storm::exceptions::InvalidJaniException, "Initial value for integer variable " + name + "(scope " + scopeDescription + ") should be a rational"); + STORM_LOG_THROW(initVal.get().hasRationalType() || initVal.get().hasIntegerType(), storm::exceptions::InvalidJaniException, "Initial value for rational variable " + name + "(scope " + scopeDescription + ") should be a rational"); } return std::make_shared(name, expressionManager->declareRationalVariable(exprManagerName), initVal.get(), transientVar); @@ -632,7 +632,7 @@ namespace storm { initVal = expressionManager->boolean(defaultBooleanInitialValue); } else { initVal = parseExpression(variableStructure.at("initial-value"), "Initial value for variable " + name + " (scope: " + scopeDescription + ") ", globalVars, constants, localVars); - STORM_LOG_THROW(initVal.get().hasBooleanType(), storm::exceptions::InvalidJaniException, "Initial value for integer variable " + name + "(scope " + scopeDescription + ") should be a Boolean"); + STORM_LOG_THROW(initVal.get().hasBooleanType(), storm::exceptions::InvalidJaniException, "Initial value for boolean variable " + name + "(scope " + scopeDescription + ") should be a Boolean"); } if(transientVar) { labels.insert(name);