ValidatingSparseParameterLiftingModelChecker.h

Go to the documentation of this file.

#pragma once
 
#include "storm-pars/modelchecker/region/RegionModelChecker.h"
#include "storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h"
#include "storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.h"
#include "storm/models/sparse/Dtmc.h"
#include "storm/models/sparse/Mdp.h"
#include "storm/utility/NumberTraits.h"
 
namespace storm {
namespace modelchecker {
 
template<typename SparseModelType, typename ImpreciseType, typename PreciseType>
class ValidatingSparseParameterLiftingModelChecker : public RegionModelChecker<typename SparseModelType::ValueType> {
    static_assert(storm::NumberTraits<PreciseType>::IsExact, "Specified type for exact computations is not exact.");
 
    using ParametricType = typename SparseModelType::ValueType;
    using CoefficientType = typename RegionModelChecker<ParametricType>::CoefficientType;
    using ExtendedCoefficientType = typename RegionModelChecker<ParametricType>::ExtendedCoefficientType;
    using VariableType = typename RegionModelChecker<ParametricType>::VariableType;
    using Valuation = typename RegionModelChecker<ParametricType>::Valuation;
 
   public:
    ValidatingSparseParameterLiftingModelChecker();
    virtual ~ValidatingSparseParameterLiftingModelChecker();
 
    virtual bool canHandle(std::shared_ptr<storm::models::ModelBase> parametricModel,
                           CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) const override;
 
    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) override;

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

    virtual ExtendedCoefficientType getBoundAtInitState(Environment const& env, AnnotatedRegion<ParametricType>& region,
                                                        storm::solver::OptimizationDirection const& dirForParameters) override;

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

    virtual bool isMonotonicitySupported(MonotonicityBackend<ParametricType> const& backend,
                                         CheckTask<storm::logic::Formula, ParametricType> const& checkTask) const override;
 
   private:
    static constexpr bool IsMDP = std::is_same_v<SparseModelType, storm::models::sparse::Mdp<ParametricType>>;
    static constexpr bool IsDTMC = std::is_same_v<SparseModelType, storm::models::sparse::Dtmc<ParametricType>>;
    static_assert(IsMDP || IsDTMC, "Model type is neither MDP nor DTMC.");
 
    template<typename T>
    using UnderlyingCheckerType = typename std::conditional_t<IsMDP, SparseMdpParameterLiftingModelChecker<SparseModelType, T>,
                                                              SparseDtmcParameterLiftingModelChecker<SparseModelType, T>>;
 
    UnderlyingCheckerType<ImpreciseType> impreciseChecker;
    UnderlyingCheckerType<PreciseType> preciseChecker;
 
    void applyHintsToPreciseChecker();
 
    // Information for statistics
    uint_fast64_t numOfWrongRegions;
};
}  // namespace modelchecker
}  // namespace storm