|
@ -66,7 +66,7 @@ namespace storm { |
|
|
if (line != "") { |
|
|
if (line != "") { |
|
|
std::vector<std::string> parameters; |
|
|
std::vector<std::string> parameters; |
|
|
boost::split(parameters, line, boost::is_any_of(" ")); |
|
|
boost::split(parameters, line, boost::is_any_of(" ")); |
|
|
for (std::string parameter : parameters) { |
|
|
|
|
|
|
|
|
for (std::string const& parameter : parameters) { |
|
|
STORM_LOG_TRACE("New parameter: " << parameter); |
|
|
STORM_LOG_TRACE("New parameter: " << parameter); |
|
|
valueParser.addParameter(parameter); |
|
|
valueParser.addParameter(parameter); |
|
|
} |
|
|
} |
|
@ -75,7 +75,7 @@ namespace storm { |
|
|
|
|
|
|
|
|
} else if (line == "@reward_models") { |
|
|
} else if (line == "@reward_models") { |
|
|
// Parse reward models
|
|
|
// Parse reward models
|
|
|
STORM_LOG_THROW(rewardModelNames.size() == 0, storm::exceptions::WrongFormatException, "Reward model names declared twice"); |
|
|
|
|
|
|
|
|
STORM_LOG_THROW(rewardModelNames.empty(), storm::exceptions::WrongFormatException, "Reward model names declared twice"); |
|
|
std::getline(file, line); |
|
|
std::getline(file, line); |
|
|
boost::split(rewardModelNames, line, boost::is_any_of("\t ")); |
|
|
boost::split(rewardModelNames, line, boost::is_any_of("\t ")); |
|
|
} else if (line == "@nr_states") { |
|
|
} else if (line == "@nr_states") { |
|
@ -164,7 +164,7 @@ namespace storm { |
|
|
} |
|
|
} |
|
|
firstRowOfState = row; |
|
|
firstRowOfState = row; |
|
|
|
|
|
|
|
|
if (type == storm::models::ModelType::Ctmc || type == storm::models::ModelType::MarkovAutomaton) { |
|
|
|
|
|
|
|
|
if (continuousTime) { |
|
|
// Parse exit rate for CTMC or MA
|
|
|
// Parse exit rate for CTMC or MA
|
|
|
STORM_LOG_THROW(boost::starts_with(line, "!"), storm::exceptions::WrongFormatException, "Exit rate missing."); |
|
|
STORM_LOG_THROW(boost::starts_with(line, "!"), storm::exceptions::WrongFormatException, "Exit rate missing."); |
|
|
line = line.substr(1); //Remove "!"
|
|
|
line = line.substr(1); //Remove "!"
|
|
@ -248,7 +248,7 @@ namespace storm { |
|
|
} |
|
|
} |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
for (std::string label : labels) { |
|
|
|
|
|
|
|
|
for (std::string const& label : labels) { |
|
|
if (!modelComponents->stateLabeling.containsLabel(label)) { |
|
|
if (!modelComponents->stateLabeling.containsLabel(label)) { |
|
|
modelComponents->stateLabeling.addLabel(label); |
|
|
modelComponents->stateLabeling.addLabel(label); |
|
|
} |
|
|
} |
|
@ -305,7 +305,7 @@ namespace storm { |
|
|
|
|
|
|
|
|
} else { |
|
|
} else { |
|
|
// New transition
|
|
|
// New transition
|
|
|
size_t posColon = line.find(":"); |
|
|
|
|
|
|
|
|
size_t posColon = line.find(':'); |
|
|
STORM_LOG_THROW(posColon != std::string::npos, storm::exceptions::WrongFormatException, "':' not found."); |
|
|
STORM_LOG_THROW(posColon != std::string::npos, storm::exceptions::WrongFormatException, "':' not found."); |
|
|
size_t target = parseNumber<size_t>(line.substr(2, posColon-3)); |
|
|
size_t target = parseNumber<size_t>(line.substr(2, posColon-3)); |
|
|
std::string valueStr = line.substr(posColon+2); |
|
|
std::string valueStr = line.substr(posColon+2); |
|
@ -314,12 +314,14 @@ namespace storm { |
|
|
STORM_LOG_THROW(target < stateSize, storm::exceptions::WrongFormatException, "Target state " << target << " is greater than state size " << stateSize); |
|
|
STORM_LOG_THROW(target < stateSize, storm::exceptions::WrongFormatException, "Target state " << target << " is greater than state size " << stateSize); |
|
|
builder.addNextValue(row, target, value); |
|
|
builder.addNextValue(row, target, value); |
|
|
} |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
} // end state iteration
|
|
|
STORM_LOG_TRACE("Finished parsing"); |
|
|
STORM_LOG_TRACE("Finished parsing"); |
|
|
|
|
|
|
|
|
|
|
|
// Build transition matrix
|
|
|
modelComponents->transitionMatrix = builder.build(row + 1, stateSize, nonDeterministic ? stateSize : 0); |
|
|
modelComponents->transitionMatrix = builder.build(row + 1, stateSize, nonDeterministic ? stateSize : 0); |
|
|
STORM_LOG_TRACE("Built matrix"); |
|
|
STORM_LOG_TRACE("Built matrix"); |
|
|
|
|
|
|
|
|
|
|
|
// Build reward models
|
|
|
uint64_t numRewardModels = std::max(stateRewards.size(), actionRewards.size()); |
|
|
uint64_t numRewardModels = std::max(stateRewards.size(), actionRewards.size()); |
|
|
for (uint64_t i = 0; i < numRewardModels; ++i) { |
|
|
for (uint64_t i = 0; i < numRewardModels; ++i) { |
|
|
std::string rewardModelName; |
|
|
std::string rewardModelName; |
|
@ -329,10 +331,10 @@ namespace storm { |
|
|
rewardModelName = rewardModelNames[i]; |
|
|
rewardModelName = rewardModelNames[i]; |
|
|
} |
|
|
} |
|
|
boost::optional<std::vector<ValueType>> stateRewardVector, actionRewardVector; |
|
|
boost::optional<std::vector<ValueType>> stateRewardVector, actionRewardVector; |
|
|
if (!stateRewards[i].empty()) { |
|
|
|
|
|
|
|
|
if (i < stateRewards.size() && !stateRewards[i].empty()) { |
|
|
stateRewardVector = std::move(stateRewards[i]); |
|
|
stateRewardVector = std::move(stateRewards[i]); |
|
|
} |
|
|
} |
|
|
if (!actionRewards[i].empty()) { |
|
|
|
|
|
|
|
|
if (i < actionRewards.size() && !actionRewards[i].empty()) { |
|
|
actionRewards[i].resize(row + 1, storm::utility::zero<ValueType>()); |
|
|
actionRewards[i].resize(row + 1, storm::utility::zero<ValueType>()); |
|
|
actionRewardVector = std::move(actionRewards[i]); |
|
|
actionRewardVector = std::move(actionRewards[i]); |
|
|
} |
|
|
} |
|
|