Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
MonotonicityParser.cpp
Go to the documentation of this file.
2#include <boost/algorithm/string.hpp>
4
7#include "storm/io/file.h"
10
11namespace storm {
12namespace parser {
13
14template<typename VariableType>
15std::pair<std::set<VariableType>, std::set<VariableType>> MonotonicityParser<VariableType>::parseMonotoneVariablesFromFile(
16 std::string const& fileName, std::set<VariableType> const& consideredVariables) {
17 // Open file and initialize result.
18 std::ifstream inputFileStream;
19 storm::io::openFile(fileName, inputFileStream);
20
21 std::set<VariableType> monotoneIncrVars;
22 std::set<VariableType> monotoneDecrVars;
23
24 // Now try to parse the contents of the file.
25 try {
26 std::string fileContent((std::istreambuf_iterator<char>(inputFileStream)), (std::istreambuf_iterator<char>()));
27 std::vector<std::string> fileSplitted;
28
29 boost::split(fileSplitted, fileContent, boost::is_any_of(";"));
30 STORM_LOG_THROW(fileSplitted.size() == 2, storm::exceptions::WrongFormatException, "Expecting content to contain \";\" between monotone variables");
31 std::vector<std::string> monotoneIncrVarsString;
32 boost::split(monotoneIncrVarsString, fileSplitted[0], boost::is_any_of(" "));
33 std::vector<std::string> monotoneDecrVarsString;
34 boost::split(monotoneDecrVarsString, fileSplitted[0], boost::is_any_of(" "));
35 // TODO: throw errors if file not formatted correctly
36 for (auto varString : monotoneIncrVarsString) {
37 VariableType var;
38 for (auto const& v : consideredVariables) {
39 std::stringstream stream;
40 stream << v;
41 if (varString == stream.str()) {
42 var = v;
43 break;
44 }
45 }
46 monotoneIncrVars.insert(var);
47 }
48 for (auto varString : monotoneDecrVarsString) {
49 VariableType var;
50 for (auto const& v : consideredVariables) {
51 std::stringstream stream;
52 stream << v;
53 if (varString == stream.str()) {
54 var = v;
55 break;
56 }
57 }
58 monotoneDecrVars.insert(var);
59 }
60
61 } catch (std::exception& e) {
62 // In case of an exception properly close the file before passing exception.
63 storm::io::closeFile(inputFileStream);
64 throw e;
65 }
66
67 // Close the stream in case everything went smoothly and return result.
68 storm::io::closeFile(inputFileStream);
69 return {std::move(monotoneIncrVars), std::move(monotoneDecrVars)};
70}
71
73} // namespace parser
74} // namespace storm
static std::pair< std::set< VariableType >, std::set< VariableType > > parseMonotoneVariablesFromFile(std::string const &fileName, std::set< VariableType > const &consideredVariables)
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
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
LabParser.cpp.
Definition cli.cpp:18