AssumptionMaker.h

Go to the documentation of this file.

#pragma once
 
#include "AssumptionChecker.h"
#include "Order.h"
 
#include "storm/storage/SparseMatrix.h"
#include "storm/storage/expressions/BinaryRelationExpression.h"
#include "storm/storage/expressions/ExpressionManager.h"
 
namespace storm {
namespace analysis {
 
template<typename ValueType, typename ConstantType>
class AssumptionMaker {
    typedef std::shared_ptr<expressions::BinaryRelationExpression> AssumptionType;
 
   public:
    AssumptionMaker(storage::SparseMatrix<ValueType> matrix);

    std::map<std::shared_ptr<expressions::BinaryRelationExpression>, AssumptionStatus> createAndCheckAssumptions(
        uint_fast64_t val1, uint_fast64_t val2, std::shared_ptr<Order> order, storage::ParameterRegion<ValueType> region) const;
    std::map<std::shared_ptr<expressions::BinaryRelationExpression>, 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(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<std::shared_ptr<expressions::BinaryRelationExpression>, AssumptionStatus> createAndCheckAssumption(
        uint_fast64_t val1, uint_fast64_t val2, expressions::RelationType 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;
 
    std::shared_ptr<expressions::ExpressionManager> expressionManager;
 
    uint_fast64_t numberOfStates;
};
}  // namespace analysis
}  // namespace storm