17template<
typename ValueType>
18typename MarkovAutomatonSparseTransitionParser<ValueType>::FirstPassResult MarkovAutomatonSparseTransitionParser<ValueType>::firstPass(
char const* buf) {
19 MarkovAutomatonSparseTransitionParser::FirstPassResult result;
25 if (buf[0] <
'0' || buf[0] >
'9') {
31 uint_fast64_t source, target = 0;
32 uint_fast64_t lastsource = 0;
33 bool encounteredEOF =
false;
34 bool stateHasMarkovianChoice =
false;
35 bool stateHasProbabilisticChoice =
false;
36 while (buf[0] !=
'\0' && !encounteredEOF) {
41 if (source > result.highestStateIndex) {
42 result.highestStateIndex = source;
46 if (source > lastsource + 1) {
47 if (!dontFixDeadlocks) {
48 result.numberOfNonzeroEntries += source - lastsource - 1;
49 result.numberOfChoices += source - lastsource - 1;
51 STORM_LOG_ERROR(
"Found deadlock states (e.g. " << lastsource + 1 <<
") during parsing. Please fix them or set the appropriate flag.");
52 throw storm::exceptions::WrongFormatException()
53 <<
"Found deadlock states (e.g. " << lastsource + 1 <<
") during parsing. Please fix them or set the appropriate flag.";
55 }
else if (source < lastsource) {
56 STORM_LOG_ERROR(
"Illegal state choice order. A choice of state " << source <<
" appears at an illegal position.");
57 throw storm::exceptions::WrongFormatException() <<
"Illegal state choice order. A choice of state " << source <<
" appears at an illegal position.";
60 ++result.numberOfChoices;
63 if (source != lastsource) {
64 stateHasMarkovianChoice =
false;
65 stateHasProbabilisticChoice =
false;
74 bool isMarkovianChoice =
false;
75 if (buf[0] ==
'!' &&
skipWord(buf) - buf == 1) {
76 isMarkovianChoice =
true;
78 isMarkovianChoice =
false;
82 if (isMarkovianChoice) {
83 if (stateHasMarkovianChoice) {
84 STORM_LOG_ERROR(
"The state " << source <<
" has multiple Markovian choices.");
85 throw storm::exceptions::WrongFormatException() <<
"The state " << source <<
" has multiple Markovian choices.";
87 if (stateHasProbabilisticChoice) {
89 "The state " << source
90 <<
" has a probabilistic choice preceding a Markovian choice. The Markovian choice must be the first choice listed.");
91 throw storm::exceptions::WrongFormatException()
92 <<
"The state " << source
93 <<
" has a probabilistic choice preceding a Markovian choice. The Markovian choice must be the first choice listed.";
95 stateHasMarkovianChoice =
true;
97 stateHasProbabilisticChoice =
true;
105 bool hasSuccessorState =
false;
106 bool encounteredNewDistribution =
false;
107 uint_fast64_t lastSuccessorState = 0;
113 if (buf[0] ==
'\0') {
114 if (!hasSuccessorState) {
115 STORM_LOG_ERROR(
"Premature end-of-file. Expected at least one successor state for state " << source <<
".");
116 throw storm::exceptions::WrongFormatException()
117 <<
"Premature end-of-file. Expected at least one successor state for state " << source <<
".";
120 encounteredEOF =
true;
122 }
else if (buf[0] ==
'*') {
128 if (target > result.highestStateIndex) {
129 result.highestStateIndex = target;
131 if (hasSuccessorState && target <= lastSuccessorState) {
132 STORM_LOG_ERROR(
"Illegal transition order for source state " << source <<
".");
133 throw storm::exceptions::WrongFormatException() <<
"Illegal transition order for source state " << source <<
".";
139 STORM_LOG_ERROR(
"Illegal negative probability/rate value for transition from " << source <<
" to " << target <<
": " << val <<
".");
140 throw storm::exceptions::WrongFormatException()
141 <<
"Illegal negative probability/rate value for transition from " << source <<
" to " << target <<
": " << val <<
".";
143 if (!isMarkovianChoice && val > 1.0) {
144 STORM_LOG_ERROR(
"Illegal probability value for transition from " << source <<
" to " << target <<
": " << val <<
".");
145 throw storm::exceptions::WrongFormatException()
146 <<
"Illegal probability value for transition from " << source <<
" to " << target <<
": " << val <<
".";
150 hasSuccessorState =
true;
151 lastSuccessorState = target;
154 ++result.numberOfNonzeroEntries;
160 encounteredNewDistribution =
true;
162 }
while (!encounteredEOF && !encounteredNewDistribution);
167 if (!dontFixDeadlocks) {
168 result.numberOfNonzeroEntries += result.highestStateIndex - lastsource;
169 result.numberOfChoices += result.highestStateIndex - lastsource;
171 STORM_LOG_ERROR(
"Found deadlock states (e.g. " << lastsource + 1 <<
") during parsing. Please fix them or set the appropriate flag.");
172 throw storm::exceptions::WrongFormatException()
173 <<
"Found deadlock states (e.g. " << lastsource + 1 <<
") during parsing. Please fix them or set the appropriate flag.";
179template<
typename ValueType>
180typename MarkovAutomatonSparseTransitionParser<ValueType>::Result MarkovAutomatonSparseTransitionParser<ValueType>::secondPass(
181 char const* buf, FirstPassResult
const& firstPassResult) {
182 Result result(firstPassResult);
188 if (buf[0] <
'0' || buf[0] >
'9') {
194 uint_fast64_t source, target = 0;
195 uint_fast64_t lastsource = 0;
196 bool encounteredEOF =
false;
197 uint_fast64_t currentChoice = 0;
200 result.transitionMatrixBuilder.newRowGroup(0);
202 while (buf[0] !=
'\0' && !encounteredEOF) {
207 if (source > lastsource + 1) {
208 if (!dontFixDeadlocks) {
209 for (uint_fast64_t index = lastsource + 1; index < source; ++index) {
210 result.transitionMatrixBuilder.newRowGroup(currentChoice);
211 result.transitionMatrixBuilder.addNextValue(currentChoice, index, 1);
215 STORM_LOG_ERROR(
"Found deadlock states (e.g. " << lastsource + 1 <<
") during parsing. Please fix them or set the appropriate flag.");
216 throw storm::exceptions::WrongFormatException()
217 <<
"Found deadlock states (e.g. " << lastsource + 1 <<
") during parsing. Please fix them or set the appropriate flag.";
221 if (source != lastsource) {
223 result.transitionMatrixBuilder.newRowGroup(currentChoice);
232 bool isMarkovianChoice =
false;
233 if (buf[0] ==
'!' &&
skipWord(buf) - buf == 1) {
234 isMarkovianChoice =
true;
237 result.markovianStates.set(source,
true);
239 isMarkovianChoice =
false;
247 bool encounteredNewDistribution =
false;
254 if (buf[0] ==
'\0') {
257 encounteredEOF =
true;
258 }
else if (buf[0] ==
'*') {
269 result.transitionMatrixBuilder.addNextValue(currentChoice, target, val);
270 if (isMarkovianChoice) {
271 result.exitRates[source] += val;
278 encounteredNewDistribution =
true;
280 }
while (!encounteredEOF && !encounteredNewDistribution);
287 if (!dontFixDeadlocks) {
288 for (uint_fast64_t index = lastsource + 1; index <= firstPassResult.highestStateIndex; ++index) {
289 result.markovianStates.set(index,
true);
290 result.exitRates[index] = storm::utility::one<ValueType>();
291 result.transitionMatrixBuilder.newRowGroup(currentChoice);
292 result.transitionMatrixBuilder.addNextValue(currentChoice, index, storm::utility::one<ValueType>());
296 STORM_LOG_ERROR(
"Found deadlock states (e.g. " << lastsource + 1 <<
") during parsing. Please fix them or set the appropriate flag.");
297 throw storm::exceptions::WrongFormatException()
298 <<
"Found deadlock states (e.g. " << lastsource + 1 <<
") during parsing. Please fix them or set the appropriate flag.";
304template<
typename ValueType>
306 std::string
const& filename) {
308 setlocale(LC_NUMERIC,
"C");
312 char const* buf = file.
getData();
314 return secondPass(buf, firstPass(buf));
Opens a file and maps it to memory providing a char* containing the file content.
char const * getData() const
Returns a pointer to the beginning of the mapped file data.
A class providing the functionality to parse the transitions of a Markov automaton.
static Result parseMarkovAutomatonTransitions(std::string const &filename)
Parses the given file under the assumption that it contains a Markov automaton specified in the appro...
#define STORM_LOG_ERROR(message)
SettingsType const & getModule()
Get module.
char const * forwardToLineEnd(char const *buffer)
Encapsulates the usage of function @strcspn to forward to the end of the line (next char is the newli...
char const * skipWord(char const *buf)
Skips all numbers, letters and special characters.
double checked_strtod(char const *str, char const **end)
Calls strtod() internally and checks if the new pointer is different from the original one,...
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,...
char const * forwardToNextLine(char const *buffer)
Encapsulates the usage of function @strchr to forward to the next line.
char const * trimWhitespaces(char const *buf)
Skips spaces, tabs, newlines and carriage returns.
A structure representing the result of the parser.