QuantileHelper.h

Go to the documentation of this file.

#pragma once
 
#include <boost/optional.hpp>
#include <map>
 
#include "storm/logic/ProbabilityOperatorFormula.h"
#include "storm/logic/QuantileFormula.h"
#include "storm/modelchecker/prctl/helper/rewardbounded/CostLimitClosure.h"
#include "storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.h"
#include "storm/storage/BitVector.h"
#include "storm/utility/ExtendedNumber.h"
#include "storm/utility/Stopwatch.h"
 
namespace storm {
class Environment;
 
namespace modelchecker {
namespace helper {
namespace rewardbounded {
 
template<typename ModelType>
class QuantileHelper {
    typedef typename ModelType::ValueType ValueType;
 
   public:
    QuantileHelper(ModelType const& model, storm::logic::QuantileFormula const& quantileFormula);
 
    std::vector<std::vector<storm::utility::ExtendedValueType<ValueType>>> computeQuantile(Environment const& env);
 
   private:
    std::pair<CostLimitClosure, std::vector<ValueType>> computeQuantile(Environment& env, storm::storage::BitVector const& consideredDimensions,
                                                                        bool complementaryQuery);
    bool computeQuantile(Environment& env, storm::storage::BitVector const& consideredDimensions,
                         storm::logic::ProbabilityOperatorFormula const& boundedUntilOperator, storm::storage::BitVector const& lowerBoundedDimensions,
                         CostLimitClosure& satCostLimits, CostLimitClosure& unsatCostLimits, MultiDimensionalRewardUnfolding<ValueType, true>& rewardUnfolding);

    uint64_t getDimension() const;

    storm::storage::BitVector getOpenDimensions() const;
 
    storm::expressions::Variable const& getVariableForDimension(uint64_t const& dim) const;
 
    ModelType const& model;
    storm::logic::QuantileFormula const& quantileFormula;
    std::map<storm::storage::BitVector, std::pair<CostLimitClosure, std::vector<ValueType>>> cachedSubQueryResults;

    mutable uint64_t numCheckedEpochs;
    mutable uint64_t numPrecisionRefinements;
    mutable storm::utility::Stopwatch swEpochAnalysis;
    mutable storm::utility::Stopwatch swExploration;
};
}  // namespace rewardbounded
}  // namespace helper
}  // namespace modelchecker
}  // namespace storm