diff --git a/src/storm/parser/DirectEncodingParser.cpp b/src/storm/parser/DirectEncodingParser.cpp index a2e551838..9134e9f43 100644 --- a/src/storm/parser/DirectEncodingParser.cpp +++ b/src/storm/parser/DirectEncodingParser.cpp @@ -14,6 +14,7 @@ #include "storm/adapters/CarlAdapter.h" #include "storm/utility/constants.h" +#include "storm/utility/builder.h" #include "storm/utility/macros.h" #include "storm/utility/file.h" @@ -68,6 +69,9 @@ namespace storm { STORM_LOG_THROW(boost::starts_with(line, "@type: "), storm::exceptions::WrongFormatException, "Expected model type."); storm::models::ModelType type = storm::models::getModelType(line.substr(7)); STORM_LOG_TRACE("Model type: " << type); + STORM_LOG_THROW(type != storm::models::ModelType::MarkovAutomaton, storm::exceptions::NotSupportedException, "Markov Automata in DRN format are not supported (unclear indication of Markovian Choices in DRN format)"); + STORM_LOG_THROW(type != storm::models::ModelType::S2pg, storm::exceptions::NotSupportedException, "Stochastic Two Player Games in DRN format are not supported."); + // Parse parameters std::getline(file, line); STORM_LOG_THROW(line == "@parameters", storm::exceptions::WrongFormatException, "Expected parameter declaration."); @@ -91,35 +95,14 @@ namespace storm { std::getline(file, line); STORM_LOG_THROW(line == "@model", storm::exceptions::WrongFormatException, "Expected model declaration."); - // Construct transition matrix + // Construct model components std::shared_ptr> modelComponents = parseStates(file, type, nrStates, valueParser); - + // Done parsing storm::utility::closeFile(file); // Build model - switch (type) { - case storm::models::ModelType::Dtmc: - { - STORM_LOG_THROW(false, storm::exceptions::FileIoException, "DTMC not supported."); - } - case storm::models::ModelType::Ctmc: - { - modelComponents->rateTransitions = true; - return std::make_shared>(std::move(*modelComponents)); - } - case storm::models::ModelType::Mdp: - { - STORM_LOG_THROW(false, storm::exceptions::FileIoException, "MDP not supported."); - } - case storm::models::ModelType::MarkovAutomaton: - { - modelComponents->rateTransitions = true; - return std::make_shared>(std::move(*modelComponents)); - } - default: - STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Unknown/Unhandled model type " << type << " which cannot be parsed."); - } + return storm::utility::builder::buildModelFromComponents(type, std::move(*modelComponents)); } template @@ -130,17 +113,23 @@ namespace storm { storm::storage::SparseMatrixBuilder builder = storm::storage::SparseMatrixBuilder(0, 0, 0, false, nonDeterministic, 0); modelComponents->stateLabeling = storm::models::sparse::StateLabeling(stateSize); + // We parse rates for continuous time models. + if (type == storm::models::ModelType::Ctmc) { + modelComponents->rateTransitions = true; + } + // Iterate over all lines std::string line; size_t row = 0; size_t state = 0; - bool first = true; + bool firstState = true; + bool firstAction = true; while (std::getline(file, line)) { STORM_LOG_TRACE("Parsing: " << line); if (boost::starts_with(line, "state ")) { // New state - if (first) { - first = false; + if (firstState) { + firstState = false; } else { ++state; } @@ -180,12 +169,13 @@ namespace storm { STORM_LOG_TRACE("New state " << state); STORM_LOG_ASSERT(state == parsedId, "State ids do not correspond."); if (nonDeterministic) { + STORM_LOG_TRACE("new Row Group starts at " << row << "."); builder.newRowGroup(row); } } else if (boost::starts_with(line, "\taction ")) { // New action - if (first) { - first = false; + if (firstAction) { + firstAction = false; } else { ++row; } @@ -210,13 +200,13 @@ namespace storm { size_t target = boost::lexical_cast(line.substr(2, posColon-3)); std::string valueStr = line.substr(posColon+2); ValueType value = valueParser.parseValue(valueStr); - STORM_LOG_TRACE("Transition " << state << " -> " << target << ": " << value); - builder.addNextValue(state, target, value); + STORM_LOG_TRACE("Transition " << row << " -> " << target << ": " << value); + builder.addNextValue(row, target, value); } } STORM_LOG_TRACE("Finished parsing"); - modelComponents->transitionMatrix = builder.build(stateSize, stateSize); + modelComponents->transitionMatrix = builder.build(row + 1, stateSize, nonDeterministic ? stateSize : 0); STORM_LOG_TRACE("Built matrix"); return modelComponents; } diff --git a/src/storm/utility/DirectEncodingExporter.cpp b/src/storm/utility/DirectEncodingExporter.cpp index b82957c9c..0b1dded00 100644 --- a/src/storm/utility/DirectEncodingExporter.cpp +++ b/src/storm/utility/DirectEncodingExporter.cpp @@ -21,17 +21,20 @@ namespace storm { // Notice that for CTMCs we write the rate matrix instead of probabilities // Initialize + storm::models::ModelType type = sparseModel->getType(); std::vector exitRates; // Only for CTMCs and MAs. if(sparseModel->getType() == storm::models::ModelType::Ctmc) { exitRates = sparseModel->template as>()->getExitRateVector(); } else if(sparseModel->getType() == storm::models::ModelType::MarkovAutomaton) { + type = storm::models::ModelType::Mdp; + STORM_LOG_WARN("Markov automaton is exported as MDP (indication of Markovian choices is not supported in DRN format)."); exitRates = sparseModel->template as>()->getExitRates(); } // Write header os << "// Exported by storm" << std::endl; os << "// Original model type: " << sparseModel->getType() << std::endl; - os << "@type: " << sparseModel->getType() << std::endl; + os << "@type: " << type << std::endl; os << "@parameters" << std::endl; if (parameters.empty()) { for (std::string const& parameter : getParameters(sparseModel)) {