Storm 1.14.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
export.cpp
Go to the documentation of this file.
2
3#include <algorithm>
4#include <fstream>
5#include <iterator>
6#include <vector>
7
9#include "storm/io/file.h"
10
11namespace storm::pars {
12namespace api {
13
14template<>
15void exportParametricResultToFile(std::optional<storm::RationalFunction> result,
17 std::string const& path) {
18 std::ofstream filestream;
19 storm::io::openFile(path, filestream);
20 if (constraintCollector.has_value()) {
21 filestream << "$Parameters: ";
22 auto const& vars = constraintCollector->getVariables();
23 std::copy(vars.begin(), vars.end(), std::ostream_iterator<storm::RationalFunctionVariable>(filestream, "; "));
24 filestream << '\n';
25 } else {
26 if (result) {
27 filestream << "$Parameters: ";
28 auto const& vars = result->gatherVariables();
29 std::copy(vars.begin(), vars.end(), std::ostream_iterator<storm::RationalFunctionVariable>(filestream, "; "));
30 filestream << '\n';
31 }
32 }
33 if (result) {
34 filestream << "$Result: " << result->toString(false, true) << '\n';
35 }
36 if (constraintCollector.has_value()) {
37 filestream << "$Well-formed Constraints: \n";
38 std::vector<std::string> stringConstraints;
39 std::transform(constraintCollector->getWellformedConstraints().begin(), constraintCollector->getWellformedConstraints().end(),
40 std::back_inserter(stringConstraints),
41 [](carl::Formula<typename storm::Polynomial::PolyType> const& c) -> std::string { return c.toString(); });
42 std::copy(stringConstraints.begin(), stringConstraints.end(), std::ostream_iterator<std::string>(filestream, "\n"));
43 filestream << "$Graph-preserving Constraints: \n";
44 stringConstraints.clear();
45 std::transform(constraintCollector->getGraphPreservingConstraints().begin(), constraintCollector->getGraphPreservingConstraints().end(),
46 std::back_inserter(stringConstraints),
47 [](carl::Formula<typename storm::Polynomial::PolyType> const& c) -> std::string { return c.toString(); });
48 std::copy(stringConstraints.begin(), stringConstraints.end(), std::ostream_iterator<std::string>(filestream, "\n"));
49 }
50 storm::io::closeFile(filestream);
51}
52
53} // namespace api
54} // namespace storm::pars
Helper class that optionally holds a reference to an object of type T.
Definition OptionalRef.h:48
Class to collect constraints on parametric Markov chains.
void closeFile(std::ofstream &stream)
Close the given file after writing.
Definition file.h:47
void openFile(std::string const &filepath, std::ofstream &filestream, bool append=false, bool silent=false)
Open the given file for writing.
Definition file.h:18
void exportParametricResultToFile(std::optional< storm::RationalFunction > result, storm::OptionalRef< storm::analysis::ConstraintCollector< storm::RationalFunction > const > const &constraintCollector, std::string const &path)
Definition export.cpp:15