From 53a2723e0cce7dd4fc9c8cb3e9f4e69956ec7b41 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Tue, 11 Jul 2017 22:48:09 +0200 Subject: [PATCH] storm pars result moved from storm to storm pars --- src/storm-pars/api/export.h | 34 +++++++++++++++++++++++++++++++++ src/storm-pars/api/storm-pars.h | 1 + src/storm/api/export.h | 29 +--------------------------- src/storm/utility/export.h | 31 ++---------------------------- 4 files changed, 38 insertions(+), 57 deletions(-) create mode 100644 src/storm-pars/api/export.h diff --git a/src/storm-pars/api/export.h b/src/storm-pars/api/export.h new file mode 100644 index 000000000..cae413bd8 --- /dev/null +++ b/src/storm-pars/api/export.h @@ -0,0 +1,34 @@ +#include "storm/utility/file.h" +#include "storm/utility/macros.h" +#include "storm/exceptions/NotSupportedException.h" +#include "storm/analysis/GraphConditions.h" + +namespace storm { + namespace api { + + template + void exportParametricResultToFile(ValueType const& result, storm::analysis::ConstraintCollector const& constraintCollector, std::string const& path) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Cannot export non-parametric result."); + } + + template <> + inline void exportParametricResultToFile(storm::RationalFunction const& result, storm::analysis::ConstraintCollector const& constraintCollector, std::string const& path) { + std::ofstream filestream; + storm::utility::openFile(path, filestream); + filestream << "$Parameters: "; + std::set vars = result.gatherVariables(); + std::copy(vars.begin(), vars.end(), std::ostream_iterator(filestream, "; ")); + filestream << std::endl; + filestream << "$Result: " << result.toString(false, true) << std::endl; + filestream << "$Well-formed Constraints: " << std::endl; + std::vector stringConstraints; + std::transform(constraintCollector.getWellformedConstraints().begin(), constraintCollector.getWellformedConstraints().end(), std::back_inserter(stringConstraints), [](carl::Formula const& c) -> std::string { return c.toString();}); + std::copy(stringConstraints.begin(), stringConstraints.end(), std::ostream_iterator(filestream, "\n")); + filestream << "$Graph-preserving Constraints: " << std::endl; + stringConstraints.clear(); + std::transform(constraintCollector.getGraphPreservingConstraints().begin(), constraintCollector.getGraphPreservingConstraints().end(), std::back_inserter(stringConstraints), [](carl::Formula const& c) -> std::string { return c.toString();}); + std::copy(stringConstraints.begin(), stringConstraints.end(), std::ostream_iterator(filestream, "\n")); + storm::utility::closeFile(filestream); + } + } +} diff --git a/src/storm-pars/api/storm-pars.h b/src/storm-pars/api/storm-pars.h index 42ac7dc79..a1a32ac05 100644 --- a/src/storm-pars/api/storm-pars.h +++ b/src/storm-pars/api/storm-pars.h @@ -1,3 +1,4 @@ #pragma once #include "storm-pars/api/region.h" +#include "storm-pars/api/export.h" \ No newline at end of file diff --git a/src/storm/api/export.h b/src/storm/api/export.h index b9d781789..3ba81525d 100644 --- a/src/storm/api/export.h +++ b/src/storm/api/export.h @@ -2,7 +2,6 @@ #include "storm/storage/jani/JSONExporter.h" -#include "storm/analysis/GraphConditions.h" #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/JaniExportSettings.h" @@ -10,7 +9,6 @@ #include "storm/utility/DirectEncodingExporter.h" #include "storm/utility/file.h" #include "storm/utility/macros.h" -#include "storm/exceptions/NotSupportedException.h" namespace storm { namespace api { @@ -18,32 +16,7 @@ namespace storm { void exportJaniModel(storm::jani::Model const& model, std::vector const& properties, std::string const& filename); void exportJaniModelAsDot(storm::jani::Model const& model, std::string const& filename); - - template - void exportParametricResultToFile(ValueType const& result, storm::analysis::ConstraintCollector const& constraintCollector, std::string const& path) { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Cannot export non-parametric result."); - } - - template <> - inline void exportParametricResultToFile(storm::RationalFunction const& result, storm::analysis::ConstraintCollector const& constraintCollector, std::string const& path) { - std::ofstream filestream; - storm::utility::openFile(path, filestream); - filestream << "!Parameters: "; - std::set vars = result.gatherVariables(); - std::copy(vars.begin(), vars.end(), std::ostream_iterator(filestream, "; ")); - filestream << std::endl; - filestream << "!Result: " << result.toString(false, true) << std::endl; - filestream << "!Well-formed Constraints: " << std::endl; - std::vector stringConstraints; - std::transform(constraintCollector.getWellformedConstraints().begin(), constraintCollector.getWellformedConstraints().end(), std::back_inserter(stringConstraints), [](carl::Formula const& c) -> std::string { return c.toString();}); - std::copy(stringConstraints.begin(), stringConstraints.end(), std::ostream_iterator(filestream, "\n")); - filestream << "!Graph-preserving Constraints: " << std::endl; - stringConstraints.clear(); - std::transform(constraintCollector.getGraphPreservingConstraints().begin(), constraintCollector.getGraphPreservingConstraints().end(), std::back_inserter(stringConstraints), [](carl::Formula const& c) -> std::string { return c.toString();}); - std::copy(stringConstraints.begin(), stringConstraints.end(), std::ostream_iterator(filestream, "\n")); - storm::utility::closeFile(filestream); - } - + template void exportSparseModelAsDrn(std::shared_ptr> const& model, std::string const& filename, std::vector const& parameterNames) { std::ofstream stream; diff --git a/src/storm/utility/export.h b/src/storm/utility/export.h index b4f5020c0..61fb9e46f 100644 --- a/src/storm/utility/export.h +++ b/src/storm/utility/export.h @@ -1,10 +1,3 @@ -/** - * @file: export.h - * @author: Sebastian Junges - * - * @since October 7, 2014 - */ - #ifndef STORM_UTILITY_EXPORT_H_ #define STORM_UTILITY_EXPORT_H_ @@ -14,32 +7,12 @@ #include "storm/utility/macros.h" #include "storm/utility/file.h" -//#include "storm/storage/parameters.h" -//#include "storm/settings/modules/ParametricSettings.h" -//#include "storm/modelchecker/reachability/CollectConstraints.h" + namespace storm { namespace utility { - /* TODO Fix me - template - void exportParametricMcResult(const ValueType& mcresult, storm::modelchecker::reachability::CollectConstraints const& constraintCollector) { - std::string path = storm::settings::getModule().exportResultPath(); - std::ofstream filestream; - filestream.open(path); - // todo add checks. - filestream << "!Parameters: "; - std::set vars = mcresult.gatherVariables(); - std::copy(vars.begin(), vars.end(), std::ostream_iterator(filestream, ", ")); - filestream << std::endl; - filestream << "!Result: " << mcresult << std::endl; - filestream << "!Well-formed Constraints: " << std::endl; - std::copy(constraintCollector.wellformedConstraints().begin(), constraintCollector.wellformedConstraints().end(), std::ostream_iterator>(filestream, "\n")); - filestream << "!Graph-preserving Constraints: " << std::endl; - std::copy(constraintCollector.graphPreservingConstraints().begin(), constraintCollector.graphPreservingConstraints().end(), std::ostream_iterator>(filestream, "\n")); - filestream.close(); - } - */ + template inline void exportDataToCSVFile(std::string filepath, std::vector> const& data, boost::optional> const& columnHeaders) {