tempest/src/storm/transformer/SymbolicToSparseTransformer.cpp

#include "SymbolicToSparseTransformer.h"

#include "storm/storage/dd/DdManager.h"
#include "storm/storage/dd/Add.h"
#include "storm/storage/dd/Bdd.h"
#include "storm/storage/sparse/ModelComponents.h"
#include "storm/models/symbolic/StandardRewardModel.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/utility/macros.h"
#include "storm/exceptions/NotImplementedException.h"
#include "storm/logic/AtomicExpressionFormula.h"
#include "storm/logic/AtomicLabelFormula.h"

namespace storm {
    namespace transformer {

        struct LabelInformation {
            LabelInformation(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
                for (auto const& formula : formulas) {
                    std::vector<std::shared_ptr<storm::logic::AtomicLabelFormula const>> atomicLabelFormulas = formula->getAtomicLabelFormulas();
                    for (auto const& labelFormula : atomicLabelFormulas) {
                        atomicLabels.insert(labelFormula->getLabel());
                    }
                    
                    std::vector<std::shared_ptr<storm::logic::AtomicExpressionFormula const>> atomicExpressionFormulas = formula->getAtomicExpressionFormulas();
                    for (auto const& expressionFormula : atomicExpressionFormulas) {
                        std::stringstream ss;
                        ss << expressionFormula->getExpression();
                        expressionLabels[ss.str()] = expressionFormula->getExpression();
                    }
                }
            }
            
            std::set<std::string> atomicLabels;
            std::map<std::string, storm::expressions::Expression> expressionLabels;
        };
        
        template<storm::dd::DdType Type, typename ValueType>
        std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> SymbolicDtmcToSparseDtmcTransformer<Type, ValueType>::translate(storm::models::symbolic::Dtmc<Type, ValueType> const& symbolicDtmc, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
            
            this->odd = symbolicDtmc.getReachableStates().createOdd();
            storm::storage::SparseMatrix<ValueType> transitionMatrix = symbolicDtmc.getTransitionMatrix().toMatrix(this->odd, this->odd);
            std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<ValueType>> rewardModels;
            for (auto const& rewardModelNameAndModel : symbolicDtmc.getRewardModels()) {
                boost::optional<std::vector<ValueType>> stateRewards;
                boost::optional<std::vector<ValueType>> stateActionRewards;
                boost::optional<storm::storage::SparseMatrix<ValueType>> transitionRewards;
                if (rewardModelNameAndModel.second.hasStateRewards()) {
                    stateRewards = rewardModelNameAndModel.second.getStateRewardVector().toVector(this->odd);
                }
                if (rewardModelNameAndModel.second.hasStateActionRewards()) {
                    stateActionRewards = rewardModelNameAndModel.second.getStateActionRewardVector().toVector(this->odd);
                }
                if (rewardModelNameAndModel.second.hasTransitionRewards()) {
                    transitionRewards = rewardModelNameAndModel.second.getTransitionRewardMatrix().toMatrix(this->odd, this->odd);
                }
                rewardModels.emplace(rewardModelNameAndModel.first,storm::models::sparse::StandardRewardModel<ValueType>(stateRewards, stateActionRewards, transitionRewards));
            }
            storm::models::sparse::StateLabeling labelling(transitionMatrix.getRowGroupCount());
            
            labelling.addLabel("init", symbolicDtmc.getInitialStates().toVector(this->odd));
            labelling.addLabel("deadlock", symbolicDtmc.getDeadlockStates().toVector(this->odd));
            if (formulas.empty()) {
                for (auto const& label : symbolicDtmc.getLabels()) {
                    labelling.addLabel(label, symbolicDtmc.getStates(label).toVector(this->odd));
                }
            } else {
                LabelInformation labelInfo(formulas);
                for (auto const& label : labelInfo.atomicLabels) {
                    labelling.addLabel(label, symbolicDtmc.getStates(label).toVector(this->odd));
                }
                for (auto const& expressionLabel : labelInfo.expressionLabels) {
                    labelling.addLabel(expressionLabel.first, symbolicDtmc.getStates(expressionLabel.second).toVector(this->odd));
                }
            }
            return std::make_shared<storm::models::sparse::Dtmc<ValueType>>(transitionMatrix, labelling, rewardModels);
        }
        
