Browse Source

DRN parser now supports state rewards

tempestpy_adaptions
TimQu 7 years ago
parent
commit
73b23e133e
  1. 23
      src/storm/parser/DirectEncodingParser.cpp

23
src/storm/parser/DirectEncodingParser.cpp

@ -122,7 +122,8 @@ namespace storm {
bool nonDeterministic = (type == storm::models::ModelType::Mdp || type == storm::models::ModelType::MarkovAutomaton);
storm::storage::SparseMatrixBuilder<ValueType> builder = storm::storage::SparseMatrixBuilder<ValueType>(0, 0, 0, false, nonDeterministic, 0);
modelComponents->stateLabeling = storm::models::sparse::StateLabeling(stateSize);
std::vector<std::vector<ValueType>> stateRewards;
// We parse rates for continuous time models.
if (type == storm::models::ModelType::Ctmc) {
modelComponents->rateTransitions = true;
@ -156,10 +157,18 @@ namespace storm {
// Rewards found
size_t posEndReward = line.find(']');
STORM_LOG_THROW(posEndReward != std::string::npos, storm::exceptions::WrongFormatException, "] missing.");
std::string rewards = line.substr(1, posEndReward-1);
STORM_LOG_TRACE("State rewards: " << rewards);
// TODO import rewards
STORM_LOG_WARN("Rewards were not imported");
std::string rewardsStr = line.substr(1, posEndReward-1);
STORM_LOG_TRACE("State rewards: " << rewardsStr);
std::vector<std::string> rewards;
boost::split(rewards, rewardsStr, boost::is_any_of(","));
if (stateRewards.size() < rewards.size()) {
stateRewards.resize(rewards.size(), std::vector<ValueType>(stateSize, storm::utility::zero<ValueType>()));
}
auto stateRewardsIt = stateRewards.begin();
for (auto const& rew : rewards) {
(*stateRewardsIt)[state] = valueParser.parseValue(rew);
++stateRewardsIt;
}
line = line.substr(posEndReward+1);
}
// Check for labels
@ -198,6 +207,7 @@ namespace storm {
STORM_LOG_THROW(posEndReward != std::string::npos, storm::exceptions::WrongFormatException, "] missing.");
std::string rewards = line.substr(1, posEndReward-1);
STORM_LOG_TRACE("Transition rewards: " << rewards);
STORM_LOG_WARN("Transition rewards [" << rewards << "] not parsed.");
// TODO save rewards
line = line.substr(posEndReward+1);
}
@ -217,6 +227,9 @@ namespace storm {
STORM_LOG_TRACE("Finished parsing");
modelComponents->transitionMatrix = builder.build(row + 1, stateSize, nonDeterministic ? stateSize : 0);
for (uint64_t i = 0; i < stateRewards.size(); ++i) {
modelComponents->rewardModels.emplace("rew" + std::to_string(i), storm::models::sparse::StandardRewardModel<ValueType>(std::move(stateRewards[i])));
}
STORM_LOG_TRACE("Built matrix");
return modelComponents;
}

Loading…
Cancel
Save