MonotonicityBackend.h

Go to the documentation of this file.

#pragma once
 
#include <set>
#include "storm-pars/modelchecker/region/monotonicity/MonotonicityKind.h"
#include "storm-pars/utility/parametric.h"
 
namespace storm {
class Environment;
}
 
namespace storm::modelchecker {
 
template<typename ParametricType>
struct AnnotatedRegion;
 
template<typename ParametricType>
class MonotonicityBackend {
   public:
    using CoefficientType = storm::utility::parametric::CoefficientType_t<ParametricType>;
    using VariableType = storm::utility::parametric::VariableType_t<ParametricType>;
    using Valuation = storm::utility::parametric::Valuation<ParametricType>;
    using MonotonicityKind = storm::analysis::MonotonicityKind;
 
    MonotonicityBackend() = default;
    virtual ~MonotonicityBackend() = default;
 
    void setMonotoneParameter(VariableType const& parameter, MonotonicityKind const& kind);
 
    virtual bool requiresInteractionWithRegionModelChecker() const;
 
    virtual bool recommendModelSimplifications() const;
 
    virtual void initializeMonotonicity(storm::Environment const& env, AnnotatedRegion<ParametricType>& region);
 
    virtual void updateMonotonicity(storm::Environment const& env, AnnotatedRegion<ParametricType>& region);
 
    virtual void updateMonotonicityBeforeSplitting(storm::Environment const& env, AnnotatedRegion<ParametricType>& region);
 
    virtual std::map<VariableType, MonotonicityKind> getOptimisticMonotonicityApproximation(AnnotatedRegion<ParametricType> const& region);
 
   protected:
    std::map<VariableType, MonotonicityKind> globallyKnownMonotonicityInformation;
};
 
}  // namespace storm::modelchecker