        template<storm::dd::DdType Type, typename ValueType>
        storm::dd::Odd const& SymbolicDtmcToSparseDtmcTransformer<Type, ValueType>::getOdd() const {
            return this->odd;
        }
        
        template<storm::dd::DdType Type, typename ValueType>
        std::shared_ptr<storm::models::sparse::Mdp<ValueType>> SymbolicMdpToSparseMdpTransformer<Type, ValueType>::translate(storm::models::symbolic::Mdp<Type, ValueType> const& symbolicMdp, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
            storm::dd::Odd odd = symbolicMdp.getReachableStates().createOdd();
            
            // Collect action reward vectors that need translation
            std::vector<storm::dd::Add<Type, ValueType>> symbolicActionRewardVectors;
            std::map<std::string, uint64_t> rewardNameToActionRewardIndexMap;
            for (auto const& rewardModelNameAndModel : symbolicMdp.getRewardModels()) {
                if (rewardModelNameAndModel.second.hasStateActionRewards()) {
                    rewardNameToActionRewardIndexMap.emplace(rewardModelNameAndModel.first, symbolicActionRewardVectors.size());
                    symbolicActionRewardVectors.push_back(rewardModelNameAndModel.second.getStateActionRewardVector());
                }
            }
            // Build transition matrix and (potentially) actionRewardVectors.
            storm::storage::SparseMatrix<ValueType> transitionMatrix;
            std::vector<std::vector<ValueType>> actionRewardVectors;
            if (symbolicActionRewardVectors.empty()) {
                transitionMatrix = symbolicMdp.getTransitionMatrix().toMatrix(symbolicMdp.getNondeterminismVariables(), odd, odd);
            } else {
                auto matrRewards = symbolicMdp.getTransitionMatrix().toMatrixVectors(symbolicActionRewardVectors, symbolicMdp.getNondeterminismVariables(), odd, odd);
                transitionMatrix = std::move(matrRewards.first);
                actionRewardVectors = std::move(matrRewards.second);
            }
            
            // Translate reward models
            std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<ValueType>> rewardModels;
            for (auto const& rewardModelNameAndModel : symbolicMdp.getRewardModels()) {
                boost::optional<std::vector<ValueType>> stateRewards;
                boost::optional<std::vector<ValueType>> stateActionRewards;
                boost::optional<storm::storage::SparseMatrix<ValueType>> transitionRewards;
                if (rewardModelNameAndModel.second.hasStateRewards()) {
                    stateRewards = rewardModelNameAndModel.second.getStateRewardVector().toVector(odd);
                }
                auto actRewIndexIt = rewardNameToActionRewardIndexMap.find(rewardModelNameAndModel.first);
                if (actRewIndexIt != rewardNameToActionRewardIndexMap.end()) {
                    stateActionRewards = std::move(actionRewardVectors[actRewIndexIt->second]);
                }
                STORM_LOG_THROW(!rewardModelNameAndModel.second.hasTransitionRewards(), storm::exceptions::NotImplementedException, "Translation of symbolic to explicit transition rewards is not yet supported.");
                rewardModels.emplace(rewardModelNameAndModel.first, storm::models::sparse::StandardRewardModel<ValueType>(stateRewards, stateActionRewards, transitionRewards));
            }

            storm::models::sparse::StateLabeling labelling(transitionMatrix.getRowGroupCount());

            labelling.addLabel("init", symbolicMdp.getInitialStates().toVector(odd));
            labelling.addLabel("deadlock", symbolicMdp.getDeadlockStates().toVector(odd));
            if (formulas.empty()) {
                for (auto const& label : symbolicMdp.getLabels()) {
                    labelling.addLabel(label, symbolicMdp.getStates(label).toVector(odd));
                }
            } else {
                LabelInformation labelInfo(formulas);
                for (auto const& label : labelInfo.atomicLabels) {
                    labelling.addLabel(label, symbolicMdp.getStates(label).toVector(odd));
                }
                for (auto const& expressionLabel : labelInfo.expressionLabels) {
                    labelling.addLabel(expressionLabel.first, symbolicMdp.getStates(expressionLabel.second).toVector(odd));
                }
            }
            
            return std::make_shared<storm::models::sparse::Mdp<ValueType>>(transitionMatrix, labelling, rewardModels);
        }

