Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
MarkovAutomatonSparseTransitionParser.cpp
Go to the documentation of this file.
2
11
12namespace storm {
13namespace parser {
14
15using namespace storm::utility::cstring;
16
17template<typename ValueType>
18typename MarkovAutomatonSparseTransitionParser<ValueType>::FirstPassResult MarkovAutomatonSparseTransitionParser<ValueType>::firstPass(char const* buf) {
19 MarkovAutomatonSparseTransitionParser::FirstPassResult result;
20
21 bool dontFixDeadlocks = storm::settings::getModule<storm::settings::modules::BuildSettings>().isDontFixDeadlocksSet();
22
23 // Skip the format hint if it is there.
24 buf = trimWhitespaces(buf);
25 if (buf[0] < '0' || buf[0] > '9') {
26 buf = forwardToLineEnd(buf);
27 buf = trimWhitespaces(buf);
28 }
29
30 // Now read the transitions.
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) {
37 // At the current point, the next thing to read is the source state of the next choice to come.
38 source = checked_strtol(buf, &buf);
39
40 // Check if we encountered a state index that is bigger than all previously seen ones and record it if necessary.
41 if (source > result.highestStateIndex) {
42 result.highestStateIndex = source;
43 }
44
45 // If we have skipped some states, we need to reserve the space for the self-loop insertion in the second pass.
46 if (source > lastsource + 1) {
47 if (!dontFixDeadlocks) {
48 result.numberOfNonzeroEntries += source - lastsource - 1;
49 result.numberOfChoices += source - lastsource - 1;
50 } else {
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.";
54 }
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.";
58 }
59
60 ++result.numberOfChoices;
61
62 // If we have moved to the next state, we need to clear the flag that stores whether or not the source has a Markovian or probabilistic choice.
63 if (source != lastsource) {
64 stateHasMarkovianChoice = false;
65 stateHasProbabilisticChoice = false;
66 }
67
68 // Record that the current source was the last source.
69 lastsource = source;
70
71 buf = trimWhitespaces(buf);
72
73 // Depending on the action name, the choice is either a probabilitic one or a markovian one.
74 bool isMarkovianChoice = false;
75 if (buf[0] == '!' && skipWord(buf) - buf == 1) {
76 isMarkovianChoice = true;
77 } else {
78 isMarkovianChoice = false;
79 }
80 buf = skipWord(buf);
81
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.";
86 }
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.";
94 }
95 stateHasMarkovianChoice = true;
96 } else {
97 stateHasProbabilisticChoice = true;
98 }
99
100 // Go to the next line where the transitions start.
101 buf = forwardToNextLine(buf);
102
103 // Now that we have the source state and the information whether or not the current choice is probabilistic or Markovian, we need to read the list of
104 // successors and the probabilities/rates.
105 bool hasSuccessorState = false;
106 bool encounteredNewDistribution = false;
107 uint_fast64_t lastSuccessorState = 0;
108
109 // At this point, we need to check whether there is an additional successor or we have reached the next choice for the same or a different state.
110 do {
111 buf = trimWhitespaces(buf);
112 // If the end of the file was reached, we need to abort and check whether we are in a legal state.
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 << ".";
118 } else {
119 // If there was at least one successor for the current choice, this is legal and we need to move on.
120 encounteredEOF = true;
121 }
122 } else if (buf[0] == '*') {
123 // As we have encountered a "*", we know that there is an additional successor state for the current choice.
124 buf = skipWord(buf);
125
126 // Now we need to read the successor state and check if we already saw a higher state index.
127 target = checked_strtol(buf, &buf);
128 if (target > result.highestStateIndex) {
129 result.highestStateIndex = target;
130 }
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 << ".";
134 }
135
136 // And the corresponding probability/rate.
137 double val = checked_strtod(buf, &buf);
138 if (val < 0.0) {
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 << ".";
142 }
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 << ".";
147 }
148
149 // We need to record that we found at least one successor state for the current choice.
150 hasSuccessorState = true;
151 lastSuccessorState = target;
152
153 // As we found a new successor, we need to increase the number of nonzero entries.
154 ++result.numberOfNonzeroEntries;
155
156 buf = forwardToNextLine(buf);
157 } else {
158 // If it was not a "*", we have to assume that we encountered the beginning of a new choice definition. In this case, we don't move the pointer
159 // to the buffer, because we still need to read the new source state.
160 encounteredNewDistribution = true;
161 }
162 } while (!encounteredEOF && !encounteredNewDistribution);
163 }
164
165 // If there are some states with indices that are behind the last source for which no transition was specified,
166 // we need to reserve some space for introducing self-loops later.
167 if (!dontFixDeadlocks) {
168 result.numberOfNonzeroEntries += result.highestStateIndex - lastsource;
169 result.numberOfChoices += result.highestStateIndex - lastsource;
170 } else {
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.";
174 }
175
176 return result;
177}
178
179template<typename ValueType>
180typename MarkovAutomatonSparseTransitionParser<ValueType>::Result MarkovAutomatonSparseTransitionParser<ValueType>::secondPass(
181 char const* buf, FirstPassResult const& firstPassResult) {
182 Result result(firstPassResult);
183
184 bool dontFixDeadlocks = storm::settings::getModule<storm::settings::modules::BuildSettings>().isDontFixDeadlocksSet();
185
186 // Skip the format hint if it is there.
187 buf = trimWhitespaces(buf);
188 if (buf[0] < '0' || buf[0] > '9') {
189 buf = forwardToLineEnd(buf);
190 buf = trimWhitespaces(buf);
191 }
192
193 // Now read the transitions.
194 uint_fast64_t source, target = 0;
195 uint_fast64_t lastsource = 0;
196 bool encounteredEOF = false;
197 uint_fast64_t currentChoice = 0;
198
199 // The first choice of the first state already starts a new row group of the matrix.
200 result.transitionMatrixBuilder.newRowGroup(0);
201
202 while (buf[0] != '\0' && !encounteredEOF) {
203 // At the current point, the next thing to read is the source state of the next choice to come.
204 source = checked_strtol(buf, &buf);
205
206 // If we have skipped some states, we need to insert self-loops if requested.
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);
212 ++currentChoice;
213 }
214 } else {
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.";
218 }
219 }
220
221 if (source != lastsource) {
222 // If we skipped to a new state we need to create a new row group for the choices of the new state.
223 result.transitionMatrixBuilder.newRowGroup(currentChoice);
224 }
225
226 // Record that the current source was the last source.
227 lastsource = source;
228
229 buf = trimWhitespaces(buf);
230
231 // Depending on the action name, the choice is either a probabilitic one or a markovian one.
232 bool isMarkovianChoice = false;
233 if (buf[0] == '!' && skipWord(buf) - buf == 1) {
234 isMarkovianChoice = true;
235
236 // Mark the current state as a Markovian one.
237 result.markovianStates.set(source, true);
238 } else {
239 isMarkovianChoice = false;
240 }
241
242 // Go to the next line where the transitions start.
243 buf = forwardToNextLine(buf);
244
245 // Now that we have the source state and the information whether or not the current choice is probabilistic or Markovian, we need to read the list of
246 // successors and the probabilities/rates.
247 bool encounteredNewDistribution = false;
248
249 // At this point, we need to check whether there is an additional successor or we have reached the next choice for the same or a different state.
250 do {
251 buf = trimWhitespaces(buf);
252
253 // If the end of the file was reached, we need to abort and check whether we are in a legal state.
254 if (buf[0] == '\0') {
255 // Under the assumption that the currently open choice has at least one successor (which is given after the first run)
256 // we may legally stop reading here.
257 encounteredEOF = true;
258 } else if (buf[0] == '*') {
259 // As we have encountered a "*", we know that there is an additional successor state for the current choice.
260 buf = skipWord(buf);
261
262 // Now we need to read the successor state and check if we already saw a higher state index.
263 target = checked_strtol(buf, &buf);
264
265 // And the corresponding probability/rate.
266 double val = checked_strtod(buf, &buf);
267
268 // Record the value as well as the exit rate in case of a Markovian choice.
269 result.transitionMatrixBuilder.addNextValue(currentChoice, target, val);
270 if (isMarkovianChoice) {
271 result.exitRates[source] += val;
272 }
273
274 buf = forwardToNextLine(buf);
275 } else {
276 // If it was not a "*", we have to assume that we encountered the beginning of a new choice definition. In this case, we don't move the pointer
277 // to the buffer, because we still need to read the new source state.
278 encounteredNewDistribution = true;
279 }
280 } while (!encounteredEOF && !encounteredNewDistribution);
281
282 ++currentChoice;
283 }
284
285 // If there are some states with indices that are behind the last source for which no transition was specified,
286 // we need to insert the self-loops now. Note that we assume all these states to be Markovian.
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>());
293 ++currentChoice;
294 }
295 } else {
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.";
299 }
300
301 return result;
302}
303
304template<typename ValueType>
306 std::string const& filename) {
307 // Set the locale to correctly recognize floating point numbers.
308 setlocale(LC_NUMERIC, "C");
309
310 // Open file and prepare pointer to buffer.
311 MappedFile file(filename.c_str());
312 char const* buf = file.getData();
313
314 return secondPass(buf, firstPass(buf));
315}
316
318
319} // namespace parser
320} // namespace storm
Opens a file and maps it to memory providing a char* containing the file content.
Definition MappedFile.h:33
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)
Definition logging.h:31
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...
Definition cstring.cpp:74
char const * skipWord(char const *buf)
Skips all numbers, letters and special characters.
Definition cstring.cpp:55
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:39
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 * forwardToNextLine(char const *buffer)
Encapsulates the usage of function @strchr to forward to the next line.
Definition cstring.cpp:81
char const * trimWhitespaces(char const *buf)
Skips spaces, tabs, newlines and carriage returns.
Definition cstring.cpp:66
LabParser.cpp.
Definition cli.cpp:18