DftInstantiator.h

Go to the documentation of this file.

#pragma once
 
#include "storm-dft/storage/DFT.h"
#include "storm-pars/utility/parametric.h"
 
namespace storm::dft {
namespace transformations {
 
template<typename ParametricType, typename ConstantType>
class DftInstantiator {
   public:
    DftInstantiator(storm::dft::storage::DFT<ParametricType> const& dft);
 
    virtual ~DftInstantiator() = default;
 
    std::shared_ptr<storm::dft::storage::DFT<ConstantType>> instantiate(storm::utility::parametric::Valuation<ParametricType> const& valuation);
 
    void checkValid() const;
 
   private:
    storm::dft::storage::DFT<ParametricType> const& dft;
 
    template<typename PT = ParametricType>
    typename std::enable_if<std::is_same<PT, ConstantType>::value, ConstantType>::type instantiate_helper(
        ParametricType const& function, storm::utility::parametric::Valuation<ParametricType> const& valuation) {
        return storm::utility::parametric::substitute(function, valuation);
    }
 
    template<typename PT = ParametricType>
    typename std::enable_if<!std::is_same<PT, ConstantType>::value, ConstantType>::type instantiate_helper(
        ParametricType const& function, storm::utility::parametric::Valuation<ParametricType> const& valuation) {
        return storm::utility::convertNumber<ConstantType>(storm::utility::parametric::evaluate(function, valuation));
    }
 
    std::vector<std::string> getChildrenVector(std::shared_ptr<storm::dft::storage::elements::DFTElement<ParametricType> const> element);
};
 
}  // namespace transformations
}  // namespace storm::dft