RegionRefinementChecker.h

Go to the documentation of this file.

#pragma once
 
#include <memory>
 
#include "storm-pars/analysis/GraphPreservationStatus.h"
#include "storm-pars/modelchecker/region/RegionResult.h"
#include "storm-pars/modelchecker/region/RegionResultHypothesis.h"
#include "storm-pars/modelchecker/region/RegionSplittingStrategy.h"
#include "storm-pars/modelchecker/results/RegionRefinementCheckResult.h"
#include "storm-pars/storage/ParameterRegion.h"
 
#include "storm/modelchecker/CheckTask.h"
#include "storm/models/ModelBase.h"
#include "storm/utility/ExtendedNumber.h"
 
namespace storm {
 
class Environment;
 
namespace modelchecker {
 
template<typename ParametricType>
struct AnnotatedRegion;
 
template<typename ParametricType>
class RegionModelChecker;
 
template<typename ParametricType>
class MonotonicityBackend;
 
template<typename ParametricType>
class RegionRefinementChecker {
   public:
    using CoefficientType = typename storm::storage::ParameterRegion<ParametricType>::CoefficientType;
    using ExtendedCoefficientType = storm::utility::ExtendedValueType<CoefficientType>;
    using VariableType = typename storm::storage::ParameterRegion<ParametricType>::VariableType;
    using Valuation = typename storm::storage::ParameterRegion<ParametricType>::Valuation;
 
    RegionRefinementChecker(std::unique_ptr<RegionModelChecker<ParametricType>>&& regionChecker);
    ~RegionRefinementChecker() = default;
 
    bool canHandle(std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, ParametricType> const& checkTask) const;
 
    void specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel,
                 CheckTask<storm::logic::Formula, ParametricType> const& checkTask, RegionSplittingStrategy splittingStrategy = RegionSplittingStrategy(),
                 std::set<VariableType> const& discreteVariables = {}, std::shared_ptr<MonotonicityBackend<ParametricType>> monotonicityBackend = {},
                 bool allowModelSimplifications = true,
                 storm::pars::analysis::GraphPreservationStatus graphPreservationStatus = storm::pars::analysis::GraphPreservationStatus::GraphPreserving);

    std::unique_ptr<storm::modelchecker::RegionRefinementCheckResult<ParametricType>> performRegionPartitioning(
        Environment const& env, storm::storage::ParameterRegion<ParametricType> const& region, std::optional<ParametricType> coverageThreshold,
        std::optional<uint64_t> depthThreshold = std::nullopt, RegionResultHypothesis const& hypothesis = RegionResultHypothesis::Unknown,
        uint64_t monThresh = 0);

    std::pair<ExtendedCoefficientType, Valuation> computeExtremalValueHelper(
        Environment const& env, storm::storage::ParameterRegion<ParametricType> const& region, storm::solver::OptimizationDirection const& dir,
        std::function<bool(ExtendedCoefficientType const&, ExtendedCoefficientType const&)> acceptGlobalBound,
        std::function<bool(ExtendedCoefficientType const&)> rejectInstance);

    std::pair<ExtendedCoefficientType, Valuation> computeExtremalValue(Environment const& env, storm::storage::ParameterRegion<ParametricType> const& region,
                                                                       storm::solver::OptimizationDirection const& dir, ParametricType const& precision,
                                                                       bool absolutePrecision, std::optional<storm::logic::Bound> const& boundInvariant);

    bool verifyRegion(Environment const& env, storm::storage::ParameterRegion<ParametricType> const& region, storm::logic::Bound const& bound);
 
   private:
    enum class Context { Partitioning, ExtremalValue };
    std::set<VariableType> getSplittingVariablesEstimateBased(AnnotatedRegion<ParametricType> const& region, Context context) const;
    std::set<VariableType> getSplittingVariablesRoundRobin(AnnotatedRegion<ParametricType> const& region, Context context) const;
 
    std::set<VariableType> getSplittingVariables(AnnotatedRegion<ParametricType> const& region, Context context) const;
 
    std::unique_ptr<RegionModelChecker<ParametricType>> regionChecker;
    std::shared_ptr<MonotonicityBackend<ParametricType>> monotonicityBackend;
    RegionSplittingStrategy regionSplittingStrategy;
    std::set<VariableType> discreteVariables;
    storm::pars::analysis::GraphPreservationStatus graphPreservationStatus;
};
 
}  // namespace modelchecker
}  // namespace storm