RegionModelChecker.h

Go to the documentation of this file.

#pragma once
 
#include <memory>
 
#include "storm-pars/analysis/LocalMonotonicityResult.h"
#include "storm-pars/analysis/Order.h"
#include "storm-pars/analysis/OrderExtender.h"
#include "storm-pars/modelchecker/region/RegionResult.h"
#include "storm-pars/modelchecker/region/RegionResultHypothesis.h"
#include "storm-pars/modelchecker/results/RegionCheckResult.h"
#include "storm-pars/modelchecker/results/RegionRefinementCheckResult.h"
#include "storm-pars/storage/ParameterRegion.h"
 
#include "storm/modelchecker/CheckTask.h"
#include "storm/models/ModelBase.h"
 
namespace storm {
 
class Environment;
 
namespace modelchecker {
 
// TODO type names are inconsistent and all over the place
template<typename ParametricType>
class RegionModelChecker {
   public:
    typedef typename storm::storage::ParameterRegion<ParametricType>::CoefficientType CoefficientType;
    typedef typename storm::storage::ParameterRegion<ParametricType>::VariableType VariableType;
 
    RegionModelChecker();
    virtual ~RegionModelChecker() = default;
 
    virtual bool canHandle(std::shared_ptr<storm::models::ModelBase> parametricModel,
                           CheckTask<storm::logic::Formula, ParametricType> const& checkTask) const = 0;
    virtual void specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel,
                         CheckTask<storm::logic::Formula, ParametricType> const& checkTask, bool generateRegionSplitEstimates,
                         bool allowModelSimplifications = true) = 0;
 
    virtual RegionResult analyzeRegion(Environment const& env, storm::storage::ParameterRegion<ParametricType> const& region,
                                       RegionResultHypothesis const& hypothesis = RegionResultHypothesis::Unknown,
                                       RegionResult const& initialResult = RegionResult::Unknown, bool sampleVerticesOfRegion = false,
                                       std::shared_ptr<storm::analysis::LocalMonotonicityResult<VariableType>> localMonotonicityResult = nullptr) = 0;
 
    std::unique_ptr<storm::modelchecker::RegionCheckResult<ParametricType>> analyzeRegions(
        Environment const& env, std::vector<storm::storage::ParameterRegion<ParametricType>> const& regions,
        std::vector<RegionResultHypothesis> const& hypotheses, bool sampleVerticesOfRegion = false);
 
    virtual ParametricType getBoundAtInitState(Environment const& env, storm::storage::ParameterRegion<ParametricType> const& region,
                                               storm::solver::OptimizationDirection const& dirForParameters);
 
    std::unique_ptr<storm::modelchecker::RegionRefinementCheckResult<ParametricType>> performRegionRefinement(
        Environment const& env, storm::storage::ParameterRegion<ParametricType> const& region, boost::optional<ParametricType> const& coverageThreshold,
        boost::optional<uint64_t> depthThreshold = boost::none, RegionResultHypothesis const& hypothesis = RegionResultHypothesis::Unknown,
        uint64_t monThresh = 0);
 
    // TODO return type is not quite nice
    // TODO consider returning v' as well
    virtual std::pair<ParametricType, typename storm::storage::ParameterRegion<ParametricType>::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 = std::nullopt);
    virtual bool verifyRegion(Environment const& env, storm::storage::ParameterRegion<ParametricType> const& region, storm::logic::Bound const& bound);
 
    virtual bool isRegionSplitEstimateSupported() const;
 
    virtual std::map<VariableType, double> getRegionSplitEstimate() const;
 
    virtual std::shared_ptr<storm::analysis::Order> extendOrder(std::shared_ptr<storm::analysis::Order> order,
                                                                storm::storage::ParameterRegion<ParametricType> region);
 
    virtual void setConstantEntries(std::shared_ptr<storm::analysis::LocalMonotonicityResult<VariableType>> localMonotonicityResult);
 
    bool isUseMonotonicitySet() const;
    bool isUseBoundsSet();
    bool isOnlyGlobalSet();
 
    void setUseMonotonicity(bool monotonicity = true);
    void setUseBounds(bool bounds = true);
    void setUseOnlyGlobal(bool global = true);
 
    virtual void setMaxSplitDimensions(uint64_t);
    virtual void resetMaxSplitDimensions();
 
    void setMonotoneParameters(std::pair<std::set<typename storm::storage::ParameterRegion<ParametricType>::VariableType>,
                                         std::set<typename storm::storage::ParameterRegion<ParametricType>::VariableType>>
                                   monotoneParameters);
 
   private:
    bool useMonotonicity = false;
    bool useOnlyGlobal = false;
    bool useBounds = false;
 
   protected:
    uint_fast64_t numberOfRegionsKnownThroughMonotonicity;
    boost::optional<std::set<typename storm::storage::ParameterRegion<ParametricType>::VariableType>> monotoneIncrParameters;
    boost::optional<std::set<typename storm::storage::ParameterRegion<ParametricType>::VariableType>> monotoneDecrParameters;
 
    virtual void extendLocalMonotonicityResult(storm::storage::ParameterRegion<ParametricType> const& region, std::shared_ptr<storm::analysis::Order> order,
                                               std::shared_ptr<storm::analysis::LocalMonotonicityResult<VariableType>> localMonotonicityResult);
 
    virtual void splitSmart(storm::storage::ParameterRegion<ParametricType>& region, std::vector<storm::storage::ParameterRegion<ParametricType>>& regionVector,
                            storm::analysis::MonotonicityResult<VariableType>& monRes, bool splitForExtremum) const;
};
class RegionModelChecker {…};
 
}  // namespace modelchecker
}  // namespace storm