GraphConditions.h

Go to the documentation of this file.

#pragma once
 
#include <type_traits>
#include <unordered_set>
 
#pragma clang diagnostic push
#pragma clang diagnostic ignored "-Wmacro-redefined"  // clash for likely() macro between Ginac and Sylvan
#pragma clang diagnostic ignored "-Wthread-safety-negative"
#pragma clang diagnostic ignored "-Wundefined-reinterpret-cast"
#pragma clang diagnostic ignored "-Wunused-template"
#include <carl/formula/Formula.h>
#pragma clang diagnostic pop
 
#include "storm/adapters/RationalFunctionAdapter.h"
#include "storm/models/sparse/Dtmc.h"
 
namespace storm {
namespace analysis {
 
template<typename ValueType, typename Enable = void>
struct ConstraintType {
    typedef void* val;
};
 
template<typename ValueType>
struct ConstraintType<ValueType, typename std::enable_if<std::is_same<storm::RationalFunction, ValueType>::value>::type> {
    typedef carl::Formula<typename storm::RationalFunction::PolyType::PolyType> val;
};

template<typename ValueType>
class ConstraintCollector {
   private:
    // A set of constraints that says that the DTMC actually has valid probability distributions in all states.
    std::unordered_set<typename ConstraintType<ValueType>::val> wellformedConstraintSet;
 
    // A set of constraints that makes sure that the underlying graph of the model does not change depending
    // on the parameter values.
    std::unordered_set<typename ConstraintType<ValueType>::val> graphPreservingConstraintSet;
 
    // A set of variables
    std::set<storm::RationalFunctionVariable> variableSet;
 
    void wellformedRequiresNonNegativeEntries(std::vector<ValueType> const&);
 
   public:
    ConstraintCollector(storm::models::sparse::Model<ValueType> const& model);

    std::unordered_set<typename ConstraintType<ValueType>::val> const& getWellformedConstraints() const;

    std::unordered_set<typename ConstraintType<ValueType>::val> const& getGraphPreservingConstraints() const;

    std::set<storm::RationalFunctionVariable> const& getVariables() const;

    void process(storm::models::sparse::Model<ValueType> const& model);

    void operator()(storm::models::sparse::Model<ValueType> const& model);
};
 
}  // namespace analysis
}  // namespace storm