From d3abeb5f45d74f3d9b0e6fef79fcf420e4824903 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Mon, 28 Jan 2019 12:58:18 +0100 Subject: [PATCH] Started implementation on quantiles. --- src/storm/logic/TimeBound.h | 3 +- src/storm/logic/TimeBoundType.h | 2 + .../prctl/SparseMdpPrctlModelChecker.cpp | 2 +- .../helper/rewardbounded/QuantileHelper.cpp | 81 +++++++++++++++++++ .../helper/rewardbounded/QuantileHelper.h | 16 +++- 5 files changed, 99 insertions(+), 5 deletions(-) diff --git a/src/storm/logic/TimeBound.h b/src/storm/logic/TimeBound.h index 17a4c2b41..6ab0c29c8 100644 --- a/src/storm/logic/TimeBound.h +++ b/src/storm/logic/TimeBound.h @@ -8,7 +8,8 @@ namespace storm { class TimeBound { public: TimeBound(bool strict, storm::expressions::Expression const& bound); - + TimeBound(TimeBound const& other) = default; + storm::expressions::Expression const& getBound() const; bool isStrict() const; diff --git a/src/storm/logic/TimeBoundType.h b/src/storm/logic/TimeBoundType.h index 149f76215..91f4b134c 100644 --- a/src/storm/logic/TimeBoundType.h +++ b/src/storm/logic/TimeBoundType.h @@ -29,6 +29,8 @@ namespace storm { assert(rewardName != ""); // Empty reward name is reserved. } + TimeBoundReference(TimeBoundReference const& other) = default; + TimeBoundType getType() const { return type; } diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index e83fba585..b16bd7b3c 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -233,7 +233,7 @@ namespace storm { uint64_t initialState = *this->getModel().getInitialStates().begin(); helper::rewardbounded::QuantileHelper qHelper(this->getModel(), checkTask.getFormula()); - auto res = qHelper.computeMultiDimensionalQuantile(); + auto res = qHelper.computeMultiDimensionalQuantile(env); if (res.size() == 1 && res.front().size() == 1) { return std::unique_ptr(new ExplicitQuantitativeCheckResult(initialState, std::move(res.front().front()))); diff --git a/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.cpp b/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.cpp index a502569eb..54ca1622f 100644 --- a/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.cpp @@ -1,9 +1,90 @@ #include "storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.h" +#include +#include +#include +#include + +#include "storm/models/sparse/Mdp.h" +#include "storm/storage/expressions/ExpressionManager.h" + +#include "storm/logic/ProbabilityOperatorFormula.h" +#include "storm/logic/BoundedUntilFormula.h" + namespace storm { namespace modelchecker { namespace helper { namespace rewardbounded { + + template + QuantileHelper::QuantileHelper(ModelType const& model, storm::logic::QuantileFormula const& quantileFormula) : model(model), quantileFormula(quantileFormula) { + // Intentionally left empty + } + + std::shared_ptr replaceBoundsByGreaterEqZero(std::shared_ptr const& boundedUntilOperator, std::set dimensionsToReplace) { + auto const& origBoundedUntil = boundedUntilOperator->getSubformula().asBoundedUntilFormula(); + STORM_LOG_ASSERT(*(--dimensionsToReplace.end()) < origBoundedUntil.getDimension(), "Tried to replace the bound of a dimension that is higher than the number of dimensions of the formula."); + std::vector> leftSubformulas, rightSubformulas; + std::vector> lowerBounds, upperBounds; + std::vector timeBoundReferences; + + for (uint64_t dim = 0; dim < origBoundedUntil.getDimension(); ++dim) { + leftSubformulas.push_back(origBoundedUntil.getLeftSubformula(dim).asSharedPointer()); + rightSubformulas.push_back(origBoundedUntil.getRightSubformula(dim).asSharedPointer()); + timeBoundReferences.push_back(origBoundedUntil.getTimeBoundReference(dim)); + if (dimensionsToReplace.count(dim) == 0) { + if (origBoundedUntil.hasLowerBound()) { + lowerBounds.push_back(storm::logic::TimeBound(origBoundedUntil.isLowerBoundStrict(dim), origBoundedUntil.getLowerBound(dim))); + } else { + lowerBounds.push_back(boost::none); + } + if (origBoundedUntil.hasUpperBound()) { + upperBounds.emplace_back(origBoundedUntil.isUpperBoundStrict(dim), origBoundedUntil.getUpperBound(dim)); + } else { + upperBounds.push_back(boost::none); + } + } else { + storm::expressions::Expression zero; + if (origBoundedUntil.hasLowerBound(dim)) { + zero = origBoundedUntil.getLowerBound(dim).getManager().rational(0.0); + } else { + STORM_LOG_THROW(origBoundedUntil.hasUpperBound(dim), storm::exceptions::InvalidOperationException, "The given bounded until formula has no cost-bound for one dimension."); + zero = origBoundedUntil.getUpperBound(dim).getManager().rational(0.0); + } + lowerBounds.emplace_back(false, zero); + upperBounds.push_back(boost::none); + } + } + auto newBoundedUntil = std::make_shared(leftSubformulas, rightSubformulas, lowerBounds, upperBounds, timeBoundReferences); + return std::make_shared(newBoundedUntil, boundedUntilOperator->getOperatorInformation()); + } + + + + template + std::vector> QuantileHelper::computeMultiDimensionalQuantile(Environment const& env) { + std::vector> result; + if (!computeUnboundedValue(env)) { + STORM_LOG_INFO("Bound is not satisfiable."); + result.emplace_back(); + for (auto const& bv : quantileFormula.getBoundVariables()) { + result.front().push_back(storm::solver::minimize(bv.first) ? storm::utility::infinity() : -storm::utility::infinity()); + } + } else { + result = {{27}}; + } + return result; + } + + template + bool QuantileHelper::computeUnboundedValue(Environment const& env) { + return false; + } + + + template class QuantileHelper>; + template class QuantileHelper>; + } } } diff --git a/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.h b/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.h index 4d31b1624..276b9faed 100644 --- a/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.h +++ b/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.h @@ -3,6 +3,8 @@ #include "storm/logic/QuantileFormula.h" namespace storm { + class Environment; + namespace modelchecker { namespace helper { namespace rewardbounded { @@ -11,9 +13,17 @@ namespace storm { class QuantileHelper { typedef typename ModelType::ValueType ValueType; public: - QuantileHelper(ModelType const& model, storm::logic::QuantileFormula const& formula) {} - - std::vector> computeMultiDimensionalQuantile() { return {{27}};} + QuantileHelper(ModelType const& model, storm::logic::QuantileFormula const& quantileFormula); + + std::vector> computeMultiDimensionalQuantile(Environment const& env); + + + + private: + bool computeUnboundedValue(Environment const& env); + + ModelType const& model; + storm::logic::QuantileFormula const& quantileFormula; }; } }