ModelInstantiator.h

Go to the documentation of this file.

#pragma once
 
#include <memory>
#include <type_traits>
#include <unordered_map>
 
#include "storm-pars/transformer/BigStep.h"
#include "storm-pars/utility/parametric.h"
#include "storm/models/sparse/Ctmc.h"
#include "storm/models/sparse/Dtmc.h"
#include "storm/models/sparse/MarkovAutomaton.h"
#include "storm/models/sparse/Mdp.h"
#include "storm/models/sparse/StochasticTwoPlayerGame.h"
#include "storm/utility/constants.h"
 
namespace storm {
namespace utility {

template<typename ParametricSparseModelType, typename ConstantSparseModelType>
class ModelInstantiator {
   public:
    typedef typename ParametricSparseModelType::ValueType ParametricType;
    typedef typename storm::utility::parametric::VariableType<ParametricType>::type VariableType;
    typedef typename storm::utility::parametric::CoefficientType<ParametricType>::type CoefficientType;
    typedef typename ConstantSparseModelType::ValueType ConstantType;

    ModelInstantiator(ParametricSparseModelType const& parametricModel);

    virtual ~ModelInstantiator();

    ConstantSparseModelType const& instantiate(storm::utility::parametric::Valuation<ParametricType> const& valuation);

    void checkValid() const;
 
   private:
    template<typename PMT = ParametricSparseModelType>
    typename std::enable_if<std::is_same<PMT, storm::models::sparse::Dtmc<typename ParametricSparseModelType::ValueType>>::value ||
                            std::is_same<PMT, storm::models::sparse::Mdp<typename ParametricSparseModelType::ValueType>>::value>::type
    initializeModelSpecificData(PMT const& parametricModel) {
        storm::storage::sparse::ModelComponents<ConstantType, typename ConstantSparseModelType::RewardModelType> components(
            buildDummyMatrix(parametricModel.getTransitionMatrix()));
        components.stateLabeling = parametricModel.getStateLabeling();
        components.rewardModels = buildDummyRewardModels(parametricModel.getRewardModels());
        components.choiceLabeling = parametricModel.getOptionalChoiceLabeling();
 
        this->instantiatedModel = std::make_shared<ConstantSparseModelType>(std::move(components));
    }
 
    template<typename PMT = ParametricSparseModelType>
    typename std::enable_if<std::is_same<PMT, storm::models::sparse::Ctmc<typename ParametricSparseModelType::ValueType>>::value>::type
    initializeModelSpecificData(PMT const& parametricModel) {
        storm::storage::sparse::ModelComponents<ConstantType, typename ConstantSparseModelType::RewardModelType> components(
            buildDummyMatrix(parametricModel.getTransitionMatrix()));
        components.stateLabeling = parametricModel.getStateLabeling();
        components.rewardModels = buildDummyRewardModels(parametricModel.getRewardModels());
        components.exitRates = std::vector<ConstantType>(parametricModel.getExitRateVector().size(), storm::utility::one<ConstantType>());
        components.rateTransitions = true;
        components.choiceLabeling = parametricModel.getOptionalChoiceLabeling();
        this->instantiatedModel = std::make_shared<ConstantSparseModelType>(std::move(components));
 
        initializeVectorMapping(this->instantiatedModel->getExitRateVector(), this->functions, this->vectorMapping, parametricModel.getExitRateVector());
    }
 
    template<typename PMT = ParametricSparseModelType>
    typename std::enable_if<std::is_same<PMT, storm::models::sparse::MarkovAutomaton<typename ParametricSparseModelType::ValueType>>::value>::type
    initializeModelSpecificData(PMT const& parametricModel) {
        storm::storage::sparse::ModelComponents<ConstantType, typename ConstantSparseModelType::RewardModelType> components(
            buildDummyMatrix(parametricModel.getTransitionMatrix()));
        components.stateLabeling = parametricModel.getStateLabeling();
        components.rewardModels = buildDummyRewardModels(parametricModel.getRewardModels());
        components.exitRates = std::vector<ConstantType>(parametricModel.getExitRates().size(), storm::utility::one<ConstantType>());
        components.markovianStates = parametricModel.getMarkovianStates();
        components.choiceLabeling = parametricModel.getOptionalChoiceLabeling();
        this->instantiatedModel = std::make_shared<ConstantSparseModelType>(std::move(components));
 
        initializeVectorMapping(this->instantiatedModel->getExitRates(), this->functions, this->vectorMapping, parametricModel.getExitRates());
    }
 
