AssumptionMaker.h

Go to the documentation of this file.

#pragma once
 
#include "storm/storage/SparseMatrix.h"
 
#include "storm-pars/modelchecker/region/monotonicity/Assumption.h"
#include "storm-pars/modelchecker/region/monotonicity/AssumptionChecker.h"
#include "storm-pars/modelchecker/region/monotonicity/Order.h"
 
namespace storm {
namespace analysis {
 
template<typename ValueType, typename ConstantType>
class AssumptionMaker {
   public:
    AssumptionMaker(storage::SparseMatrix<ValueType> matrix);

    std::vector<std::pair<Assumption, AssumptionStatus>> createAndCheckAssumptions(uint_fast64_t val1, uint_fast64_t val2, std::shared_ptr<Order> order,
                                                                                   storage::ParameterRegion<ValueType> region) const;
    std::vector<std::pair<Assumption, AssumptionStatus>> createAndCheckAssumptions(uint_fast64_t val1, uint_fast64_t val2, std::shared_ptr<Order> order,
                                                                                   storage::ParameterRegion<ValueType> region,
                                                                                   std::vector<ConstantType> const minValues,
                                                                                   std::vector<ConstantType> const maxValue) const;

    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>> const& samples);
 
   private:
    std::pair<Assumption, AssumptionStatus> createAndCheckAssumption(uint_fast64_t val1, uint_fast64_t val2, AssumptionRelation relationType,
                                                                     std::shared_ptr<Order> order, storage::ParameterRegion<ValueType> region,
                                                                     std::vector<ConstantType> const minValues, std::vector<ConstantType> const maxValue) const;
 
    AssumptionChecker<ValueType, ConstantType> assumptionChecker;
};
}  // namespace analysis
}  // namespace storm