Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
ImcaMarkovAutomatonParser.cpp
Go to the documentation of this file.
2
3#include <fstream>
4#include <memory>
5
8#include "storm/io/file.h"
11
12namespace storm {
13namespace parser {
14
15template<typename ValueType>
16std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> ImcaMarkovAutomatonParser<ValueType>::parseImcaFile(std::string const& filename) {
17 // Open file and initialize result.
18 std::ifstream inputFileStream;
19 storm::io::openFile(filename, inputFileStream);
20
22
23 // Now try to parse the contents of the file.
24 std::string fileContent((std::istreambuf_iterator<char>(inputFileStream)), (std::istreambuf_iterator<char>()));
25 PositionIteratorType first(fileContent.begin());
26 PositionIteratorType iter = first;
27 PositionIteratorType last(fileContent.end());
28
29 try {
30 // Start parsing.
32 bool succeeded = qi::phrase_parse(
33 iter, last, grammar, storm::spirit_encoding::space_type() | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)) >> (qi::eol | qi::eoi), components);
34 STORM_LOG_THROW(succeeded, storm::exceptions::WrongFormatException, "Could not parse imca file.");
35 STORM_LOG_DEBUG("Parsed imca file successfully.");
36 } catch (qi::expectation_failure<PositionIteratorType> const& e) {
37 STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, e.what_);
38 storm::io::closeFile(inputFileStream);
39 } catch (std::exception& e) {
40 // In case of an exception properly close the file before passing exception.
41 storm::io::closeFile(inputFileStream);
42 throw e;
43 }
44
45 // Close the stream in case everything went smoothly
46 storm::io::closeFile(inputFileStream);
47
48 // Build the model from the obtained model components
50 ->template as<storm::models::sparse::MarkovAutomaton<ValueType>>();
51}
52
54} // namespace parser
55} // namespace storm
boost::spirit::line_pos_iterator< BaseIteratorType > PositionIteratorType
static std::shared_ptr< storm::models::sparse::MarkovAutomaton< ValueType > > parseImcaFile(std::string const &filename)
Parses the given file under the assumption that it contains a Markov automaton specified in the imca ...
#define STORM_LOG_DEBUG(message)
Definition logging.h:23
#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
std::shared_ptr< storm::models::sparse::Model< ValueType, RewardModelType > > buildModelFromComponents(storm::models::ModelType modelType, storm::storage::sparse::ModelComponents< ValueType, RewardModelType > &&components)
Definition builder.cpp:19
LabParser.cpp.
Definition cli.cpp:18