    template<typename PMT = ParametricSparseModelType>
    typename std::enable_if<std::is_same<PMT, storm::models::sparse::StochasticTwoPlayerGame<typename ParametricSparseModelType::ValueType>>::value>::type
    initializeModelSpecificData(PMT const& parametricModel) {
        storm::storage::sparse::ModelComponents<ConstantType, typename ConstantSparseModelType::RewardModelType> components(
            buildDummyMatrix(parametricModel.getTransitionMatrix()));
        components.stateLabeling = parametricModel.getStateLabeling();
        components.rewardModels = buildDummyRewardModels(parametricModel.getRewardModels());
        components.player1Matrix = parametricModel.getPlayer1Matrix();
        components.choiceLabeling = parametricModel.getOptionalChoiceLabeling();
 
        this->instantiatedModel = std::make_shared<ConstantSparseModelType>(std::move(components));
    }
 
    template<typename PMT = ParametricSparseModelType>
    typename std::enable_if<std::is_same<PMT, ConstantSparseModelType>::value>::type instantiate_helper(
        storm::utility::parametric::Valuation<ParametricType> const& valuation) {
        for (auto& functionResult : this->functions) {
            functionResult.second = storm::utility::parametric::substitute(functionResult.first, valuation);
        }
    }
 
    template<typename PMT = ParametricSparseModelType>
    typename std::enable_if<!std::is_same<PMT, ConstantSparseModelType>::value>::type instantiate_helper(
        storm::utility::parametric::Valuation<ParametricType> const& valuation) {
        for (auto& functionResult : this->functions) {
            if (!transformer::BigStep::lastSavedAnnotations.empty() && functionResult.first.gatherVariables().size() == 1 &&
                transformer::BigStep::lastSavedAnnotations.count(functionResult.first)) {
                auto const& annotation = transformer::BigStep::lastSavedAnnotations.at(functionResult.first);
                functionResult.second = annotation.evaluate(storm::utility::convertNumber<ConstantType>(valuation.at(annotation.getParameter())));
            } else {
                functionResult.second = storm::utility::parametric::evaluate<ConstantType>(functionResult.first, valuation);
            }
        }
    }

    storm::storage::SparseMatrix<ConstantType> buildDummyMatrix(storm::storage::SparseMatrix<ParametricType> const& parametricMatrix) const;

    std::unordered_map<std::string, typename ConstantSparseModelType::RewardModelType> buildDummyRewardModels(
        std::unordered_map<std::string, typename ParametricSparseModelType::RewardModelType> const& parametricRewardModel) const;

    void initializeMatrixMapping(storm::storage::SparseMatrix<ConstantType>& constantMatrix, std::unordered_map<ParametricType, ConstantType>& functions,
                                 std::vector<std::pair<typename storm::storage::SparseMatrix<ConstantType>::iterator, ConstantType*>>& mapping,
                                 storm::storage::SparseMatrix<ParametricType> const& parametricMatrix) const;

    void initializeVectorMapping(std::vector<ConstantType>& constantVector, std::unordered_map<ParametricType, ConstantType>& functions,
                                 std::vector<std::pair<typename std::vector<ConstantType>::iterator, ConstantType*>>& mapping,
                                 std::vector<ParametricType> const& parametricVector) const;

    std::shared_ptr<ConstantSparseModelType> instantiatedModel;
    std::unordered_map<ParametricType, ConstantType> functions;
    std::vector<std::pair<typename storm::storage::SparseMatrix<ConstantType>::iterator, ConstantType*>> matrixMapping;
    std::vector<std::pair<typename std::vector<ConstantType>::iterator, ConstantType*>> vectorMapping;
};
}  // Namespace utility
}  // namespace storm