23template<
typename ValueType>
26 return NondeterministicSparseTransitionParser::parse(filename,
false, emptyMatrix);
29template<
typename ValueType>
30template<
typename MatrixValueType>
33 return NondeterministicSparseTransitionParser::parse(filename,
true, modelInformation);
36template<
typename ValueType>
37template<
typename MatrixValueType>
41 setlocale(LC_NUMERIC,
"C");
45 char const* buf = file.getData();
49 NondeterministicSparseTransitionParser::firstPass(file.getData(), isRewardFile, modelInformation);
53 STORM_LOG_ERROR(
"Error while parsing " << filename <<
": erroneous file format.");
54 throw storm::exceptions::WrongFormatException() <<
"Error while parsing " << filename <<
": erroneous file format.";
61 if (buf[0] <
'0' || buf[0] >
'9') {
70 throw storm::exceptions::OutOfRangeException() <<
"Reward matrix size exceeds transition matrix size.";
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.";
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.";
97 uint_fast64_t source = 0, target = 0, lastSource = 0, choice = 0, lastChoice = 0, curRow = 0;
100 bool hadDeadlocks =
false;
106 while (buf[0] !=
'\0') {
114 if (source != lastSource) {
120 for (uint_fast64_t i = lastSource + 1;
i < source; ++
i) {
126 if (source != lastSource) {
132 if (source != lastSource) {
133 curRow += choice + 1;
134 }
else if (choice != lastChoice) {
135 curRow += choice - lastChoice;
140 if ((source != lastSource || choice != lastChoice)) {
147 for (uint_fast64_t node = lastSource + 1; node < source; node++) {
149 if (!dontFixDeadlocks) {
153 STORM_LOG_INFO(
"Warning while parsing " << filename <<
": node " << node <<
" has no outgoing transitions. A self-loop was inserted.");
155 STORM_LOG_ERROR(
"Error while parsing " << filename <<
": node " << node <<
" has no outgoing transitions.");
158 if (source != lastSource) {
178 if (dontFixDeadlocks && hadDeadlocks && !isRewardFile)
179 throw storm::exceptions::WrongFormatException() <<
"Some of the states do not have outgoing transitions.";
183 for (uint_fast64_t node = lastSource + 1; node < modelInformation.
getRowGroupCount(); node++) {
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.";
201template<
typename ValueType>
202template<
typename MatrixValueType>
203typename NondeterministicSparseTransitionParser<ValueType>::FirstPassResult NondeterministicSparseTransitionParser<ValueType>::firstPass(
209 if (buf[0] <
'0' || buf[0] >
'9') {
215 uint_fast64_t source = 0, target = 0, choice = 0, lastChoice = 0, lastSource = 0, lastTarget = -1;
217 typename NondeterministicSparseTransitionParser<ValueType>::FirstPassResult result;
222 while (buf[0] !=
'\0') {
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 <<
".";
236 if (source > result.highestStateIndex) {
237 result.highestStateIndex = source;
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 "
245 throw storm::exceptions::OutOfRangeException()
246 <<
"State index " << result.highestStateIndex <<
" found. This exceeds the highest state index of the model, which is "
252 if (source != lastSource) {
260 for (uint_fast64_t i = lastSource + 1;
i < source; ++
i) {
266 if (source != lastSource) {
267 result.choices += choice + 1;
268 }
else if (choice != lastChoice) {
269 result.choices += choice - lastChoice;
274 if (source > lastSource + 1) {
275 result.numberOfNonzeroEntries += source - lastSource - 1;
276 result.choices += source - lastSource - 1;
279 if (source != lastSource || choice != lastChoice) {
289 if (target > result.highestStateIndex) {
290 result.highestStateIndex = target;
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.";
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;
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;
316 result.numberOfNonzeroEntries++;
331 for (uint_fast64_t i = lastSource + 1;
i < modelInformation.
getRowGroupIndices().size() - 1; ++
i) {
339template class NondeterministicSparseTransitionParser<double>;
345#ifdef STORM_HAVE_CARL
346template class NondeterministicSparseTransitionParser<storm::Interval>;
Opens a file and maps it to memory providing a char* containing the file content.
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)
#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...
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 * trimWhitespaces(char const *buf)
Skips spaces, tabs, newlines and carriage returns.
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.