diff --git a/src/storm-pomdp-cli/storm-pomdp.cpp b/src/storm-pomdp-cli/storm-pomdp.cpp index eaa20c010..891426d49 100644 --- a/src/storm-pomdp-cli/storm-pomdp.cpp +++ b/src/storm-pomdp-cli/storm-pomdp.cpp @@ -182,7 +182,8 @@ namespace storm { std::cout << std::endl; } if (qualSettings.isExportWinningRegionSet()) { - search.getLastWinningRegion().storeToFile(qualSettings.exportWinningRegionPath()); + std::size_t hash = pomdp.hash(); + search.getLastWinningRegion().storeToFile(qualSettings.exportWinningRegionPath(), "model hash: " + std::to_string(hash)); } search.finalizeStatistics(); diff --git a/src/storm-pomdp/analysis/WinningRegion.cpp b/src/storm-pomdp/analysis/WinningRegion.cpp index 1b6c37f73..cdb329ace 100644 --- a/src/storm-pomdp/analysis/WinningRegion.cpp +++ b/src/storm-pomdp/analysis/WinningRegion.cpp @@ -1,5 +1,6 @@ #include #include +#include #include "storm/utility/file.h" #include "storm/utility/constants.h" #include "storm/storage/expressions/Expression.h" @@ -313,9 +314,12 @@ namespace pomdp { return result; } - void WinningRegion::storeToFile(std::string const& path) const { + void WinningRegion::storeToFile(std::string const& path, std::string const& preamble, bool append) const { std::ofstream file; - storm::utility::openFile(path, file); + storm::utility::openFile(path, file, append); + file << ":preamble" << std::endl; + file << preamble << std::endl; + file << ":winningregion" << std::endl; bool firstLine = true; for (auto const& i : observationSizes) { if(!firstLine) { @@ -337,26 +341,40 @@ namespace pomdp { } - WinningRegion WinningRegion::loadFromFile(std::string const& path) { + std::pair WinningRegion::loadFromFile(std::string const& path) { std::ifstream file; std::vector observationSizes; storm::utility::openFile(path, file); std::string line; - bool firstLine = true; + uint64_t state = 0; // 0 = expect preamble uint64_t observation = 0; WinningRegion wr({1}); + std::stringstream preamblestream; while (std::getline(file, line)) { - std::vector entries; - if(firstLine) { + if (boost::starts_with(line, "#")) { + continue; + } + if (state == 0) { + STORM_LOG_THROW(line == ":preamble", storm::exceptions::WrongFormatException, "Expected to see :preamble"); + state = 1; // state = 1: preamble + } else if (state == 1) { + if (line == ":winningregion") { + state = 2; // get sizes + } else { + preamblestream << line << std::endl; + } + } else if (state == 2) { + std::vector entries; boost::split(entries, line, boost::is_space()); std::vector observationSizes; - for(auto const& entry : entries) { + for (auto const &entry : entries) { observationSizes.push_back(std::stoul(entry)); } wr = WinningRegion(observationSizes); - firstLine = false; - } else { + state = 3; + } else if (state == 3) { + std::vector entries; boost::split(entries, line, boost::is_any_of(";")); entries.pop_back(); for (std::string const& bvString : entries) { @@ -366,7 +384,7 @@ namespace pomdp { } } storm::utility::closeFile(file); - return wr; + return {wr,preamblestream.str()}; } } diff --git a/src/storm-pomdp/analysis/WinningRegion.h b/src/storm-pomdp/analysis/WinningRegion.h index 88ef79cf7..e8269f154 100644 --- a/src/storm-pomdp/analysis/WinningRegion.h +++ b/src/storm-pomdp/analysis/WinningRegion.h @@ -36,8 +36,8 @@ namespace storm { bool empty() const; void print() const; - void storeToFile(std::string const& path) const; - static WinningRegion loadFromFile(std::string const& path); + void storeToFile(std::string const& path, std::string const& preamble="", bool append=false) const; + static std::pair loadFromFile(std::string const& path); private: