AssumptionChecker.h

Go to the documentation of this file.

#pragma once
 
#include "Order.h"
#include "storm-pars/storage/ParameterRegion.h"
#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/storage/expressions/BinaryRelationExpression.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(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(uint_fast64_t val1, uint_fast64_t val2, std::shared_ptr<expressions::BinaryRelationExpression> assumption,
                                        std::shared_ptr<Order> order, storage::ParameterRegion<ValueType> region, std::vector<ConstantType> const minValues,
                                        std::vector<ConstantType> const maxValue) const;
    AssumptionStatus validateAssumption(std::shared_ptr<expressions::BinaryRelationExpression> 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(uint_fast64_t val1, uint_fast64_t val2, std::shared_ptr<expressions::BinaryRelationExpression> assumption,
                                                 std::shared_ptr<Order> order, storage::ParameterRegion<ValueType> region,
                                                 std::vector<ConstantType> const minValues, std::vector<ConstantType> const maxValue) const;
 
    AssumptionStatus checkOnSamples(std::shared_ptr<expressions::BinaryRelationExpression> assumption) const;
};
}  // namespace analysis
}  // namespace storm