sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

storm pars result moved from storm to storm pars

tempestpy_adaptions
Sebastian Junges 7 years ago
parent
5a3c67c352
commit
53a2723e0c
4 changed files with 38 additions and 57 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 34
      src/storm-pars/api/export.h
  2. 1
      src/storm-pars/api/storm-pars.h
  3. 29
      src/storm/api/export.h
  4. 31
      src/storm/utility/export.h

34
src/storm-pars/api/export.h
View File

@ -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 <typename ValueType>
void exportParametricResultToFile(ValueType const& result, storm::analysis::ConstraintCollector<ValueType> 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<storm::RationalFunction> const& constraintCollector, std::string const& path) {
std::ofstream filestream;
storm::utility::openFile(path, filestream);
filestream << "$Parameters: ";
std::set<storm::RationalFunctionVariable> vars = result.gatherVariables();
std::copy(vars.begin(), vars.end(), std::ostream_iterator<storm::RationalFunctionVariable>(filestream, "; "));
filestream << std::endl;
filestream << "$Result: " << result.toString(false, true) << std::endl;
filestream << "$Well-formed Constraints: " << std::endl;
std::vector<std::string> stringConstraints;
std::transform(constraintCollector.getWellformedConstraints().begin(), constraintCollector.getWellformedConstraints().end(), std::back_inserter(stringConstraints), [](carl::Formula<typename storm::Polynomial::PolyType> const& c) -> std::string { return c.toString();});
std::copy(stringConstraints.begin(), stringConstraints.end(), std::ostream_iterator<std::string>(filestream, "\n"));
filestream << "$Graph-preserving Constraints: " << std::endl;
stringConstraints.clear();
std::transform(constraintCollector.getGraphPreservingConstraints().begin(), constraintCollector.getGraphPreservingConstraints().end(), std::back_inserter(stringConstraints), [](carl::Formula<typename storm::Polynomial::PolyType> const& c) -> std::string { return c.toString();});
std::copy(stringConstraints.begin(), stringConstraints.end(), std::ostream_iterator<std::string>(filestream, "\n"));
storm::utility::closeFile(filestream);
}
}
}

1
src/storm-pars/api/storm-pars.h
View File

@ -1,3 +1,4 @@
#pragma once
#include "storm-pars/api/region.h"
#include "storm-pars/api/export.h"

29
src/storm/api/export.h
View File

@ -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<storm::jani::Property> const& properties, std::string const& filename);
void exportJaniModelAsDot(storm::jani::Model const& model, std::string const& filename);
template <typename ValueType>
void exportParametricResultToFile(ValueType const& result, storm::analysis::ConstraintCollector<ValueType> 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<storm::RationalFunction> const& constraintCollector, std::string const& path) {
std::ofstream filestream;
storm::utility::openFile(path, filestream);
filestream << "!Parameters: ";
std::set<storm::RationalFunctionVariable> vars = result.gatherVariables();
std::copy(vars.begin(), vars.end(), std::ostream_iterator<storm::RationalFunctionVariable>(filestream, "; "));
filestream << std::endl;
filestream << "!Result: " << result.toString(false, true) << std::endl;
filestream << "!Well-formed Constraints: " << std::endl;
std::vector<std::string> stringConstraints;
std::transform(constraintCollector.getWellformedConstraints().begin(), constraintCollector.getWellformedConstraints().end(), std::back_inserter(stringConstraints), [](carl::Formula<typename storm::Polynomial::PolyType> const& c) -> std::string { return c.toString();});
std::copy(stringConstraints.begin(), stringConstraints.end(), std::ostream_iterator<std::string>(filestream, "\n"));
filestream << "!Graph-preserving Constraints: " << std::endl;
stringConstraints.clear();
std::transform(constraintCollector.getGraphPreservingConstraints().begin(), constraintCollector.getGraphPreservingConstraints().end(), std::back_inserter(stringConstraints), [](carl::Formula<typename storm::Polynomial::PolyType> const& c) -> std::string { return c.toString();});
std::copy(stringConstraints.begin(), stringConstraints.end(), std::ostream_iterator<std::string>(filestream, "\n"));
storm::utility::closeFile(filestream);
}
template <typename ValueType>
void exportSparseModelAsDrn(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, std::string const& filename, std::vector<std::string> const& parameterNames) {
std::ofstream stream;

31
src/storm/utility/export.h
View File

@ -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<typename ValueType>
void exportParametricMcResult(const ValueType& mcresult, storm::modelchecker::reachability::CollectConstraints<storm::RationalFunction> const& constraintCollector) {
std::string path = storm::settings::getModule<storm::settings::modules::ParametricSettings>().exportResultPath();
std::ofstream filestream;
filestream.open(path);
// todo add checks.
filestream << "!Parameters: ";
std::set<storm::RationalFunctionVariable> vars = mcresult.gatherVariables();
std::copy(vars.begin(), vars.end(), std::ostream_iterator<storm::RationalFunctionVariable>(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<carl::Constraint<ValueType>>(filestream, "\n"));
filestream << "!Graph-preserving Constraints: " << std::endl;
std::copy(constraintCollector.graphPreservingConstraints().begin(), constraintCollector.graphPreservingConstraints().end(), std::ostream_iterator<carl::Constraint<ValueType>>(filestream, "\n"));
filestream.close();
}
*/
template <typename ValueType>
inline void exportDataToCSVFile(std::string filepath, std::vector<std::vector<ValueType>> const& data, boost::optional<std::vector<std::string>> const& columnHeaders) {

Write Preview
Loading…
Cancel
Save