diff --git a/src/storm/logic/Formula.cpp b/src/storm/logic/Formula.cpp index fe3a1e41a..58970c77b 100644 --- a/src/storm/logic/Formula.cpp +++ b/src/storm/logic/Formula.cpp @@ -209,6 +209,14 @@ namespace storm { return dynamic_cast(*this); } + QuantileFormula& Formula::asQuantileFormula() { + return dynamic_cast(*this); + } + + QuantileFormula const& Formula::asQuantileFormula() const { + return dynamic_cast(*this); + } + BinaryStateFormula& Formula::asBinaryStateFormula() { return dynamic_cast(*this); } diff --git a/src/storm/logic/Formula.h b/src/storm/logic/Formula.h index bd88374a3..dc6396e71 100644 --- a/src/storm/logic/Formula.h +++ b/src/storm/logic/Formula.h @@ -110,6 +110,9 @@ namespace storm { MultiObjectiveFormula& asMultiObjectiveFormula(); MultiObjectiveFormula const& asMultiObjectiveFormula() const; + QuantileFormula& asQuantileFormula(); + QuantileFormula const& asQuantileFormula() const; + BinaryStateFormula& asBinaryStateFormula(); BinaryStateFormula const& asBinaryStateFormula() const; diff --git a/src/storm/modelchecker/AbstractModelChecker.cpp b/src/storm/modelchecker/AbstractModelChecker.cpp index 42bb2a753..2c12639c3 100644 --- a/src/storm/modelchecker/AbstractModelChecker.cpp +++ b/src/storm/modelchecker/AbstractModelChecker.cpp @@ -48,6 +48,8 @@ namespace storm { return this->checkStateFormula(env, checkTask.substituteFormula(formula.asStateFormula())); } else if (formula.isMultiObjectiveFormula()){ return this->checkMultiObjectiveFormula(env, checkTask.substituteFormula(formula.asMultiObjectiveFormula())); + } else if (formula.isQuantileFormula()){ + return this->checkQuantileFormula(env, checkTask.substituteFormula(formula.asQuantileFormula())); } STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << formula << "' is invalid."); } @@ -311,6 +313,11 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker (" << getClassName() << ") does not support the formula: " << checkTask.getFormula() << "."); } + template + std::unique_ptr AbstractModelChecker::checkQuantileFormula(Environment const& env, CheckTask const& checkTask) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker (" << getClassName() << ") does not support the formula: " << checkTask.getFormula() << "."); + } + /////////////////////////////////////////////// // Explicitly instantiate the template class. /////////////////////////////////////////////// diff --git a/src/storm/modelchecker/AbstractModelChecker.h b/src/storm/modelchecker/AbstractModelChecker.h index 44373de03..80bf18fb6 100644 --- a/src/storm/modelchecker/AbstractModelChecker.h +++ b/src/storm/modelchecker/AbstractModelChecker.h @@ -91,7 +91,10 @@ namespace storm { // The methods to check multi-objective formulas. virtual std::unique_ptr checkMultiObjectiveFormula(Environment const& env, CheckTask const& checkTask); - + + // The methods to check quantile formulas. + virtual std::unique_ptr checkQuantileFormula(Environment const& env, CheckTask const& checkTask); + }; } } diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index b78ad3856..e83fba585 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -7,6 +7,7 @@ #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "storm/modelchecker/results/ExplicitParetoCurveCheckResult.h" #include "storm/logic/FragmentSpecification.h" @@ -14,6 +15,7 @@ #include "storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h" +#include "storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.h" #include "storm/modelchecker/multiobjective/multiObjectiveModelChecking.h" #include "storm/solver/SolveGoal.h" @@ -40,13 +42,17 @@ namespace storm { storm::logic::Formula const& formula = checkTask.getFormula(); if (formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true).setTotalRewardFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true).setRewardBoundedCumulativeRewardFormulasAllowed(true).setMultiDimensionalBoundedUntilFormulasAllowed(true).setMultiDimensionalCumulativeRewardFormulasAllowed(true).setTimeOperatorsAllowed(true).setReachbilityTimeFormulasAllowed(true))) { return true; - } else { + } else if (formula.isInFragment(storm::logic::multiObjective().setCumulativeRewardFormulasAllowed(true).setTimeBoundedCumulativeRewardFormulasAllowed(true).setStepBoundedCumulativeRewardFormulasAllowed(true).setRewardBoundedCumulativeRewardFormulasAllowed(true).setTimeBoundedUntilFormulasAllowed(true).setStepBoundedUntilFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true).setMultiDimensionalBoundedUntilFormulasAllowed(true).setMultiDimensionalCumulativeRewardFormulasAllowed(true))) { // 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).setMultiDimensionalCumulativeRewardFormulasAllowed(true)); + return true; + } else if (formula.isInFragment(storm::logic::quantiles())) { + if (this->getModel().getInitialStates().getNumberOfSetBits() > 1) return false; + return true; } + return false; } template @@ -220,6 +226,22 @@ namespace storm { return multiobjective::performMultiObjectiveModelChecking(env, this->getModel(), checkTask.getFormula()); } + template + std::unique_ptr SparseMdpPrctlModelChecker::checkQuantileFormula(Environment const& env, CheckTask const& checkTask) { + STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidOperationException, "Computing quantiles is only supported for models with a single initial states."); + STORM_LOG_THROW(this->getModel().getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::InvalidOperationException, "Quantiles not supported on models with multiple initial states."); + uint64_t initialState = *this->getModel().getInitialStates().begin(); + + helper::rewardbounded::QuantileHelper qHelper(this->getModel(), checkTask.getFormula()); + auto res = qHelper.computeMultiDimensionalQuantile(); + + if (res.size() == 1 && res.front().size() == 1) { + return std::unique_ptr(new ExplicitQuantitativeCheckResult(initialState, std::move(res.front().front()))); + } else { + return std::unique_ptr(new ExplicitParetoCurveCheckResult(initialState, std::move(res))); + } + } + template class SparseMdpPrctlModelChecker>; #ifdef STORM_HAVE_CARL diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h index 19c2cc6a1..38a0a090c 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h @@ -33,6 +33,7 @@ namespace storm { virtual std::unique_ptr computeLongRunAverageProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr checkMultiObjectiveFormula(Environment const& env, CheckTask const& checkTask) override; + virtual std::unique_ptr checkQuantileFormula(Environment const& env, CheckTask const& checkTask) override; }; } // namespace modelchecker diff --git a/src/storm/modelchecker/prctl/helper/rewardbounded/Dimension.h b/src/storm/modelchecker/prctl/helper/rewardbounded/Dimension.h index 80059ce1e..76127e5e8 100644 --- a/src/storm/modelchecker/prctl/helper/rewardbounded/Dimension.h +++ b/src/storm/modelchecker/prctl/helper/rewardbounded/Dimension.h @@ -3,6 +3,7 @@ #include #include "storm/storage/BitVector.h" +#include "storm/solver/OptimizationDirection.h" namespace storm { namespace modelchecker { @@ -18,6 +19,7 @@ namespace storm { ValueType scalingFactor; storm::storage::BitVector dependentDimensions; boost::optional maxValue; + boost::optional optimizationDirection; }; } } diff --git a/src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.cpp b/src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.cpp index efc3c81f7..87d2b968d 100644 --- a/src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.cpp +++ b/src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.cpp @@ -88,6 +88,7 @@ namespace storm { dimension.memoryLabel = memLabel; dimension.isUpperBounded = subformula.hasUpperBound(dim); // for simplicity we do not allow intervals or unbounded formulas. + // TODO: Quantiles: allow unbounded formulas STORM_LOG_THROW(subformula.hasLowerBound(dim) != dimension.isUpperBounded, storm::exceptions::NotSupportedException, "Bounded until formulas are only supported by this method if they consider either an upper bound or a lower bound. Got " << subformula << " instead."); // lower bounded until formulas with non-trivial left hand side are excluded as this would require some additional effort (in particular the ProductModel::transformMemoryState method). STORM_LOG_THROW(dimension.isUpperBounded || subformula.getLeftSubformula(dim).isTrueFormula(), storm::exceptions::NotSupportedException, "Lower bounded until formulas are only supported by this method if the left subformula is 'true'. Got " << subformula << " instead."); @@ -216,20 +217,22 @@ namespace storm { bound = dimFormula.asCumulativeRewardFormula().getBound(); isStrict = dimFormula.asCumulativeRewardFormula().isBoundStrict(); } - STORM_LOG_THROW(!bound.containsVariables(), storm::exceptions::NotSupportedException, "The bound " << bound << " contains undefined constants."); - ValueType discretizedBound = storm::utility::convertNumber(bound.evaluateAsRational()); - STORM_LOG_THROW(dimensions[dim].isUpperBounded || isStrict || !storm::utility::isZero(discretizedBound), storm::exceptions::NotSupportedException, "Lower bounds need to be either strict or greater than zero."); - discretizedBound /= dimensions[dim].scalingFactor; - if (storm::utility::isInteger(discretizedBound)) { - if (isStrict == dimensions[dim].isUpperBounded) { - discretizedBound -= storm::utility::one(); + + if (bound.containsVariables()) { + ValueType discretizedBound = storm::utility::convertNumber(bound.evaluateAsRational()); + STORM_LOG_THROW(dimensions[dim].isUpperBounded || isStrict || !storm::utility::isZero(discretizedBound), storm::exceptions::NotSupportedException, "Lower bounds need to be either strict or greater than zero."); + discretizedBound /= dimensions[dim].scalingFactor; + if (storm::utility::isInteger(discretizedBound)) { + if (isStrict == dimensions[dim].isUpperBounded) { + discretizedBound -= storm::utility::one(); + } + } else { + discretizedBound = storm::utility::floor(discretizedBound); } - } else { - discretizedBound = storm::utility::floor(discretizedBound); + uint64_t dimensionValue = storm::utility::convertNumber(discretizedBound); + STORM_LOG_THROW(epochManager.isValidDimensionValue(dimensionValue), storm::exceptions::NotSupportedException, "The bound " << bound << " is too high for the considered number of dimensions."); + dimensions[dim].maxValue = dimensionValue; } - uint64_t dimensionValue = storm::utility::convertNumber(discretizedBound); - STORM_LOG_THROW(epochManager.isValidDimensionValue(dimensionValue), storm::exceptions::NotSupportedException, "The bound " << bound << " is too high for the considered number of dimensions."); - dimensions[dim].maxValue = dimensionValue; } } diff --git a/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.cpp b/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.cpp new file mode 100644 index 000000000..a502569eb --- /dev/null +++ b/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.cpp @@ -0,0 +1,10 @@ +#include "storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.h" + +namespace storm { + namespace modelchecker { + namespace helper { + namespace rewardbounded { + } + } + } +} diff --git a/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.h b/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.h new file mode 100644 index 000000000..4d31b1624 --- /dev/null +++ b/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.h @@ -0,0 +1,21 @@ +#pragma once + +#include "storm/logic/QuantileFormula.h" + +namespace storm { + namespace modelchecker { + namespace helper { + namespace rewardbounded { + + template + class QuantileHelper { + typedef typename ModelType::ValueType ValueType; + public: + QuantileHelper(ModelType const& model, storm::logic::QuantileFormula const& formula) {} + + std::vector> computeMultiDimensionalQuantile() { return {{27}};} + }; + } + } + } +} diff --git a/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.h b/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.h index 5bc42feff..e25221958 100644 --- a/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.h +++ b/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.h @@ -12,8 +12,8 @@ namespace storm { class ExplicitParetoCurveCheckResult : public ParetoCurveCheckResult { public: ExplicitParetoCurveCheckResult(); - ExplicitParetoCurveCheckResult(storm::storage::sparse::state_type const& state, std::vector::point_type> const& points, typename ParetoCurveCheckResult::polytope_type const& underApproximation, typename ParetoCurveCheckResult::polytope_type const& overApproximation); - ExplicitParetoCurveCheckResult(storm::storage::sparse::state_type const& state, std::vector::point_type>&& points, typename ParetoCurveCheckResult::polytope_type&& underApproximation, typename ParetoCurveCheckResult::polytope_type&& overApproximation); + ExplicitParetoCurveCheckResult(storm::storage::sparse::state_type const& state, std::vector::point_type> const& points, typename ParetoCurveCheckResult::polytope_type const& underApproximation = nullptr, typename ParetoCurveCheckResult::polytope_type const& overApproximation = nullptr); + ExplicitParetoCurveCheckResult(storm::storage::sparse::state_type const& state, std::vector::point_type>&& points, typename ParetoCurveCheckResult::polytope_type&& underApproximation = nullptr, typename ParetoCurveCheckResult::polytope_type&& overApproximation = nullptr); ExplicitParetoCurveCheckResult(ExplicitParetoCurveCheckResult const& other) = default; ExplicitParetoCurveCheckResult& operator=(ExplicitParetoCurveCheckResult const& other) = default; diff --git a/src/storm/modelchecker/results/ParetoCurveCheckResult.cpp b/src/storm/modelchecker/results/ParetoCurveCheckResult.cpp index 39ae4e265..ffc34528a 100644 --- a/src/storm/modelchecker/results/ParetoCurveCheckResult.cpp +++ b/src/storm/modelchecker/results/ParetoCurveCheckResult.cpp @@ -31,22 +31,38 @@ namespace storm { return points; } + template + bool ParetoCurveCheckResult::hasUnderApproximation() const { + return bool(underApproximation); + } + + template + bool ParetoCurveCheckResult::hasOverApproximation() const { + return bool(overApproximation); + } + template typename ParetoCurveCheckResult::polytope_type const& ParetoCurveCheckResult::getUnderApproximation() const { + STORM_LOG_ASSERT(hasUnderApproximation(), "Requested under approx. of Pareto curve although it does not exist."); return underApproximation; } template typename ParetoCurveCheckResult::polytope_type const& ParetoCurveCheckResult::getOverApproximation() const { + STORM_LOG_ASSERT(hasUnderApproximation(), "Requested over approx. of Pareto curve although it does not exist."); return overApproximation; } template std::ostream& ParetoCurveCheckResult::writeToStream(std::ostream& out) const { out << std::endl; - out << "Underapproximation of achievable values: " << underApproximation->toString() << std::endl; - out << "Overapproximation of achievable values: " << overApproximation->toString() << std::endl; - out << points.size() << " pareto optimal points found (Note that these points are safe, i.e., contained in the underapproximation, but there is no guarantee for optimality):" << std::endl; + if (hasUnderApproximation()) { + out << "Underapproximation of achievable values: " << underApproximation->toString() << std::endl; + } + if (hasOverApproximation()) { + out << "Overapproximation of achievable values: " << overApproximation->toString() << std::endl; + } + out << points.size() << " Pareto optimal points found:" << std::endl; for(auto const& p : points) { out << " ("; for(auto it = p.begin(); it != p.end(); ++it){ diff --git a/src/storm/modelchecker/results/ParetoCurveCheckResult.h b/src/storm/modelchecker/results/ParetoCurveCheckResult.h index e2b3be825..9397bc4c5 100644 --- a/src/storm/modelchecker/results/ParetoCurveCheckResult.h +++ b/src/storm/modelchecker/results/ParetoCurveCheckResult.h @@ -19,14 +19,16 @@ namespace storm { virtual bool isParetoCurveCheckResult() const override; std::vector const& getPoints() const; + bool hasUnderApproximation() const; + bool hasOverApproximation() const; polytope_type const& getUnderApproximation() const; polytope_type const& getOverApproximation() const; virtual std::ostream& writeToStream(std::ostream& out) const override; protected: - ParetoCurveCheckResult(std::vector const& points, polytope_type const& underApproximation, polytope_type const& overApproximation); - ParetoCurveCheckResult(std::vector&& points, polytope_type&& underApproximation, polytope_type&& overApproximation); + ParetoCurveCheckResult(std::vector const& points, polytope_type const& underApproximation = nullptr, polytope_type const& overApproximation = nullptr); + ParetoCurveCheckResult(std::vector&& points, polytope_type&& underApproximation = nullptr, polytope_type&& overApproximation = nullptr); // The pareto optimal points that have been found. std::vector points;