BinaryDtmcTransformer.h

Go to the documentation of this file.

#pragma once
 
#include "storm/models/sparse/Dtmc.h"
#include "storm/models/sparse/StandardRewardModel.h"
 
namespace storm {
namespace transformer {
 
class BinaryDtmcTransformer {
   public:
    BinaryDtmcTransformer() = default;
 
    std::shared_ptr<storm::models::sparse::Dtmc<RationalFunction>> transform(storm::models::sparse::Dtmc<RationalFunction> const& dtmc,
                                                                             bool keepStateValuations = false) const;
 
   private:
    struct TransformationData {
        storm::storage::SparseMatrix<RationalFunction> simpleMatrix;
        std::vector<uint64_t> simpleStateToOriginalState;
    };
 
    TransformationData transformTransitions(storm::models::sparse::Dtmc<RationalFunction> const& dtmc) const;
    storm::models::sparse::StateLabeling transformStateLabeling(storm::models::sparse::Dtmc<RationalFunction> const& dtmc,
                                                                TransformationData const& data) const;
    storm::models::sparse::StandardRewardModel<RationalFunction> transformRewardModel(
        storm::models::sparse::Dtmc<RationalFunction> const& dtmc, storm::models::sparse::StandardRewardModel<RationalFunction> const& rewardModel,
        TransformationData const& data) const;
    storm::models::sparse::ChoiceLabeling transformChoiceLabeling(storm::models::sparse::Dtmc<RationalFunction> const& dtmc,
                                                                  TransformationData const& data) const;
};
}  // namespace transformer
}  // namespace storm