Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
NondeterministicSparseTransitionParser.cpp
Go to the documentation of this file.
2
3#include <string>
4
10
13
15
18namespace storm {
19namespace parser {
20
21using namespace storm::utility::cstring;
22
23template<typename ValueType>
26 return NondeterministicSparseTransitionParser::parse(filename, false, emptyMatrix);
27}
28
29template<typename ValueType>
30template<typename MatrixValueType>
32 std::string const& filename, storm::storage::SparseMatrix<MatrixValueType> const& modelInformation) {
33 return NondeterministicSparseTransitionParser::parse(filename, true, modelInformation);
34}
35
36template<typename ValueType>
37template<typename MatrixValueType>
39 std::string const& filename, bool isRewardFile, storm::storage::SparseMatrix<MatrixValueType> const& modelInformation) {
40 // Enforce locale where decimal point is '.'.
41 setlocale(LC_NUMERIC, "C");
42
43 // Open file.
44 MappedFile file(filename.c_str());
45 char const* buf = file.getData();
46
47 // Perform first pass, i.e. obtain number of columns, rows and non-zero elements.
49 NondeterministicSparseTransitionParser::firstPass(file.getData(), isRewardFile, modelInformation);
50
51 // If first pass returned zero, the file format was wrong.
52 if (firstPass.numberOfNonzeroEntries == 0) {
53 STORM_LOG_ERROR("Error while parsing " << filename << ": erroneous file format.");
54 throw storm::exceptions::WrongFormatException() << "Error while parsing " << filename << ": erroneous file format.";
55 }
56
57 // Perform second pass.
58
59 // Skip the format hint if it is there.
60 buf = trimWhitespaces(buf);
61 if (buf[0] < '0' || buf[0] > '9') {
62 buf = forwardToLineEnd(buf);
63 buf = trimWhitespaces(buf);
64 }
65
66 if (isRewardFile) {
67 // The reward matrix should match the size of the transition matrix.
68 if (firstPass.choices > modelInformation.getRowCount() || (uint_fast64_t)(firstPass.highestStateIndex + 1) > modelInformation.getColumnCount()) {
69 STORM_LOG_ERROR("Reward matrix size exceeds transition matrix size.");
70 throw storm::exceptions::OutOfRangeException() << "Reward matrix size exceeds transition matrix size.";
71 } else if (firstPass.choices != modelInformation.getRowCount()) {
72 STORM_LOG_ERROR("Reward matrix row count does not match transition matrix row count.");
73 throw storm::exceptions::OutOfRangeException() << "Reward matrix row count does not match transition matrix row count.";
74 } else if (firstPass.numberOfNonzeroEntries > modelInformation.getEntryCount()) {
75 STORM_LOG_ERROR("The reward matrix has more entries than the transition matrix. There must be a reward for a non existent transition");
76 throw storm::exceptions::OutOfRangeException() << "The reward matrix has more entries than the transition matrix.";
77 } else {
78 firstPass.highestStateIndex = modelInformation.getColumnCount() - 1;
79 }
80 }
81
82 // Create the matrix builder.
83 // The matrix to be build should have as many columns as we have nodes and as many rows as we have choices.
84 // Those two values, as well as the number of nonzero elements, was been calculated in the first run.
85 STORM_LOG_INFO("Attempting to create matrix of size " << firstPass.choices << " x " << (firstPass.highestStateIndex + 1) << " with "
86 << firstPass.numberOfNonzeroEntries << " entries.");
88 if (!isRewardFile) {
90 true, true, firstPass.highestStateIndex + 1);
91 } else {
93 true, true, modelInformation.getRowGroupCount());
94 }
95
96 // Initialize variables for the parsing run.
97 uint_fast64_t source = 0, target = 0, lastSource = 0, choice = 0, lastChoice = 0, curRow = 0;
98 double val = 0.0;
99 bool dontFixDeadlocks = storm::settings::getModule<storm::settings::modules::BuildSettings>().isDontFixDeadlocksSet();
100 bool hadDeadlocks = false;
101
102 // The first state already starts a new row group of the matrix.
103 matrixBuilder.newRowGroup(0);
104
105 // Read all transitions from file.
106 while (buf[0] != '\0') {
107 // Read source state and choice.
108 source = checked_strtol(buf, &buf);
109 choice = checked_strtol(buf, &buf);
110
111 if (isRewardFile) {
112 // If we have switched the source state, we possibly need to insert the rows of the last
113 // source state.
114 if (source != lastSource) {
115 curRow += ((modelInformation.getRowGroupIndices())[lastSource + 1] - (modelInformation.getRowGroupIndices())[lastSource]) - (lastChoice + 1);
116 }
117
118 // If we skipped some states, we need to reserve empty rows for all their nondeterministic
119 // choices and create the row groups.
120 for (uint_fast64_t i = lastSource + 1; i < source; ++i) {
121 matrixBuilder.newRowGroup(modelInformation.getRowGroupIndices()[i]);
122 curRow += ((modelInformation.getRowGroupIndices())[i + 1] - (modelInformation.getRowGroupIndices())[i]);
123 }
124
125 // If we moved to the next source, we need to open the next row group.
126 if (source != lastSource) {
127 matrixBuilder.newRowGroup(modelInformation.getRowGroupIndices()[source]);
128 }
129
130 // If we advanced to the next state, but skipped some choices, we have to reserve rows
131 // for them
132 if (source != lastSource) {
133 curRow += choice + 1;
134 } else if (choice != lastChoice) {
135 curRow += choice - lastChoice;
136 }
137 } else {
138 // Increase line count if we have either finished reading the transitions of a certain state
139 // or we have finished reading one nondeterministic choice of a state.
140 if ((source != lastSource || choice != lastChoice)) {
141 ++curRow;
142 }
143
144 // Check if we have skipped any source node, i.e. if any node has no
145 // outgoing transitions. If so, insert a self-loop.
146 // Also begin a new rowGroup for the skipped state.
147 for (uint_fast64_t node = lastSource + 1; node < source; node++) {
148 hadDeadlocks = true;
149 if (!dontFixDeadlocks) {
150 matrixBuilder.newRowGroup(curRow);
151 matrixBuilder.addNextValue(curRow, node, 1);
152 ++curRow;
153 STORM_LOG_INFO("Warning while parsing " << filename << ": node " << node << " has no outgoing transitions. A self-loop was inserted.");
154 } else {
155 STORM_LOG_ERROR("Error while parsing " << filename << ": node " << node << " has no outgoing transitions.");
156 }
157 }
158 if (source != lastSource) {
159 // Create a new rowGroup for the source, if this is the first choice we encounter for this state.
160 matrixBuilder.newRowGroup(curRow);
161 }
162 }
163
164 // Read target and value and write it to the matrix.
165 target = checked_strtol(buf, &buf);
166 val = checked_strtod(buf, &buf);
167 matrixBuilder.addNextValue(curRow, target, val);
168
169 lastSource = source;
170 lastChoice = choice;
171
172 // Proceed to beginning of next line in file and next row in matrix.
173 buf = forwardToLineEnd(buf);
174
175 buf = trimWhitespaces(buf);
176 }
177
178 if (dontFixDeadlocks && hadDeadlocks && !isRewardFile)
179 throw storm::exceptions::WrongFormatException() << "Some of the states do not have outgoing transitions.";
180
181 // Since we assume the transition rewards are for the transitions of the model, we copy the rowGroupIndices.
182 if (isRewardFile) {
183 for (uint_fast64_t node = lastSource + 1; node < modelInformation.getRowGroupCount(); node++) {
184 matrixBuilder.newRowGroup(modelInformation.getRowGroupIndices()[node]);
185 }
186 }
187
188 // Finally, build the actual matrix, test and return it.
189 storm::storage::SparseMatrix<ValueType> resultMatrix = matrixBuilder.build();
190
191 // Since we cannot check if each transition for which there is a reward in the reward file also exists in the transition matrix during parsing, we have to
192 // do it afterwards.
193 if (isRewardFile && !resultMatrix.isSubmatrixOf(modelInformation)) {
194 STORM_LOG_ERROR("There are rewards for non existent transitions given in the reward file.");
195 throw storm::exceptions::WrongFormatException() << "There are rewards for non existent transitions given in the reward file.";
196 }
197
198 return resultMatrix;
199}
200
201template<typename ValueType>
202template<typename MatrixValueType>
203typename NondeterministicSparseTransitionParser<ValueType>::FirstPassResult NondeterministicSparseTransitionParser<ValueType>::firstPass(
204 char const* buf, bool isRewardFile, storm::storage::SparseMatrix<MatrixValueType> const& modelInformation) {
205 // Check file header and extract number of transitions.
206
207 // Skip the format hint if it is there.
208 buf = trimWhitespaces(buf);
209 if (buf[0] < '0' || buf[0] > '9') {
210 buf = forwardToLineEnd(buf);
211 buf = trimWhitespaces(buf);
212 }
213
214 // Read all transitions.
215 uint_fast64_t source = 0, target = 0, choice = 0, lastChoice = 0, lastSource = 0, lastTarget = -1;
216 double val = 0.0;
217 typename NondeterministicSparseTransitionParser<ValueType>::FirstPassResult result;
218
219 // Since the first line is already a new choice but is not covered below, that has to be covered here.
220 result.choices = 1;
221
222 while (buf[0] != '\0') {
223 // Read source state and choice.
224 source = checked_strtol(buf, &buf);
225
226 // Read the name of the nondeterministic choice.
227 choice = checked_strtol(buf, &buf);
228
229 if (source < lastSource) {
230 STORM_LOG_ERROR("The current source state " << source << " is smaller than the last one " << lastSource << ".");
231 throw storm::exceptions::InvalidArgumentException()
232 << "The current source state " << source << " is smaller than the last one " << lastSource << ".";
233 }
234
235 // Check if we encountered a state index that is bigger than all previously seen.
236 if (source > result.highestStateIndex) {
237 result.highestStateIndex = source;
238 }
239
240 if (isRewardFile) {
241 // Make sure that the highest state index of the reward file is not higher than the highest state index of the corresponding model.
242 if (result.highestStateIndex > modelInformation.getColumnCount() - 1) {
243 STORM_LOG_ERROR("State index " << result.highestStateIndex << " found. This exceeds the highest state index of the model, which is "
244 << modelInformation.getColumnCount() - 1 << " .");
245 throw storm::exceptions::OutOfRangeException()
246 << "State index " << result.highestStateIndex << " found. This exceeds the highest state index of the model, which is "
247 << modelInformation.getColumnCount() - 1 << " .";
248 }
249
250 // If we have switched the source state, we possibly need to insert rows for skipped choices of the last
251 // source state.
252 if (source != lastSource) {
253 // number of choices skipped = number of choices of last state - number of choices read
254 result.choices +=
255 ((modelInformation.getRowGroupIndices())[lastSource + 1] - (modelInformation.getRowGroupIndices())[lastSource]) - (lastChoice + 1);
256 }
257
258 // If we skipped some states, we need to reserve empty rows for all their nondeterministic
259 // choices.
260 for (uint_fast64_t i = lastSource + 1; i < source; ++i) {
261 result.choices += ((modelInformation.getRowGroupIndices())[i + 1] - (modelInformation.getRowGroupIndices())[i]);
262 }
263
264 // If we advanced to the next state, but skipped some choices, we have to reserve rows
265 // for them.
266 if (source != lastSource) {
267 result.choices += choice + 1;
268 } else if (choice != lastChoice) {
269 result.choices += choice - lastChoice;
270 }
271 } else {
272 // If we have skipped some states, we need to reserve the space for the self-loop insertion
273 // in the second pass.
274 if (source > lastSource + 1) {
275 result.numberOfNonzeroEntries += source - lastSource - 1;
276 result.choices += source - lastSource - 1;
277 }
278
279 if (source != lastSource || choice != lastChoice) {
280 // If we have switched the source state or the nondeterministic choice, we need to
281 // reserve one row more.
282 ++result.choices;
283 }
284 }
285
286 // Read target and check if we encountered a state index that is bigger than all previously seen.
287 target = checked_strtol(buf, &buf);
288
289 if (target > result.highestStateIndex) {
290 result.highestStateIndex = target;
291 }
292
293 // Also, have we already seen this transition?
294 if (target == lastTarget && choice == lastChoice && source == lastSource) {
295 STORM_LOG_ERROR("The same transition (" << source << ", " << choice << ", " << target << ") is given twice.");
296 throw storm::exceptions::InvalidArgumentException() << "The same transition (" << source << ", " << choice << ", " << target << ") is given twice.";
297 }
298
299 // Read value and check whether it's positive.
300 val = checked_strtod(buf, &buf);
301 if (!isRewardFile && (val < 0.0 || val > 1.0)) {
302 STORM_LOG_ERROR("Expected a positive probability but got \"" << std::string(buf, 0, 16) << "\".");
303 NondeterministicSparseTransitionParser::FirstPassResult nullResult;
304 return nullResult;
305 } else if (val < 0.0) {
306 STORM_LOG_ERROR("Expected a positive reward value but got \"" << std::string(buf, 0, 16) << "\".");
307 NondeterministicSparseTransitionParser::FirstPassResult nullResult;
308 return nullResult;
309 }
310
311 lastChoice = choice;
312 lastSource = source;
313 lastTarget = target;
314
315 // Increase number of non-zero values.
316 result.numberOfNonzeroEntries++;
317
318 // The PRISM output format lists the name of the transition in the fourth column,
319 // but omits the fourth column if it is an internal action. In either case we can skip to the end of the line.
320 buf = forwardToLineEnd(buf);
321
322 buf = trimWhitespaces(buf);
323 }
324
325 if (isRewardFile) {
326 // If not all rows were filled for the last state, we need to insert them.
327 result.choices += ((modelInformation.getRowGroupIndices())[lastSource + 1] - (modelInformation.getRowGroupIndices())[lastSource]) - (lastChoice + 1);
328
329 // If we skipped some states, we need to reserve empty rows for all their nondeterministic
330 // choices.
331 for (uint_fast64_t i = lastSource + 1; i < modelInformation.getRowGroupIndices().size() - 1; ++i) {
332 result.choices += ((modelInformation.getRowGroupIndices())[i + 1] - (modelInformation.getRowGroupIndices())[i]);
333 }
334 }
335
336 return result;
337}
338
339template class NondeterministicSparseTransitionParser<double>;
341 std::string const& filename, storm::storage::SparseMatrix<double> const& modelInformation);
342template storm::storage::SparseMatrix<double> NondeterministicSparseTransitionParser<double>::parse(
343 std::string const& filename, bool isRewardFile, storm::storage::SparseMatrix<double> const& modelInformation);
344
345#ifdef STORM_HAVE_CARL
346template class NondeterministicSparseTransitionParser<storm::Interval>;
347
348template storm::storage::SparseMatrix<storm::Interval> NondeterministicSparseTransitionParser<storm::Interval>::parseNondeterministicTransitionRewards<double>(
349 std::string const& filename, storm::storage::SparseMatrix<double> const& modelInformation);
350template storm::storage::SparseMatrix<storm::Interval> NondeterministicSparseTransitionParser<storm::Interval>::parse<double>(
351 std::string const& filename, bool isRewardFile, storm::storage::SparseMatrix<double> const& modelInformation);
352#endif
353
354} // namespace parser
355} // namespace storm
Opens a file and maps it to memory providing a char* containing the file content.
Definition MappedFile.h:33
A class providing the functionality to parse the transitions of a nondeterministic model.
static storm::storage::SparseMatrix< ValueType > parseNondeterministicTransitionRewards(std::string const &filename, storm::storage::SparseMatrix< MatrixValueType > const &modelInformation)
Load a nondeterministic transition system from file and create a sparse adjacency matrix whose entrie...
static storm::storage::SparseMatrix< ValueType > parseNondeterministicTransitions(std::string const &filename)
Load a nondeterministic transition system from file and create a sparse adjacency matrix whose entrie...
A class that can be used to build a sparse matrix by adding value by value.
void addNextValue(index_type row, index_type column, value_type const &value)
Sets the matrix entry at the given row and column to the given value.
void newRowGroup(index_type startingRow)
Starts a new row group in the matrix.
SparseMatrix< value_type > build(index_type overriddenRowCount=0, index_type overriddenColumnCount=0, index_type overriddenRowGroupCount=0)
A class that holds a possibly non-square matrix in the compressed row storage format.
index_type getEntryCount() const
Returns the number of entries in the matrix.
index_type getRowGroupCount() const
Returns the number of row groups in the matrix.
bool isSubmatrixOf(SparseMatrix< OtherValueType > const &matrix) const
Checks if the current matrix is a submatrix of the given matrix, where a matrix A is called a submatr...
index_type getColumnCount() const
Returns the number of columns of the matrix.
std::vector< index_type > const & getRowGroupIndices() const
Returns the grouping of rows of this matrix.
index_type getRowCount() const
Returns the number of rows of the matrix.
#define STORM_LOG_INFO(message)
Definition logging.h:29
#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
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 * trimWhitespaces(char const *buf)
Skips spaces, tabs, newlines and carriage returns.
Definition cstring.cpp:66
LabParser.cpp.
Definition cli.cpp:18
A structure representing the result of the first pass of this parser.
uint_fast64_t numberOfNonzeroEntries
The total number of non-zero entries of the model.
uint_fast64_t highestStateIndex
The highest state index that appears in the model.
uint_fast64_t choices
The total number of nondeterministic choices within the transition system.