AssumptionChecker.h

Go to the documentation of this file.

#pragma once
 
#include "storm/environment/Environment.h"
#include "storm/logic/Formula.h"
#include "storm/models/sparse/Dtmc.h"
#include "storm/models/sparse/Mdp.h"
#include "storm/storage/SparseMatrix.h"
 
#include "storm-pars/modelchecker/region/monotonicity/Assumption.h"
#include "storm-pars/modelchecker/region/monotonicity/Order.h"
#include "storm-pars/storage/ParameterRegion.h"
 
namespace storm {
namespace analysis {
enum AssumptionStatus {
    VALID,
    INVALID,
    UNKNOWN,
};
 
template<typename ValueType, typename ConstantType>
class AssumptionChecker {
   public:
    typedef typename utility::parametric::VariableType<ValueType>::type VariableType;
    typedef typename utility::parametric::CoefficientType<ValueType>::type CoefficientType;

    AssumptionChecker(storage::SparseMatrix<ValueType> matrix);

    AssumptionChecker(std::shared_ptr<logic::Formula const> formula, std::shared_ptr<models::sparse::Mdp<ValueType>> model,
                      uint_fast64_t const numberOfSamples);

    void initializeCheckingOnSamples(Environment const& env, std::shared_ptr<logic::Formula const> formula,
                                     std::shared_ptr<models::sparse::Dtmc<ValueType>> model, storage::ParameterRegion<ValueType> region,
                                     uint_fast64_t numberOfSamples);

    void setSampleValues(std::vector<std::vector<ConstantType>> samples);

    AssumptionStatus validateAssumption(Assumption const& assumption, std::shared_ptr<Order> order, storage::ParameterRegion<ValueType> region,
                                        std::vector<ConstantType> const minValues, std::vector<ConstantType> const maxValue) const;
    AssumptionStatus validateAssumption(Assumption const& assumption, std::shared_ptr<Order> order, storage::ParameterRegion<ValueType> region) const;
 
   private:
    bool useSamples;
 
    std::vector<std::vector<ConstantType>> samples;
 
    storage::SparseMatrix<ValueType> matrix;
 
    AssumptionStatus validateAssumptionSMTSolver(Assumption const& assumption, std::shared_ptr<Order> order, storage::ParameterRegion<ValueType> region,
                                                 std::vector<ConstantType> const minValues, std::vector<ConstantType> const maxValue) const;
 
    AssumptionStatus checkOnSamples(Assumption const& assumption) const;
};
}  // namespace analysis
}  // namespace storm