From 76d5ddad3032d33fa7397362ab997f236ab781b6 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 29 Mar 2018 13:42:56 +0200 Subject: [PATCH] Minor improvements in DRN parser --- src/storm/parser/DirectEncodingParser.cpp | 35 +++++++++++--------- src/storm/utility/DirectEncodingExporter.cpp | 31 +++++++++-------- src/storm/utility/DirectEncodingExporter.h | 4 +-- 3 files changed, 36 insertions(+), 34 deletions(-) diff --git a/src/storm/parser/DirectEncodingParser.cpp b/src/storm/parser/DirectEncodingParser.cpp index 288eda7e5..a0595e7be 100644 --- a/src/storm/parser/DirectEncodingParser.cpp +++ b/src/storm/parser/DirectEncodingParser.cpp @@ -40,26 +40,27 @@ namespace storm { bool sawParameters = false; size_t nrStates = 0; storm::models::ModelType type; - std::vector rewardModelNames; - - std::shared_ptr> modelComponents; + std::shared_ptr> modelComponents; // Parse header - while(std::getline(file, line)) { - if(line.empty() || boost::starts_with(line, "//")) { + while (std::getline(file, line)) { + if (line.empty() || boost::starts_with(line, "//")) { continue; } if (boost::starts_with(line, "@type: ")) { + // Parse type STORM_LOG_THROW(!sawType, storm::exceptions::WrongFormatException, "Type declared twice"); 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."); sawType = true; - } - if(line == "@parameters") { + + } else if (line == "@parameters") { + // Parse parameters + STORM_LOG_THROW(!sawParameters, storm::exceptions::WrongFormatException, "Parameters declared twice"); std::getline(file, line); if (line != "") { std::vector parameters; @@ -70,26 +71,28 @@ namespace storm { } } sawParameters = true; - } - if(line == "@reward_models") { + + } else if (line == "@reward_models") { + // Parse reward models STORM_LOG_THROW(rewardModelNames.size() == 0, storm::exceptions::WrongFormatException, "Reward model names declared twice"); std::getline(file, line); boost::split(rewardModelNames, line, boost::is_any_of("\t ")); - } - if(line == "@nr_states") { + } else if (line == "@nr_states") { + // Parse no. of states STORM_LOG_THROW(nrStates == 0, storm::exceptions::WrongFormatException, "Number states declared twice"); std::getline(file, line); nrStates = NumberParser::parse(line); - - } - if(line == "@model") { + } else if (line == "@model") { + // Parse rest of the model STORM_LOG_THROW(sawType, storm::exceptions::WrongFormatException, "Type has to be declared before model."); STORM_LOG_THROW(sawParameters, storm::exceptions::WrongFormatException, "Parameters have to be declared before model."); - STORM_LOG_THROW(nrStates != 0, storm::exceptions::WrongFormatException, "Nr States has to be declared before model."); + STORM_LOG_THROW(nrStates != 0, storm::exceptions::WrongFormatException, "No. of states has to be declared before model."); // Construct model components modelComponents = parseStates(file, type, nrStates, valueParser, rewardModelNames); break; + } else { + STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Could not parse line '" << line << "'."); } } // Done parsing @@ -182,8 +185,8 @@ namespace storm { } else { ++row; } - line = line.substr(8); STORM_LOG_TRACE("New action: " << row); + line = line.substr(8); //Remove "\taction " // Check for rewards if (boost::starts_with(line, "[")) { // Rewards found diff --git a/src/storm/utility/DirectEncodingExporter.cpp b/src/storm/utility/DirectEncodingExporter.cpp index e0913a0f2..43c34b3ce 100644 --- a/src/storm/utility/DirectEncodingExporter.cpp +++ b/src/storm/utility/DirectEncodingExporter.cpp @@ -55,7 +55,8 @@ namespace storm { os << "@model" << std::endl; storm::storage::SparseMatrix const& matrix = sparseModel->getTransitionMatrix(); - + + // Iterate over states and export state information and outgoing transitions for (typename storm::storage::SparseMatrix::index_type group = 0; group < matrix.getRowGroupCount(); ++group) { os << "state " << group; @@ -92,22 +93,23 @@ namespace storm { // Iterate over all actions for (typename storm::storage::SparseMatrix::index_type row = start; row < end; ++row) { - // Print the actual row. + // Write choice if (sparseModel->hasChoiceLabeling()) { os << "\taction "; bool lfirst = true; for (auto const& label : sparseModel->getChoiceLabeling().getLabelsOfChoice(row)) { if (!lfirst) { os << "_"; + lfirst = false; } os << label; - lfirst = false; } } else { os << "\taction " << row - start; } + + // Write action rewards bool first = true; - // Write transition rewards for (auto const& rewardModelEntry : sparseModel->getRewardModels()) { if (first) { os << " ["; @@ -116,7 +118,7 @@ namespace storm { os << ", "; } - if(rewardModelEntry.second.hasStateActionRewards()) { + if (rewardModelEntry.second.hasStateActionRewards()) { os << storm::utility::to_string(rewardModelEntry.second.getStateActionRewardVector().at(row)); } else { os << "0"; @@ -126,19 +128,18 @@ namespace storm { if (!first) { os << "]"; } - os << std::endl; - - // Write probabilities - for(auto it = matrix.begin(row); it != matrix.end(row); ++it) { + + // Write transitions + for (auto it = matrix.begin(row); it != matrix.end(row); ++it) { ValueType prob = it->getValue(); os << "\t\t" << it->getColumn() << " : "; os << storm::utility::to_string(prob) << std::endl; } - + } - } // end matrix iteration - + } // end state iteration + } template @@ -146,9 +147,6 @@ namespace storm { return {}; } - template void explicitExportSparseModel(std::ostream& os, std::shared_ptr> sparseModel, std::vector const& parameters); - -#ifdef STORM_HAVE_CARL template<> std::vector getParameters(std::shared_ptr> sparseModel) { std::vector parameters; @@ -167,8 +165,9 @@ namespace storm { return parameters; } + // Template instantiations + template void explicitExportSparseModel(std::ostream& os, std::shared_ptr> sparseModel, std::vector const& parameters); template void explicitExportSparseModel(std::ostream& os, std::shared_ptr> sparseModel, std::vector const& parameters); template void explicitExportSparseModel(std::ostream& os, std::shared_ptr> sparseModel, std::vector const& parameters); -#endif } } diff --git a/src/storm/utility/DirectEncodingExporter.h b/src/storm/utility/DirectEncodingExporter.h index 9728599a6..5ffe4d10d 100644 --- a/src/storm/utility/DirectEncodingExporter.h +++ b/src/storm/utility/DirectEncodingExporter.h @@ -18,13 +18,13 @@ namespace storm { void explicitExportSparseModel(std::ostream& os, std::shared_ptr> sparseModel, std::vector const& parameters); /*! - * Accumalate parameters in the model. + * Accumulate parameters in the model. * * @param sparseModel Model. * @return List of parameters in the model. */ template std::vector getParameters(std::shared_ptr> sparseModel); - + } }