        template<storm::dd::DdType Type, typename ValueType>
        std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> SymbolicCtmcToSparseCtmcTransformer<Type, ValueType>::translate(storm::models::symbolic::Ctmc<Type, ValueType> const& symbolicCtmc, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
            storm::dd::Odd odd = symbolicCtmc.getReachableStates().createOdd();
            storm::storage::SparseMatrix<ValueType> transitionMatrix = symbolicCtmc.getTransitionMatrix().toMatrix(odd, odd);
            std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<ValueType>> rewardModels;
            for (auto const& rewardModelNameAndModel : symbolicCtmc.getRewardModels()) {
                boost::optional<std::vector<ValueType>> stateRewards;
                boost::optional<std::vector<ValueType>> stateActionRewards;
                boost::optional<storm::storage::SparseMatrix<ValueType>> transitionRewards;
                if (rewardModelNameAndModel.second.hasStateRewards()) {
                    stateRewards = rewardModelNameAndModel.second.getStateRewardVector().toVector(odd);
                }
                if (rewardModelNameAndModel.second.hasStateActionRewards()) {
                    stateActionRewards = rewardModelNameAndModel.second.getStateActionRewardVector().toVector(odd);
                }
                if (rewardModelNameAndModel.second.hasTransitionRewards()) {
                    transitionRewards = rewardModelNameAndModel.second.getTransitionRewardMatrix().toMatrix(odd, odd);
                }
                rewardModels.emplace(rewardModelNameAndModel.first,storm::models::sparse::StandardRewardModel<ValueType>(stateRewards, stateActionRewards, transitionRewards));
            }
            storm::models::sparse::StateLabeling labelling(transitionMatrix.getRowGroupCount());

            labelling.addLabel("init", symbolicCtmc.getInitialStates().toVector(odd));
            labelling.addLabel("deadlock", symbolicCtmc.getDeadlockStates().toVector(odd));
            if (formulas.empty()) {
                for (auto const& label : symbolicCtmc.getLabels()) {
                    labelling.addLabel(label, symbolicCtmc.getStates(label).toVector(odd));
                }
            } else {
                LabelInformation labelInfo(formulas);
                for (auto const& label : labelInfo.atomicLabels) {
                    labelling.addLabel(label, symbolicCtmc.getStates(label).toVector(odd));
                }
                for (auto const& expressionLabel : labelInfo.expressionLabels) {
                    labelling.addLabel(expressionLabel.first, symbolicCtmc.getStates(expressionLabel.second).toVector(odd));
                }
            }
            
            return std::make_shared<storm::models::sparse::Ctmc<ValueType>>(transitionMatrix, labelling, rewardModels);
        }
        
        
        template<storm::dd::DdType Type, typename ValueType>
        std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> SymbolicMaToSparseMaTransformer<Type, ValueType>::translate(storm::models::symbolic::MarkovAutomaton<Type, ValueType> const& symbolicMa, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
            storm::dd::Odd odd = symbolicMa.getReachableStates().createOdd();
            // Collect action reward vectors that need translation
            std::vector<storm::dd::Add<Type, ValueType>> symbolicActionRewardVectors;
            std::map<std::string, uint64_t> rewardNameToActionRewardIndexMap;
            for (auto const& rewardModelNameAndModel : symbolicMa.getRewardModels()) {
                if (rewardModelNameAndModel.second.hasStateActionRewards()) {
                    rewardNameToActionRewardIndexMap.emplace(rewardModelNameAndModel.first, symbolicActionRewardVectors.size());
                    symbolicActionRewardVectors.push_back(rewardModelNameAndModel.second.getStateActionRewardVector());
                }
            }
            // Build transition matrix and (potentially) actionRewardVectors.
            storm::storage::SparseMatrix<ValueType> transitionMatrix;
            std::vector<std::vector<ValueType>> actionRewardVectors;
            if (symbolicActionRewardVectors.empty()) {
                transitionMatrix = symbolicMa.getTransitionMatrix().toMatrix(symbolicMa.getNondeterminismVariables(), odd, odd);
            } else {
                auto matrRewards = symbolicMa.getTransitionMatrix().toMatrixVectors(symbolicActionRewardVectors, symbolicMa.getNondeterminismVariables(), odd, odd);
                transitionMatrix = std::move(matrRewards.first);
                actionRewardVectors = std::move(matrRewards.second);
            }
            
            // Translate reward models
            std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<ValueType>> rewardModels;
            for (auto const& rewardModelNameAndModel : symbolicMa.getRewardModels()) {
                boost::optional<std::vector<ValueType>> stateRewards;
                boost::optional<std::vector<ValueType>> stateActionRewards;
                boost::optional<storm::storage::SparseMatrix<ValueType>> transitionRewards;
                if (rewardModelNameAndModel.second.hasStateRewards()) {
                    stateRewards = rewardModelNameAndModel.second.getStateRewardVector().toVector(odd);
                }
                auto actRewIndexIt = rewardNameToActionRewardIndexMap.find(rewardModelNameAndModel.first);
                if (actRewIndexIt != rewardNameToActionRewardIndexMap.end()) {
                    stateActionRewards = std::move(actionRewardVectors[actRewIndexIt->second]);
                }
                STORM_LOG_THROW(!rewardModelNameAndModel.second.hasTransitionRewards(), storm::exceptions::NotImplementedException, "Translation of symbolic to explicit transition rewards is not yet supported.");
                rewardModels.emplace(rewardModelNameAndModel.first, storm::models::sparse::StandardRewardModel<ValueType>(stateRewards, stateActionRewards, transitionRewards));
            }

            storm::models::sparse::StateLabeling labelling(transitionMatrix.getRowGroupCount());

            labelling.addLabel("init", symbolicMa.getInitialStates().toVector(odd));
            labelling.addLabel("deadlock", symbolicMa.getDeadlockStates().toVector(odd));
            if (formulas.empty()) {
                for (auto const& label : symbolicMa.getLabels()) {
                    labelling.addLabel(label, symbolicMa.getStates(label).toVector(odd));
                }
            } else {
                LabelInformation labelInfo(formulas);
                for (auto const& label : labelInfo.atomicLabels) {
                    labelling.addLabel(label, symbolicMa.getStates(label).toVector(odd));
                }
                for (auto const& expressionLabel : labelInfo.expressionLabels) {
                    labelling.addLabel(expressionLabel.first, symbolicMa.getStates(expressionLabel.second).toVector(odd));
                }
            }
            storm::storage::BitVector markovianStates = symbolicMa.getMarkovianStates().toVector(odd);
            storm::storage::sparse::ModelComponents<ValueType> components(std::move(transitionMatrix), std::move(labelling), std::move(rewardModels), false, std::move(markovianStates));
            components.exitRates = symbolicMa.getExitRateVector().toVector(odd);
            
            return std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(components));
        }
        

