DeterministicModelParser.cpp

Go to the documentation of this file.

#include "storm-parsers/parser/DeterministicModelParser.h"
 
#include <string>
#include <vector>
 
#include "storm/models/sparse/StandardRewardModel.h"
 
#include "storm-parsers/parser/DeterministicSparseTransitionParser.h"
#include "storm-parsers/parser/SparseItemLabelingParser.h"
#include "storm-parsers/parser/SparseStateRewardParser.h"
 
#include "storm/adapters/RationalFunctionAdapter.h"
 
namespace storm {
namespace parser {
 
template<typename ValueType, typename RewardValueType>
storm::storage::sparse::ModelComponents<ValueType, storm::models::sparse::StandardRewardModel<RewardValueType>>
DeterministicModelParser<ValueType, RewardValueType>::parseDeterministicModel(std::string const& transitionsFilename, std::string const& labelingFilename,
                                                                              std::string const& stateRewardFilename,
                                                                              std::string const& transitionRewardFilename,
                                                                              std::string const& choiceLabelingFilename) {
    // Parse the transitions.
    storm::storage::SparseMatrix<ValueType> transitions(
        std::move(storm::parser::DeterministicSparseTransitionParser<ValueType>::parseDeterministicTransitions(transitionsFilename)));
 
    uint_fast64_t stateCount = transitions.getColumnCount();
 
    // Parse the state labeling.
    storm::models::sparse::StateLabeling labeling(storm::parser::SparseItemLabelingParser::parseAtomicPropositionLabeling(stateCount, labelingFilename));
 
    // Construct the result.
    storm::storage::sparse::ModelComponents<ValueType, storm::models::sparse::StandardRewardModel<RewardValueType>> result(std::move(transitions),
                                                                                                                           std::move(labeling));
 
    // Only parse state rewards if a file is given.
    std::optional<std::vector<RewardValueType>> stateRewards;
    if (stateRewardFilename != "") {
        stateRewards = storm::parser::SparseStateRewardParser<RewardValueType>::parseSparseStateReward(stateCount, stateRewardFilename);
    }
 
    // Only parse transition rewards if a file is given.
    std::optional<storm::storage::SparseMatrix<RewardValueType>> transitionRewards;
    if (transitionRewardFilename != "") {
        transitionRewards = storm::parser::DeterministicSparseTransitionParser<RewardValueType>::parseDeterministicTransitionRewards(transitionRewardFilename,
                                                                                                                                     result.transitionMatrix);
    }
 
    if (stateRewards || transitionRewards) {
        result.rewardModels.insert(std::make_pair(
            "", storm::models::sparse::StandardRewardModel<RewardValueType>(std::move(stateRewards), std::nullopt, std::move(transitionRewards))));
    }
 
    // Only parse choice labeling if a file is given.
    std::optional<storm::models::sparse::ChoiceLabeling> choiceLabeling;
    if (!choiceLabelingFilename.empty()) {
        result.choiceLabeling = storm::parser::SparseItemLabelingParser::parseChoiceLabeling(result.transitionMatrix.getRowCount(), choiceLabelingFilename);
    }
 
    return result;
}
 
template<typename ValueType, typename RewardValueType>
storm::models::sparse::Dtmc<ValueType, storm::models::sparse::StandardRewardModel<RewardValueType>>
DeterministicModelParser<ValueType, RewardValueType>::parseDtmc(std::string const& transitionsFilename, std::string const& labelingFilename,
                                                                std::string const& stateRewardFilename, std::string const& transitionRewardFilename,
                                                                std::string const& choiceLabelingFilename) {
    auto parserResult = parseDeterministicModel(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename, choiceLabelingFilename);
    return storm::models::sparse::Dtmc<ValueType, storm::models::sparse::StandardRewardModel<RewardValueType>>(std::move(parserResult));
}
 
template<typename ValueType, typename RewardValueType>
storm::models::sparse::Ctmc<ValueType, storm::models::sparse::StandardRewardModel<RewardValueType>>
DeterministicModelParser<ValueType, RewardValueType>::parseCtmc(std::string const& transitionsFilename, std::string const& labelingFilename,
                                                                std::string const& stateRewardFilename, std::string const& transitionRewardFilename,
                                                                std::string const& choiceLabelingFilename) {
    auto parserResult = parseDeterministicModel(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename, choiceLabelingFilename);
    parserResult.rateTransitions = true;
    return storm::models::sparse::Ctmc<ValueType, storm::models::sparse::StandardRewardModel<RewardValueType>>(std::move(parserResult));
}
 
template class DeterministicModelParser<double, double>;
 
#ifdef STORM_HAVE_CARL
template class DeterministicModelParser<double, storm::Interval>;
#endif
 
} /* namespace parser */
} /* namespace storm */