RegionModelChecker.h

Go to the documentation of this file.

#pragma once
 
#include <memory>
#include <optional>
 
#include "storm-pars/analysis/GraphPreservationStatus.h"
#include "storm-pars/modelchecker/region/AnnotatedRegion.h"
#include "storm-pars/modelchecker/region/RegionResult.h"
#include "storm-pars/modelchecker/region/RegionResultHypothesis.h"
#include "storm-pars/modelchecker/region/RegionSplitEstimateKind.h"
#include "storm-pars/modelchecker/results/RegionCheckResult.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>
struct AnnotatedRegion;
template<typename ParametricType>
class MonotonicityBackend;
 
template<typename ParametricType>
class RegionModelChecker {
   public:
    typedef typename storm::storage::ParameterRegion<ParametricType>::CoefficientType CoefficientType;
    typedef storm::utility::ExtendedValueType<CoefficientType> ExtendedCoefficientType;
    typedef typename storm::storage::ParameterRegion<ParametricType>::VariableType VariableType;
    typedef typename storm::storage::ParameterRegion<ParametricType>::Valuation Valuation;
 
    RegionModelChecker() = default;
    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,
        std::optional<RegionSplitEstimateKind> generateRegionSplitEstimates = std::nullopt,
        std::shared_ptr<MonotonicityBackend<ParametricType>> monotonicityBackend = {}, bool allowModelSimplifications = true,
        storm::pars::analysis::GraphPreservationStatus graphPreservationStatus = storm::pars::analysis::GraphPreservationStatus::GraphPreserving) = 0;

    virtual RegionResult analyzeRegion(Environment const& env, AnnotatedRegion<ParametricType>& region,
                                       RegionResultHypothesis const& hypothesis = RegionResultHypothesis::Unknown, bool sampleVerticesOfRegion = false) = 0;

    RegionResult analyzeRegion(Environment const& env, storm::storage::ParameterRegion<ParametricType> const& region,
                               RegionResultHypothesis const& hypothesis = RegionResultHypothesis::Unknown, bool sampleVerticesOfRegion = false);

    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 ExtendedCoefficientType getBoundAtInitState(Environment const& env, AnnotatedRegion<ParametricType>& region,
                                                        storm::solver::OptimizationDirection const& dirForParameters) = 0;

    ExtendedCoefficientType getBoundAtInitState(Environment const& env, storm::storage::ParameterRegion<ParametricType> const& region,
                                                storm::solver::OptimizationDirection const& dirForParameters);

    virtual std::pair<ExtendedCoefficientType, Valuation> getAndEvaluateGoodPoint(Environment const& env, AnnotatedRegion<ParametricType>& region,
                                                                                  storm::solver::OptimizationDirection const& dirForParameters) = 0;

    virtual RegionSplitEstimateKind getDefaultRegionSplitEstimateKind(CheckTask<storm::logic::Formula, ParametricType> const& checkTask) const;

    virtual bool isRegionSplitEstimateKindSupported(RegionSplitEstimateKind kind, CheckTask<storm::logic::Formula, ParametricType> const& checkTask) const;

    std::optional<RegionSplitEstimateKind> getSpecifiedRegionSplitEstimateKind() const;

    virtual std::vector<CoefficientType> obtainRegionSplitEstimates(std::set<VariableType> const& relevantParameters) const;

    virtual bool isMonotonicitySupported(MonotonicityBackend<ParametricType> const& backend,
                                         CheckTask<storm::logic::Formula, ParametricType> const& checkTask) const = 0;
 
   protected:
    virtual void specifySplitEstimates(std::optional<RegionSplitEstimateKind> splitEstimates,
                                       CheckTask<storm::logic::Formula, ParametricType> const& checkTask);
    virtual void specifyMonotonicity(std::shared_ptr<MonotonicityBackend<ParametricType>> backend,
                                     CheckTask<storm::logic::Formula, ParametricType> const& checkTask);
 
    std::optional<storm::storage::ParameterRegion<ParametricType>> lastCheckedRegion;
    std::optional<RegionSplitEstimateKind> specifiedRegionSplitEstimateKind;
    std::shared_ptr<MonotonicityBackend<ParametricType>> monotonicityBackend;
};
 
}  // namespace modelchecker
}  // namespace storm