        template class SymbolicDtmcToSparseDtmcTransformer<storm::dd::DdType::CUDD, double>;
        template class SymbolicDtmcToSparseDtmcTransformer<storm::dd::DdType::Sylvan, double>;
        template class SymbolicDtmcToSparseDtmcTransformer<storm::dd::DdType::Sylvan, storm::RationalNumber>;
        template class SymbolicDtmcToSparseDtmcTransformer<storm::dd::DdType::Sylvan, storm::RationalFunction>;
        
        template class SymbolicMdpToSparseMdpTransformer<storm::dd::DdType::CUDD, double>;
        template class SymbolicMdpToSparseMdpTransformer<storm::dd::DdType::Sylvan, double>;
        template class SymbolicMdpToSparseMdpTransformer<storm::dd::DdType::Sylvan, storm::RationalNumber>;
        template class SymbolicMdpToSparseMdpTransformer<storm::dd::DdType::Sylvan, storm::RationalFunction>;

        template class SymbolicCtmcToSparseCtmcTransformer<storm::dd::DdType::CUDD, double>;
        template class SymbolicCtmcToSparseCtmcTransformer<storm::dd::DdType::Sylvan, double>;
        template class SymbolicCtmcToSparseCtmcTransformer<storm::dd::DdType::Sylvan, storm::RationalNumber>;
        template class SymbolicCtmcToSparseCtmcTransformer<storm::dd::DdType::Sylvan, storm::RationalFunction>;

        template class SymbolicMaToSparseMaTransformer<storm::dd::DdType::CUDD, double>;
        template class SymbolicMaToSparseMaTransformer<storm::dd::DdType::Sylvan, double>;
        template class SymbolicMaToSparseMaTransformer<storm::dd::DdType::Sylvan, storm::RationalNumber>;
        template class SymbolicMaToSparseMaTransformer<storm::dd::DdType::Sylvan, storm::RationalFunction>;

    }
}