You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
50 lines
2.5 KiB
50 lines
2.5 KiB
#include "src/parser/NondeterministicModelParser.h"
|
|
|
|
#include <string>
|
|
#include <vector>
|
|
|
|
#include "src/parser/NondeterministicSparseTransitionParser.h"
|
|
#include "src/parser/AtomicPropositionLabelingParser.h"
|
|
#include "src/parser/SparseStateRewardParser.h"
|
|
|
|
namespace storm {
|
|
namespace parser {
|
|
|
|
NondeterministicModelParser::Result NondeterministicModelParser::parseNondeterministicModel(std::string const & transitionsFilename, std::string const & labelingFilename, std::string const & stateRewardFilename, std::string const & transitionRewardFilename) {
|
|
|
|
// Parse the transitions.
|
|
storm::storage::SparseMatrix<double> transitions(std::move(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions(transitionsFilename)));
|
|
|
|
uint_fast64_t stateCount = transitions.getColumnCount();
|
|
|
|
// Parse the state labeling.
|
|
storm::models::sparse::StateLabeling labeling(std::move(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(stateCount, labelingFilename)));
|
|
|
|
// Only parse state rewards if a file is given.
|
|
boost::optional<std::vector<double>> stateRewards;
|
|
if (stateRewardFilename != "") {
|
|
stateRewards = storm::parser::SparseStateRewardParser::parseSparseStateReward(stateCount, stateRewardFilename);
|
|
}
|
|
|
|
// Only parse transition rewards if a file is given.
|
|
boost::optional<storm::storage::SparseMatrix<double>> transitionRewards;
|
|
if (transitionRewardFilename != "") {
|
|
transitionRewards = storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitionRewards(transitionRewardFilename, transitions);
|
|
}
|
|
|
|
// Construct the result.
|
|
Result result(std::move(transitions), std::move(labeling));
|
|
result.stateRewards = stateRewards;
|
|
result.transitionRewards = transitionRewards;
|
|
|
|
return result;
|
|
}
|
|
|
|
storm::models::sparse::Mdp<double> NondeterministicModelParser::parseMdp(std::string const & transitionsFilename, std::string const & labelingFilename, std::string const & stateRewardFilename, std::string const & transitionRewardFilename) {
|
|
|
|
Result parserResult = parseNondeterministicModel(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename);
|
|
return storm::models::sparse::Mdp<double>(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>());
|
|
}
|
|
|
|
} /* namespace parser */
|
|
} /* namespace storm */
|