SparseParameterLiftingModelChecker.h

Go to the documentation of this file.

#pragma once
 
#include "storm-pars/modelchecker/region/RegionModelChecker.h"
#include "storm-pars/storage/ParameterRegion.h"
#include "storm-pars/utility/parametric.h"
 
#include "storm/logic/Formulas.h"
#include "storm/modelchecker/CheckTask.h"
#include "storm/modelchecker/results/CheckResult.h"
#include "storm/solver/OptimizationDirection.h"
#include "storm/utility/ExtendedNumber.h"
 
namespace storm {
namespace modelchecker {
 
template<typename SparseModelType, typename ConstantType>
class SparseInstantiationModelChecker;

template<typename SparseModelType, typename ConstantType>
class SparseParameterLiftingModelChecker : public RegionModelChecker<typename SparseModelType::ValueType> {
   public:
    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;
    using ExtendedConstantType = storm::utility::ExtendedValueType<ConstantType>;
 
    SparseParameterLiftingModelChecker();
    virtual ~SparseParameterLiftingModelChecker() = default;

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

    RegionResult sampleVertices(Environment const& env, storm::storage::ParameterRegion<ParametricType> const& region,
                                RegionResult const& initialResult = RegionResult::Unknown);

    std::unique_ptr<CheckResult> check(Environment const& env, AnnotatedRegion<ParametricType>& region,
                                       storm::solver::OptimizationDirection const& dirForParameters);

    std::unique_ptr<QuantitativeCheckResult<ConstantType>> getBound(Environment const& env, AnnotatedRegion<ParametricType>& region,
                                                                    storm::solver::OptimizationDirection const& dirForParameters);

    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;
 
    SparseModelType const& getConsideredParametricModel() const;
    CheckTask<storm::logic::Formula, ConstantType> const& getCurrentCheckTask() const;
 
   protected:
    void specifyFormula(Environment const& env, CheckTask<storm::logic::Formula, ParametricType> const& checkTask);
 
    bool hasUniqueInitialState() const;
    uint64_t getUniqueInitialState() const;
 
    // Resets all data that correspond to the currently defined property.
    virtual void reset() = 0;
 
    virtual void specifyBoundedUntilFormula(const CheckTask<storm::logic::BoundedUntilFormula, ConstantType>& checkTask);
    virtual void specifyUntilFormula(Environment const& env, CheckTask<storm::logic::UntilFormula, ConstantType> const& checkTask);
    virtual void specifyReachabilityProbabilityFormula(Environment const& env, CheckTask<storm::logic::EventuallyFormula, ConstantType> const& checkTask);
    virtual void specifyReachabilityRewardFormula(Environment const& env, CheckTask<storm::logic::EventuallyFormula, ConstantType> const& checkTask);
    virtual void specifyCumulativeRewardFormula(const CheckTask<storm::logic::CumulativeRewardFormula, ConstantType>& checkTask);
 
    virtual storm::modelchecker::SparseInstantiationModelChecker<SparseModelType, ConstantType>& getInstantiationChecker(Environment const& env,
                                                                                                                         bool quantitative) = 0;
    virtual storm::modelchecker::SparseInstantiationModelChecker<SparseModelType, ConstantType>& getInstantiationCheckerSAT(Environment const& env,
                                                                                                                            bool quantitative);
    virtual storm::modelchecker::SparseInstantiationModelChecker<SparseModelType, ConstantType>& getInstantiationCheckerVIO(Environment const& env,
                                                                                                                            bool quantitative);
 
    virtual std::vector<ExtendedConstantType> computeQuantitativeValues(Environment const& env, AnnotatedRegion<ParametricType>& region,
                                                                        storm::solver::OptimizationDirection const& dirForParameters) = 0;
 
    void updateKnownValueBoundInRegion(AnnotatedRegion<ParametricType>& region, storm::solver::OptimizationDirection dir,
                                       std::vector<ExtendedConstantType> const& newValues);
 
    std::shared_ptr<SparseModelType> parametricModel;
    std::unique_ptr<CheckTask<storm::logic::Formula, ConstantType>> currentCheckTask;
 
   private:
    // store the current formula. Note that currentCheckTask only stores a reference to the formula.
    std::shared_ptr<storm::logic::Formula const> currentFormula;
};
}  // namespace modelchecker
}  // namespace storm