Storm 1.14.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
SparseStateRewardParser.cpp
Go to the documentation of this file.
2
3#include <iostream>
4
11
12namespace storm {
13namespace parser {
14
15using namespace storm::utility::cstring;
16
17template<typename ValueType>
18std::vector<ValueType> SparseStateRewardParser<ValueType>::parseSparseStateReward(uint_fast64_t stateCount, std::string const& filename) {
19 // Open file.
20 MappedFile file(filename.c_str());
21 char const* buf = file.getData();
22
23 // Create state reward vector with given state count.
24 std::vector<ValueType> stateRewards(stateCount);
25
26 // Now parse state reward assignments.
27 uint_fast64_t state = 0;
28 uint_fast64_t lastState = (uint_fast64_t)-1;
29 uint_fast64_t const startIndexComparison = lastState;
30 double reward;
31
32 // Iterate over states.
33 while (buf[0] != '\0') {
34 // Parse state.
35 state = checked_strtol(buf, &buf);
36
37 // If the state has already been read or skipped once there might be a problem with the file (doubled lines, or blocks).
38 // Note: The value -1 shows that lastState has not yet been set, i.e. this is the first run of the loop (state index (2^64)-1 is a really bad starting
39 // index).
40 STORM_LOG_THROW(state > lastState || lastState == startIndexComparison, storm::exceptions::WrongFormatException,
41 "Error while parsing " << filename << ": State " << state << " was found but has already been read or skipped previously.");
42
43 if (stateCount <= state) {
44 STORM_LOG_ERROR("Error while parsing " << filename << ": Found reward for a state of an invalid index \"" << state << "\". The model has only "
45 << stateCount << " states.");
46 STORM_LOG_THROW(false, storm::exceptions::OutOfRangeException,
47 "Error while parsing " << filename << ": Found reward for a state of an invalid index \"" << state << "\".");
48 }
49
50 // Parse reward value.
51 reward = checked_strtod(buf, &buf);
52
53 if (reward < 0.0) {
54 STORM_LOG_ERROR("Error while parsing " << filename << ": Expected positive reward value but got \"" << reward << "\".");
55 STORM_LOG_THROW(false, storm::exceptions::WrongFormatException,
56 "Error while parsing " << filename << ": State reward file specifies illegal reward value.");
57 }
58
59 stateRewards[state] = reward;
60
61 buf = trimWhitespaces(buf);
62 lastState = state;
63 }
64 return stateRewards;
65}
66
69} // namespace parser
70} // namespace storm
Opens a file and maps it to memory providing a char* containing the file content.
Definition MappedFile.h:21
char const * getData() const
Returns a pointer to the beginning of the mapped file data.
A class providing the functionality to parse a the state rewards of a model.
static std::vector< ValueType > parseSparseStateReward(uint_fast64_t stateCount, std::string const &filename)
Reads a state reward file and puts the result in a state reward vector.
#define STORM_LOG_ERROR(message)
Definition logging.h:29
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:28
Contains all file parsers and helper classes.
double checked_strtod(char const *str, char const **end)
Calls strtod() internally and checks if the new pointer is different from the original one,...
Definition cstring.cpp:36
uint_fast64_t checked_strtol(char const *str, char const **end)
Calls strtol() internally and checks if the new pointer is different from the original one,...
Definition cstring.cpp:21
char const * trimWhitespaces(char const *buf)
Skips spaces, tabs, newlines and carriage returns.
Definition cstring.cpp:62