|
@ -3,25 +3,21 @@ |
|
|
#include <iostream>
|
|
|
#include <iostream>
|
|
|
#include <string>
|
|
|
#include <string>
|
|
|
#include <regex>
|
|
|
#include <regex>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
#include <boost/algorithm/string.hpp>
|
|
|
#include <boost/algorithm/string.hpp>
|
|
|
#include <boost/algorithm/string/predicate.hpp>
|
|
|
#include <boost/algorithm/string/predicate.hpp>
|
|
|
|
|
|
|
|
|
#include "storm/models/sparse/MarkovAutomaton.h"
|
|
|
|
|
|
#include "storm/models/sparse/Ctmc.h"
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
#include "storm/adapters/RationalFunctionAdapter.h"
|
|
|
#include "storm/exceptions/FileIoException.h"
|
|
|
#include "storm/exceptions/FileIoException.h"
|
|
|
#include "storm/exceptions/WrongFormatException.h"
|
|
|
|
|
|
#include "storm/exceptions/InvalidArgumentException.h"
|
|
|
#include "storm/exceptions/InvalidArgumentException.h"
|
|
|
#include "storm/exceptions/NotSupportedException.h"
|
|
|
#include "storm/exceptions/NotSupportedException.h"
|
|
|
|
|
|
#include "storm/exceptions/WrongFormatException.h"
|
|
|
|
|
|
#include "storm/models/sparse/MarkovAutomaton.h"
|
|
|
|
|
|
#include "storm/models/sparse/Ctmc.h"
|
|
|
#include "storm/settings/SettingsManager.h"
|
|
|
#include "storm/settings/SettingsManager.h"
|
|
|
|
|
|
|
|
|
#include "storm/adapters/RationalFunctionAdapter.h"
|
|
|
|
|
|
#include "storm/utility/constants.h"
|
|
|
|
|
|
#include "storm/utility/builder.h"
|
|
|
#include "storm/utility/builder.h"
|
|
|
#include "storm/utility/macros.h"
|
|
|
|
|
|
|
|
|
#include "storm/utility/constants.h"
|
|
|
#include "storm/utility/file.h"
|
|
|
#include "storm/utility/file.h"
|
|
|
|
|
|
#include "storm/utility/macros.h"
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
namespace storm { |
|
|
namespace storm { |
|
@ -48,7 +44,7 @@ namespace storm { |
|
|
std::shared_ptr<storm::storage::sparse::ModelComponents<ValueType, RewardModelType>> modelComponents; |
|
|
std::shared_ptr<storm::storage::sparse::ModelComponents<ValueType, RewardModelType>> modelComponents; |
|
|
|
|
|
|
|
|
// Parse header
|
|
|
// Parse header
|
|
|
while (std::getline(file, line)) { |
|
|
|
|
|
|
|
|
while (storm::utility::getline(file, line)) { |
|
|
if (line.empty() || boost::starts_with(line, "//")) { |
|
|
if (line.empty() || boost::starts_with(line, "//")) { |
|
|
continue; |
|
|
continue; |
|
|
} |
|
|
} |
|
@ -65,7 +61,7 @@ namespace storm { |
|
|
} else if (line == "@parameters") { |
|
|
} else if (line == "@parameters") { |
|
|
// Parse parameters
|
|
|
// Parse parameters
|
|
|
STORM_LOG_THROW(!sawParameters, storm::exceptions::WrongFormatException, "Parameters declared twice"); |
|
|
STORM_LOG_THROW(!sawParameters, storm::exceptions::WrongFormatException, "Parameters declared twice"); |
|
|
std::getline(file, line); |
|
|
|
|
|
|
|
|
storm::utility::getline(file, line); |
|
|
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(" ")); |
|
@ -78,7 +74,7 @@ namespace storm { |
|
|
|
|
|
|
|
|
} else if (line == "@placeholders") { |
|
|
} else if (line == "@placeholders") { |
|
|
// Parse placeholders
|
|
|
// Parse placeholders
|
|
|
while (std::getline(file, line)) { |
|
|
|
|
|
|
|
|
while (storm::utility::getline(file, line)) { |
|
|
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."); |
|
|
std::string placeName = line.substr(0, posColon - 1); |
|
|
std::string placeName = line.substr(0, posColon - 1); |
|
@ -96,16 +92,16 @@ namespace storm { |
|
|
} else if (line == "@reward_models") { |
|
|
} else if (line == "@reward_models") { |
|
|
// Parse reward models
|
|
|
// Parse reward models
|
|
|
STORM_LOG_THROW(rewardModelNames.empty(), 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); |
|
|
|
|
|
|
|
|
storm::utility::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") { |
|
|
// Parse no. of states
|
|
|
// Parse no. of states
|
|
|
STORM_LOG_THROW(nrStates == 0, storm::exceptions::WrongFormatException, "Number states declared twice"); |
|
|
STORM_LOG_THROW(nrStates == 0, storm::exceptions::WrongFormatException, "Number states declared twice"); |
|
|
std::getline(file, line); |
|
|
|
|
|
|
|
|
storm::utility::getline(file, line); |
|
|
nrStates = parseNumber<size_t>(line); |
|
|
nrStates = parseNumber<size_t>(line); |
|
|
} else if (line == "@nr_choices") { |
|
|
} else if (line == "@nr_choices") { |
|
|
STORM_LOG_THROW(nrChoices == 0, storm::exceptions::WrongFormatException, "Number of actions declared twice"); |
|
|
STORM_LOG_THROW(nrChoices == 0, storm::exceptions::WrongFormatException, "Number of actions declared twice"); |
|
|
std::getline(file, line); |
|
|
|
|
|
|
|
|
storm::utility::getline(file, line); |
|
|
nrChoices = parseNumber<size_t>(line); |
|
|
nrChoices = parseNumber<size_t>(line); |
|
|
} else if (line == "@model") { |
|
|
} else if (line == "@model") { |
|
|
// Parse rest of the model
|
|
|
// Parse rest of the model
|
|
@ -164,7 +160,7 @@ namespace storm { |
|
|
size_t state = 0; |
|
|
size_t state = 0; |
|
|
bool firstState = true; |
|
|
bool firstState = true; |
|
|
bool firstActionForState = true; |
|
|
bool firstActionForState = true; |
|
|
while (std::getline(file, line)) { |
|
|
|
|
|
|
|
|
while (storm::utility::getline(file, line)) { |
|
|
STORM_LOG_TRACE("Parsing: " << line); |
|
|
STORM_LOG_TRACE("Parsing: " << line); |
|
|
if (boost::starts_with(line, "state ")) { |
|
|
if (boost::starts_with(line, "state ")) { |
|
|
// New state
|
|
|
// New state
|
|
|