From cc71a002f4bd9bc81d7401812d5f3f50e2f6a118 Mon Sep 17 00:00:00 2001
From: masawei <manuel.sascha.weiand@rwth-aachen.de>
Date: Thu, 2 Jan 2014 16:46:53 +0100
Subject: [PATCH] Refactored NondeterministicSparseTransitionParser.h/.cpp.
-Changed structure to conform to common parser structure: static class with two passes and structs to handle value passing.
-Killed all warnings (signed unsigned interger compare)
-Made parser more flexible: Is now able to ignore arbitrarily many columns after the value column (instead of only one).
-Threw out a number of unnecessary includes.
-more...
Next up: Refactor NondeterministicModelParser.h/.cpp
Former-commit-id: fd2fdb7fdf88af38f733ed6f83ef2d353a614e2f
---
.../DeterministicSparseTransitionParser.cpp | 18 +-
.../DeterministicSparseTransitionParser.h | 4 +-
.../MarkovAutomatonSparseTransitionParser.cpp | 2 +-
src/parser/NondeterministicModelParser.cpp | 18 +-
...NondeterministicSparseTransitionParser.cpp | 565 +++++++-----------
.../NondeterministicSparseTransitionParser.h | 113 +++-
src/parser/Parser.cpp | 23 +
src/parser/Parser.h | 5 +
8 files changed, 373 insertions(+), 375 deletions(-)
diff --git a/src/parser/DeterministicSparseTransitionParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp
index 03b94c78c..2ac9098bd 100644
--- a/src/parser/DeterministicSparseTransitionParser.cpp
+++ b/src/parser/DeterministicSparseTransitionParser.cpp
@@ -30,12 +30,14 @@ namespace parser {
storm::storage::SparseMatrix<double> DeterministicSparseTransitionParser::parseDeterministicTransitions(std::string const& filename, bool insertDiagonalEntriesIfMissing) {
- return DeterministicSparseTransitionParser::parse(filename, false, insertDiagonalEntriesIfMissing);
+ RewardMatrixInformationStruct nullInformation;
+
+ return DeterministicSparseTransitionParser::parse(filename, false, nullInformation, insertDiagonalEntriesIfMissing);
}
storm::storage::SparseMatrix<double> DeterministicSparseTransitionParser::parseDeterministicTransitionRewards(std::string const& filename, RewardMatrixInformationStruct const& rewardMatrixInformation) {
- return DeterministicSparseTransitionParser::parse(filename, true, false, rewardMatrixInformation);
+ return DeterministicSparseTransitionParser::parse(filename, true, rewardMatrixInformation);
}
DeterministicSparseTransitionParser::FirstPassResult DeterministicSparseTransitionParser::firstPass(char* buf, SupportedLineEndingsEnum lineEndings, bool insertDiagonalEntriesIfMissing) {
@@ -44,7 +46,7 @@ DeterministicSparseTransitionParser::FirstPassResult DeterministicSparseTransiti
// Skip the format hint if it is there.
buf = trimWhitespaces(buf);
- if(buf[0] != '0') {
+ if(buf[0] < '0' || buf[0] > '9') {
buf = storm::parser::forwardToNextLine(buf, lineEndings);
}
@@ -53,7 +55,7 @@ DeterministicSparseTransitionParser::FirstPassResult DeterministicSparseTransiti
bool rowHadDiagonalEntry = false;
while (buf[0] != '\0') {
- // Read the transition..
+ // Read the transition.
row = checked_strtol(buf, &buf);
col = checked_strtol(buf, &buf);
// The actual read value is not needed here.
@@ -106,7 +108,7 @@ DeterministicSparseTransitionParser::FirstPassResult DeterministicSparseTransiti
return result;
}
-storm::storage::SparseMatrix<double> DeterministicSparseTransitionParser::parse(std::string const& filename, bool rewardFile, bool insertDiagonalEntriesIfMissing, RewardMatrixInformationStruct const& rewardMatrixInformation) {
+storm::storage::SparseMatrix<double> DeterministicSparseTransitionParser::parse(std::string const& filename, bool isRewardFile, RewardMatrixInformationStruct const& rewardMatrixInformation, bool insertDiagonalEntriesIfMissing) {
// Enforce locale where decimal point is '.'.
setlocale(LC_NUMERIC, "C");
@@ -138,11 +140,11 @@ storm::storage::SparseMatrix<double> DeterministicSparseTransitionParser::parse(
// Skip the format hint if it is there.
buf = trimWhitespaces(buf);
- if(buf[0] != '0') {
+ if(buf[0] < '0' || buf[0] > '9') {
buf = storm::parser::forwardToNextLine(buf, lineEndings);
}
- if(rewardFile) {
+ if(isRewardFile) {
// The reward matrix should match the size of the transition matrix.
if (firstPass.highestStateIndex + 1 > rewardMatrixInformation.rowCount || firstPass.highestStateIndex + 1 > rewardMatrixInformation.columnCount) {
LOG4CPLUS_ERROR(logger, "Reward matrix has more rows or columns than transition matrix.");
@@ -169,7 +171,7 @@ storm::storage::SparseMatrix<double> DeterministicSparseTransitionParser::parse(
// work, i.e. the values in the matrix will be at wrong places.
// Different parsing routines for transition systems and transition rewards.
- if(rewardFile) {
+ if(isRewardFile) {
while (buf[0] != '\0') {
// Read next transition.
diff --git a/src/parser/DeterministicSparseTransitionParser.h b/src/parser/DeterministicSparseTransitionParser.h
index 45ce9ac26..b9bb1621e 100644
--- a/src/parser/DeterministicSparseTransitionParser.h
+++ b/src/parser/DeterministicSparseTransitionParser.h
@@ -59,7 +59,7 @@ private:
*
* @param buffer The buffer that cointains the input.
* @param lineEndings The line endings that are to be used while parsing.
- * @param insertDiagonalEntriesIfMissing Flag determining whether
+ * @param insertDiagonalEntriesIfMissing A flag set iff entries on the primary diagonal of the matrix should be added in case they are missing in the parsed file.
* @return A structure representing the result of the first pass.
*/
static FirstPassResult firstPass(char* buffer, SupportedLineEndingsEnum lineEndings, bool insertDiagonalEntriesIfMissing = true);
@@ -74,7 +74,7 @@ private:
* @param rewardMatrixInformation A struct containing information that is used to check if the transition reward matrix fits to the rest of the model.
* @return A SparseMatrix containing the parsed file contents.
*/
- static storm::storage::SparseMatrix<double> parse(std::string const& filename, bool rewardFile, bool insertDiagonalEntriesIfMissing = false, RewardMatrixInformationStruct const& rewardMatrixInformation = nullptr);
+ static storm::storage::SparseMatrix<double> parse(std::string const& filename, bool isRewardFile, RewardMatrixInformationStruct const& rewardMatrixInformation, bool insertDiagonalEntriesIfMissing = false);
};
diff --git a/src/parser/MarkovAutomatonSparseTransitionParser.cpp b/src/parser/MarkovAutomatonSparseTransitionParser.cpp
index 1ca4f7264..15a7c5809 100644
--- a/src/parser/MarkovAutomatonSparseTransitionParser.cpp
+++ b/src/parser/MarkovAutomatonSparseTransitionParser.cpp
@@ -14,7 +14,7 @@ MarkovAutomatonSparseTransitionParser::FirstPassResult MarkovAutomatonSparseTran
// Skip the format hint if it is there.
buf = trimWhitespaces(buf);
- if(buf[0] != '0') {
+ if(buf[0] < '0' || buf[0] > '9') {
buf = storm::parser::forwardToNextLine(buf, lineEndings);
}
diff --git a/src/parser/NondeterministicModelParser.cpp b/src/parser/NondeterministicModelParser.cpp
index d4ab649ba..5f6e13360 100644
--- a/src/parser/NondeterministicModelParser.cpp
+++ b/src/parser/NondeterministicModelParser.cpp
@@ -29,23 +29,23 @@ namespace parser {
NondeterministicModelParserResultContainer<double> parseNondeterministicModel(std::string const & transitionSystemFile, std::string const & labelingFile,
std::string const & stateRewardFile, std::string const & transitionRewardFile) {
- NondeterministicSparseTransitionParserResult_t nondeterministicSparseTransitionParserResult(std::move(storm::parser::NondeterministicSparseTransitionParser(transitionSystemFile)));
- storm::storage::SparseMatrix<double> resultTransitionSystem(std::move(nondeterministicSparseTransitionParserResult.first));
+ NondeterministicSparseTransitionParser::Result transitionParserResult(std::move(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions(transitionSystemFile)));
+ storm::storage::SparseMatrix<double> transitions(std::move(transitionParserResult.transitionMatrix));
- uint_fast64_t stateCount = resultTransitionSystem.getColumnCount();
- uint_fast64_t rowCount = resultTransitionSystem.getRowCount();
+ uint_fast64_t stateCount = transitions.getColumnCount();
+ uint_fast64_t rowCount = transitions.getRowCount();
- storm::models::AtomicPropositionsLabeling resultLabeling(std::move(storm::parser::AtomicPropositionLabelingParser(stateCount, labelingFile)));
+ storm::models::AtomicPropositionsLabeling labeling(std::move(storm::parser::AtomicPropositionLabelingParser(stateCount, labelingFile)));
- NondeterministicModelParserResultContainer<double> result(std::move(resultTransitionSystem), std::move(nondeterministicSparseTransitionParserResult.second), std::move(resultLabeling));
+ NondeterministicModelParserResultContainer<double> result(std::move(transitions), std::move(transitionParserResult.rowMapping), std::move(labeling));
if (stateRewardFile != "") {
result.stateRewards.reset(storm::parser::SparseStateRewardParser::parseSparseStateReward(stateCount, stateRewardFile));
}
+
if (transitionRewardFile != "") {
- RewardMatrixInformationStruct* rewardMatrixInfo = new RewardMatrixInformationStruct(rowCount, stateCount, &result.rowMapping);
- result.transitionRewards.reset(storm::parser::NondeterministicSparseTransitionParser(transitionRewardFile, rewardMatrixInfo).first);
- delete rewardMatrixInfo;
+ RewardMatrixInformationStruct rewardMatrixInfo(rowCount, stateCount, &result.rowMapping);
+ result.transitionRewards.reset(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitionRewards(transitionRewardFile, rewardMatrixInfo).transitionMatrix);
}
return result;
}
diff --git a/src/parser/NondeterministicSparseTransitionParser.cpp b/src/parser/NondeterministicSparseTransitionParser.cpp
index 02a1e94f1..fa20585ec 100644
--- a/src/parser/NondeterministicSparseTransitionParser.cpp
+++ b/src/parser/NondeterministicSparseTransitionParser.cpp
@@ -1,5 +1,5 @@
/*!
- * TraParser.cpp
+ * NondeterministicSparseTransitionParser.cpp
*
* Created on: 20.11.2012
* Author: Gereon Kremer
@@ -7,380 +7,277 @@
#include "src/parser/NondeterministicSparseTransitionParser.h"
-#include <errno.h>
-#include <time.h>
-#include <sys/stat.h>
-#include <fcntl.h>
-#include <locale.h>
-
-#include <cstdlib>
-#include <cstdio>
-#include <cstring>
-#include <clocale>
-#include <iostream>
-#include <utility>
#include <string>
#include "src/settings/Settings.h"
#include "src/exceptions/FileIoException.h"
#include "src/exceptions/WrongFormatException.h"
-#include <cstdint>
+
#include "log4cplus/logger.h"
#include "log4cplus/loggingmacros.h"
extern log4cplus::Logger logger;
namespace storm {
-namespace parser {
+ namespace parser {
-/*!
- * @brief Perform first pass through the file and obtain overall number of
- * choices, number of non-zero cells and maximum node id.
- *
- * This method does the first pass through the transition file.
- *
- * It computes the overall number of nondeterministic choices, i.e. the
- * number of rows in the matrix that should be created.
- * It also calculates the overall number of non-zero cells, i.e. the number
- * of elements the matrix has to hold, and the maximum node id, i.e. the
- * number of columns of the matrix.
- *
- * @param buf Data to scan. Is expected to be some char array.
- * @param choices Overall number of choices.
- * @param maxnode Is set to highest id of all nodes.
- * @return The number of non-zero elements.
- */
-uint_fast64_t firstPass(char* buf, SupportedLineEndingsEnum lineEndings, uint_fast64_t& choices, int_fast64_t& maxnode, RewardMatrixInformationStruct* rewardMatrixInformation) {
- bool isRewardFile = rewardMatrixInformation != nullptr;
-
- /*
- * Check file header and extract number of transitions.
- */
- if (!isRewardFile) {
- // skip format hint
- buf = storm::parser::forwardToNextLine(buf, lineEndings);
- }
-
- /*
- * Read all transitions.
- */
- int_fast64_t source, target, choice, lastchoice = -1;
- int_fast64_t lastsource = -1;
- uint_fast64_t nonzero = 0;
- double val;
- choices = 0;
- maxnode = 0;
- while (buf[0] != '\0') {
- /*
- * Read source state and choice.
- */
- source = checked_strtol(buf, &buf);
-
- // Read the name of the nondeterministic choice.
- choice = checked_strtol(buf, &buf);
-
- // Check if we encountered a state index that is bigger than all previously seen.
- if (source > maxnode) {
- maxnode = source;
+ NondeterministicSparseTransitionParser::Result NondeterministicSparseTransitionParser::parseNondeterministicTransitions(std::string const& filename) {
+
+ RewardMatrixInformationStruct nullInformation;
+
+ return NondeterministicSparseTransitionParser::parse(filename, false, nullInformation);
}
- if (isRewardFile) {
- // If we have switched the source state, we possibly need to insert the rows of the last
- // last source state.
- if (source != lastsource && lastsource != -1) {
- choices += lastchoice - ((*rewardMatrixInformation->nondeterministicChoiceIndices)[lastsource + 1] - (*rewardMatrixInformation->nondeterministicChoiceIndices)[lastsource] - 1);
- }
+ NondeterministicSparseTransitionParser::Result NondeterministicSparseTransitionParser::parseNondeterministicTransitionRewards(std::string const& filename, RewardMatrixInformationStruct const& rewardMatrixInformation) {
- // If we skipped some states, we need to reserve empty rows for all their nondeterministic
- // choices.
- for (int_fast64_t i = lastsource + 1; i < source; ++i) {
- choices += ((*rewardMatrixInformation->nondeterministicChoiceIndices)[i + 1] - (*rewardMatrixInformation->nondeterministicChoiceIndices)[i]);
- }
+ return NondeterministicSparseTransitionParser::parse(filename, true, rewardMatrixInformation);
+ }
- // If we advanced to the next state, but skipped some choices, we have to reserve rows
- // for them
- if (source != lastsource) {
- choices += choice + 1;
- } else if (choice != lastchoice) {
- choices += choice - lastchoice;
- }
- } else {
- // If we have skipped some states, we need to reserve the space for the self-loop insertion
- // in the second pass.
- if (source > lastsource + 1) {
- nonzero += source - lastsource - 1;
- choices += source - lastsource - 1;
- } else if (source != lastsource || choice != lastchoice) {
- // If we have switched the source state or the nondeterministic choice, we need to
- // reserve one row more.
- ++choices;
+ NondeterministicSparseTransitionParser::FirstPassResult NondeterministicSparseTransitionParser::firstPass(char* buf, SupportedLineEndingsEnum lineEndings, bool isRewardFile, RewardMatrixInformationStruct const& rewardMatrixInformation) {
+
+ // Check file header and extract number of transitions.
+
+ // Skip the format hint if it is there.
+ buf = trimWhitespaces(buf);
+ if(buf[0] < '0' || buf[0] > '9') {
+ buf = storm::parser::forwardToNextLine(buf, lineEndings);
}
- }
- // Read target and check if we encountered a state index that is bigger than all previously
- // seen.
- target = checked_strtol(buf, &buf);
- if (target > maxnode) {
- maxnode = target;
- }
+ // Read all transitions.
+ uint_fast64_t source = 0, target = 0, choice = 0, lastchoice = 0, lastsource = 0;
+ double val = 0.0;
+ NondeterministicSparseTransitionParser::FirstPassResult result;
- // Read value and check whether it's positive.
- val = checked_strtod(buf, &buf);
- if ((val < 0.0) || (val > 1.0)) {
- LOG4CPLUS_ERROR(logger, "Expected a positive probability but got \"" << std::string(buf, 0, 16) << "\".");
- return 0;
- }
+ // Since the first line is already a new choice but is not covered below, that has to be covered here.
+ result.choices = 1;
- lastchoice = choice;
- lastsource = source;
-
- /*
- * Increase number of non-zero values.
- */
- nonzero++;
-
- // The PRISM output format lists the name of the transition in the fourth column,
- // but omits the fourth column if it is an internal action. In either case, however, the third column
- // is followed by a space. We need to skip over that space first (instead of trimming whitespaces),
- // before we can skip to the line end, because trimming the white spaces will proceed to the next line
- // in case there is no action label in the fourth column.
- if (buf[0] == ' ') {
- ++buf;
- }
+ while (buf[0] != '\0') {
- /*
- * Proceed to beginning of next line.
- */
- switch (lineEndings) {
- case SupportedLineEndingsEnum::SlashN:
- buf += strcspn(buf, " \t\n");
- break;
- case SupportedLineEndingsEnum::SlashR:
- buf += strcspn(buf, " \t\r");
- break;
- case SupportedLineEndingsEnum::SlashRN:
- buf += strcspn(buf, " \t\r\n");
- break;
- default:
- case storm::parser::SupportedLineEndingsEnum::Unsupported:
- // This Line will never be reached as the Parser would have thrown already.
- throw;
- break;
- }
- buf = trimWhitespaces(buf);
- }
+ // Read source state and choice.
+ source = checked_strtol(buf, &buf);
- if (isRewardFile) {
- // If not all rows were filled for the last state, we need to insert them.
- choices += lastchoice - ((*rewardMatrixInformation->nondeterministicChoiceIndices)[lastsource + 1] - (*rewardMatrixInformation->nondeterministicChoiceIndices)[lastsource] - 1);
+ // Read the name of the nondeterministic choice.
+ choice = checked_strtol(buf, &buf);
- // If we skipped some states, we need to reserve empty rows for all their nondeterministic
- // choices.
- for (uint_fast64_t i = lastsource + 1; i < rewardMatrixInformation->nondeterministicChoiceIndices->size() - 1; ++i) {
- choices += ((*rewardMatrixInformation->nondeterministicChoiceIndices)[i + 1] - (*rewardMatrixInformation->nondeterministicChoiceIndices)[i]);
- }
- }
+ // Check if we encountered a state index that is bigger than all previously seen.
+ if (source > result.highestStateIndex) {
+ result.highestStateIndex = source;
+ }
- return nonzero;
-}
+ if (isRewardFile) {
+ // If we have switched the source state, we possibly need to insert rows for skipped choices of the last
+ // source state.
+ if (source != lastsource) {
+ // number of choices skipped = number of choices of last state - number of choices read
+ result.choices += ((*rewardMatrixInformation.nondeterministicChoiceIndices)[lastsource + 1] - (*rewardMatrixInformation.nondeterministicChoiceIndices)[lastsource]) - (lastchoice + 1);
+ }
+
+ // If we skipped some states, we need to reserve empty rows for all their nondeterministic
+ // choices.
+ for (uint_fast64_t i = lastsource + 1; i < source; ++i) {
+ result.choices += ((*rewardMatrixInformation.nondeterministicChoiceIndices)[i + 1] - (*rewardMatrixInformation.nondeterministicChoiceIndices)[i]);
+ }
+
+ // If we advanced to the next state, but skipped some choices, we have to reserve rows
+ // for them.
+ if (source != lastsource) {
+ result.choices += choice + 1;
+ } else if (choice != lastchoice) {
+ result.choices += choice - lastchoice;
+ }
+ } else {
+ // If we have skipped some states, we need to reserve the space for the self-loop insertion
+ // in the second pass.
+ if (source > lastsource + 1) {
+ result.numberOfNonzeroEntries += source - lastsource - 1;
+ result.choices += source - lastsource - 1;
+ } else if (source != lastsource || choice != lastchoice) {
+ // If we have switched the source state or the nondeterministic choice, we need to
+ // reserve one row more.
+ ++result.choices;
+ }
+ }
+ // Read target and check if we encountered a state index that is bigger than all previously
+ // seen.
+ target = checked_strtol(buf, &buf);
+ if (target > result.highestStateIndex) {
+ result.highestStateIndex = target;
+ }
-/*!
- * Reads a .tra file and produces a sparse matrix representing the described Markov Chain.
- *
- * Matrices created with this method have to be freed with the delete operator.
- * @param filename input .tra file's name.
- * @return a pointer to the created sparse matrix.
- */
+ // Read value and check whether it's positive.
+ val = checked_strtod(buf, &buf);
+ if ((val < 0.0) || (val > 1.0)) {
+ LOG4CPLUS_ERROR(logger, "Expected a positive probability but got \"" << std::string(buf, 0, 16) << "\".");
+ NondeterministicSparseTransitionParser::FirstPassResult nullResult;
+ return nullResult;
+ }
-NondeterministicSparseTransitionParserResult_t NondeterministicSparseTransitionParser(std::string const &filename, RewardMatrixInformationStruct* rewardMatrixInformation) {
- /*
- * Enforce locale where decimal point is '.'.
- */
- setlocale(LC_NUMERIC, "C");
-
- if (!fileExistsAndIsReadable(filename.c_str())) {
- LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": File does not exist or is not readable.");
- throw storm::exceptions::WrongFormatException();
- }
-
- bool isRewardFile = rewardMatrixInformation != nullptr;
-
- /*
- * Find out about the used line endings.
- */
- SupportedLineEndingsEnum lineEndings = findUsedLineEndings(filename, true);
-
- /*
- * Open file.
- */
- MappedFile file(filename.c_str());
- char* buf = file.data;
-
- /*
- * Perform first pass, i.e. obtain number of columns, rows and non-zero elements.
- */
- int_fast64_t maxnode;
- uint_fast64_t choices;
- uint_fast64_t nonzero = firstPass(file.data, lineEndings, choices, maxnode, rewardMatrixInformation);
-
- /*
- * If first pass returned zero, the file format was wrong.
- */
- if (nonzero == 0) {
- LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": erroneous file format.");
- throw storm::exceptions::WrongFormatException();
- }
-
- /*
- * Perform second pass.
- *
- * From here on, we already know that the file header is correct.
- */
-
- /*
- * Skip file header.
- */
- if (!isRewardFile) {
- // skip format hint
- buf = storm::parser::forwardToNextLine(buf, lineEndings);
- }
-
- if (isRewardFile) {
- if (choices > rewardMatrixInformation->rowCount || (uint_fast64_t)(maxnode + 1) > rewardMatrixInformation->columnCount) {
- LOG4CPLUS_ERROR(logger, "Reward matrix size exceeds transition matrix size.");
- throw storm::exceptions::WrongFormatException() << "Reward matrix size exceeds transition matrix size.";
- } else if (choices != rewardMatrixInformation->rowCount) {
- LOG4CPLUS_ERROR(logger, "Reward matrix row count does not match transition matrix row count.");
- throw storm::exceptions::WrongFormatException() << "Reward matrix row count does not match transition matrix row count.";
- } else {
- maxnode = rewardMatrixInformation->columnCount - 1;
- }
- }
-
- /*
- * Create and initialize matrix.
- * The matrix should have as many columns as we have nodes and as many rows as we have choices.
- * Those two values, as well as the number of nonzero elements, was been calculated in the first run.
- */
- LOG4CPLUS_INFO(logger, "Attempting to create matrix of size " << choices << " x " << (maxnode+1) << " with " << nonzero << " entries.");
- storm::storage::SparseMatrixBuilder<double> matrixBuilder(choices, maxnode + 1, nonzero);
-
- /*
- * Create row mapping.
- */
- std::vector<uint_fast64_t> rowMapping(maxnode + 2, 0);
-
- /*
- * Parse file content.
- */
- int_fast64_t source, target, lastsource = -1, choice, lastchoice = -1;
- uint_fast64_t curRow = -1;
- double val;
- bool fixDeadlocks = storm::settings::Settings::getInstance()->isSet("fixDeadlocks");
- bool hadDeadlocks = false;
-
- /*
- * Read all transitions from file.
- */
- while (buf[0] != '\0') {
- /*
- * Read source state and choice.
- */
- source = checked_strtol(buf, &buf);
- choice = checked_strtol(buf, &buf);
-
- if (isRewardFile) {
- // If we have switched the source state, we possibly need to insert the rows of the last
- // last source state.
- if (source != lastsource && lastsource != -1) {
- curRow += lastchoice - ((*rewardMatrixInformation->nondeterministicChoiceIndices)[lastsource + 1] - (*rewardMatrixInformation->nondeterministicChoiceIndices)[lastsource] - 1);
+ lastchoice = choice;
+ lastsource = source;
+
+ // Increase number of non-zero values.
+ result.numberOfNonzeroEntries++;
+
+ // The PRISM output format lists the name of the transition in the fourth column,
+ // but omits the fourth column if it is an internal action. In either case we can skip to the end of the line.
+ buf = forwardToLineEnd(buf, lineEndings);
+
+ buf = trimWhitespaces(buf);
}
- // If we skipped some states, we need to reserve empty rows for all their nondeterministic
- // choices.
- for (int_fast64_t i = lastsource + 1; i < source; ++i) {
- curRow += ((*rewardMatrixInformation->nondeterministicChoiceIndices)[i + 1] - (*rewardMatrixInformation->nondeterministicChoiceIndices)[i]);
+ if (isRewardFile) {
+ // If not all rows were filled for the last state, we need to insert them.
+ result.choices += ((*rewardMatrixInformation.nondeterministicChoiceIndices)[lastsource + 1] - (*rewardMatrixInformation.nondeterministicChoiceIndices)[lastsource] ) - (lastchoice + 1);
+
+ // If we skipped some states, we need to reserve empty rows for all their nondeterministic
+ // choices.
+ for (uint_fast64_t i = lastsource + 1; i < rewardMatrixInformation.nondeterministicChoiceIndices->size() - 1; ++i) {
+ result.choices += ((*rewardMatrixInformation.nondeterministicChoiceIndices)[i + 1] - (*rewardMatrixInformation.nondeterministicChoiceIndices)[i]);
+ }
}
- // If we advanced to the next state, but skipped some choices, we have to reserve rows
- // for them
- if (source != lastsource) {
- curRow += choice + 1;
- } else if (choice != lastchoice) {
- curRow += choice - lastchoice;
+ return result;
+ }
+
+ NondeterministicSparseTransitionParser::Result NondeterministicSparseTransitionParser::parse(std::string const &filename, bool isRewardFile, RewardMatrixInformationStruct const& rewardMatrixInformation) {
+
+ // Enforce locale where decimal point is '.'.
+ setlocale(LC_NUMERIC, "C");
+
+ if (!fileExistsAndIsReadable(filename.c_str())) {
+ LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": File does not exist or is not readable.");
+ throw storm::exceptions::WrongFormatException();
}
- } else {
- // Increase line count if we have either finished reading the transitions of a certain state
- // or we have finished reading one nondeterministic choice of a state.
- if ((source != lastsource || choice != lastchoice)) {
- ++curRow;
+
+ // Find out about the used line endings.
+ SupportedLineEndingsEnum lineEndings = findUsedLineEndings(filename, true);
+
+ // Open file.
+ MappedFile file(filename.c_str());
+ char* buf = file.data;
+
+ // Perform first pass, i.e. obtain number of columns, rows and non-zero elements.
+ NondeterministicSparseTransitionParser::FirstPassResult firstPass = NondeterministicSparseTransitionParser::firstPass(file.data, lineEndings, isRewardFile, rewardMatrixInformation);
+
+ // If first pass returned zero, the file format was wrong.
+ if (firstPass.numberOfNonzeroEntries == 0) {
+ LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": erroneous file format.");
+ throw storm::exceptions::WrongFormatException();
}
- /*
- * Check if we have skipped any source node, i.e. if any node has no
- * outgoing transitions. If so, insert a self-loop.
- * Also add self-loops to rowMapping.
- */
- for (int_fast64_t node = lastsource + 1; node < source; node++) {
- hadDeadlocks = true;
- if (fixDeadlocks) {
- rowMapping.at(node) = curRow;
- matrixBuilder.addNextValue(curRow, node, 1);
- ++curRow;
- LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": node " << node << " has no outgoing transitions. A self-loop was inserted.");
+
+ // Perform second pass.
+
+ // Skip the format hint if it is there.
+ buf = trimWhitespaces(buf);
+ if(buf[0] < '0' || buf[0] > '9') {
+ buf = storm::parser::forwardToNextLine(buf, lineEndings);
+ }
+
+ if (isRewardFile) {
+ // The reward matrix should match the size of the transition matrix.
+ if (firstPass.choices > rewardMatrixInformation.rowCount || (uint_fast64_t)(firstPass.highestStateIndex + 1) > rewardMatrixInformation.columnCount) {
+ LOG4CPLUS_ERROR(logger, "Reward matrix size exceeds transition matrix size.");
+ throw storm::exceptions::WrongFormatException() << "Reward matrix size exceeds transition matrix size.";
+ } else if (firstPass.choices != rewardMatrixInformation.rowCount) {
+ LOG4CPLUS_ERROR(logger, "Reward matrix row count does not match transition matrix row count.");
+ throw storm::exceptions::WrongFormatException() << "Reward matrix row count does not match transition matrix row count.";
} else {
- LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": node " << node << " has no outgoing transitions.");
+ firstPass.highestStateIndex = rewardMatrixInformation.columnCount - 1;
}
}
- if (source != lastsource) {
- /*
- * Add this source to rowMapping, if this is the first choice we encounter for this state.
- */
- rowMapping.at(source) = curRow;
- }
- }
- // Read target and value and write it to the matrix.
- target = checked_strtol(buf, &buf);
- val = checked_strtod(buf, &buf);
- matrixBuilder.addNextValue(curRow, target, val);
- lastsource = source;
- lastchoice = choice;
+ // Create the matrix builder.
+ // The matrix to be build should have as many columns as we have nodes and as many rows as we have choices.
+ // Those two values, as well as the number of nonzero elements, was been calculated in the first run.
+ LOG4CPLUS_INFO(logger, "Attempting to create matrix of size " << firstPass.choices << " x " << (firstPass.highestStateIndex+1) << " with " << firstPass.numberOfNonzeroEntries << " entries.");
+ storm::storage::SparseMatrixBuilder<double> matrixBuilder(firstPass.choices, firstPass.highestStateIndex + 1, firstPass.numberOfNonzeroEntries);
+
+ // Create row mapping.
+ std::vector<uint_fast64_t> rowMapping(firstPass.highestStateIndex + 2, 0);
+
+ // Initialize variables for the parsing run.
+ uint_fast64_t source = 0, target = 0, lastsource = 0, choice = 0, lastchoice = 0, curRow = 0;
+ double val = 0.0;
+ bool fixDeadlocks = storm::settings::Settings::getInstance()->isSet("fixDeadlocks");
+ bool hadDeadlocks = false;
+
+ // Read all transitions from file.
+ while (buf[0] != '\0') {
+
+ // Read source state and choice.
+ source = checked_strtol(buf, &buf);
+ choice = checked_strtol(buf, &buf);
+
+ if (isRewardFile) {
+ // If we have switched the source state, we possibly need to insert the rows of the last
+ // source state.
+ if (source != lastsource) {
+ curRow += ((*rewardMatrixInformation.nondeterministicChoiceIndices)[lastsource + 1] - (*rewardMatrixInformation.nondeterministicChoiceIndices)[lastsource]) -(lastchoice + 1);
+ }
+
+ // If we skipped some states, we need to reserve empty rows for all their nondeterministic
+ // choices.
+ for (uint_fast64_t i = lastsource + 1; i < source; ++i) {
+ curRow += ((*rewardMatrixInformation.nondeterministicChoiceIndices)[i + 1] - (*rewardMatrixInformation.nondeterministicChoiceIndices)[i]);
+ }
+
+ // If we advanced to the next state, but skipped some choices, we have to reserve rows
+ // for them
+ if (source != lastsource) {
+ curRow += choice + 1;
+ } else if (choice != lastchoice) {
+ curRow += choice - lastchoice;
+ }
+ } else {
+ // Increase line count if we have either finished reading the transitions of a certain state
+ // or we have finished reading one nondeterministic choice of a state.
+ if ((source != lastsource || choice != lastchoice)) {
+ ++curRow;
+ }
+ // Check if we have skipped any source node, i.e. if any node has no
+ // outgoing transitions. If so, insert a self-loop.
+ // Also add self-loops to rowMapping.
+ for (uint_fast64_t node = lastsource + 1; node < source; node++) {
+ hadDeadlocks = true;
+ if (fixDeadlocks) {
+ rowMapping.at(node) = curRow;
+ matrixBuilder.addNextValue(curRow, node, 1);
+ ++curRow;
+ LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": node " << node << " has no outgoing transitions. A self-loop was inserted.");
+ } else {
+ LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": node " << node << " has no outgoing transitions.");
+ }
+ }
+ if (source != lastsource) {
+ // Add this source to rowMapping, if this is the first choice we encounter for this state.
+ rowMapping.at(source) = curRow;
+ }
+ }
- /*
- * Proceed to beginning of next line in file and next row in matrix.
- */
- if (buf[0] == ' ') {
- ++buf;
- }
- switch (lineEndings) {
- case SupportedLineEndingsEnum::SlashN:
- buf += strcspn(buf, " \t\n");
- break;
- case SupportedLineEndingsEnum::SlashR:
- buf += strcspn(buf, " \t\r");
- break;
- case SupportedLineEndingsEnum::SlashRN:
- buf += strcspn(buf, " \t\r\n");
- break;
- default:
- case storm::parser::SupportedLineEndingsEnum::Unsupported:
- // This Line will never be reached as the Parser would have thrown already.
- throw;
- break;
- }
- buf = trimWhitespaces(buf);
- }
+ // Read target and value and write it to the matrix.
+ target = checked_strtol(buf, &buf);
+ val = checked_strtod(buf, &buf);
+ matrixBuilder.addNextValue(curRow, target, val);
+
+ lastsource = source;
+ lastchoice = choice;
- for (int_fast64_t node = lastsource + 1; node <= maxnode + 1; node++) {
- rowMapping.at(node) = curRow + 1;
- }
+ // Proceed to beginning of next line in file and next row in matrix.
+ buf = forwardToLineEnd(buf, lineEndings);
- if (!fixDeadlocks && hadDeadlocks && !isRewardFile) throw storm::exceptions::WrongFormatException() << "Some of the nodes had deadlocks. You can use --fixDeadlocks to insert self-loops on the fly.";
+ buf = trimWhitespaces(buf);
+ }
- return std::make_pair(matrixBuilder.build(), std::move(rowMapping));
-}
+ for (uint_fast64_t node = lastsource + 1; node <= firstPass.highestStateIndex + 1; node++) {
+ rowMapping.at(node) = curRow + 1;
+ }
+
+ if (!fixDeadlocks && hadDeadlocks && !isRewardFile) throw storm::exceptions::WrongFormatException() << "Some of the nodes had deadlocks. You can use --fixDeadlocks to insert self-loops on the fly.";
+
+ return NondeterministicSparseTransitionParser::Result(matrixBuilder.build(), rowMapping);
+ }
-} // namespace parser
+ } // namespace parser
} // namespace storm
diff --git a/src/parser/NondeterministicSparseTransitionParser.h b/src/parser/NondeterministicSparseTransitionParser.h
index 900bc088e..34fc3f397 100644
--- a/src/parser/NondeterministicSparseTransitionParser.h
+++ b/src/parser/NondeterministicSparseTransitionParser.h
@@ -1,30 +1,101 @@
-#ifndef STORM_PARSER_NONDETTRAPARSER_H_
-#define STORM_PARSER_NONDETTRAPARSER_H_
-
-#include "src/storage/SparseMatrix.h"
+#ifndef STORM_PARSER_NONDETERMINISTICSPARSETRANSITIONPARSER_H_
+#define STORM_PARSER_NONDETERMINISTICSPARSETRANSITIONPARSER_H_
#include "src/parser/Parser.h"
-#include "src/utility/OsDetection.h"
+#include "src/storage/SparseMatrix.h"
-#include <utility>
-#include <memory>
#include <vector>
namespace storm {
-namespace parser {
+ namespace parser {
+
+ class NondeterministicSparseTransitionParser {
+
+ public:
+
+ /*
+ * A structure representing the result of the first pass of this parser.
+ * It contains the number of non-zero entries in the model, the highest state index and the total number if nondeterministic choices.
+ */
+ struct FirstPassResult {
+
+ FirstPassResult() : numberOfNonzeroEntries(0), highestStateIndex(0), choices(0) {
+ // Intentionally left empty.
+ }
+
+ // The total number of non-zero entries of the model.
+ uint_fast64_t numberOfNonzeroEntries;
+
+ // The highest state index that appears in the model.
+ uint_fast64_t highestStateIndex;
+
+ // The total number of nondeterministic choices within the transition system.
+ uint_fast64_t choices;
+ };
+
+ /*!
+ * A structure representing the result of the parser.
+ * It contains the resulting matrix as well as the row mapping.
+ */
+ struct Result {
+
+ Result(storm::storage::SparseMatrix<double> transitionMatrix, std::vector<uint_fast64_t> rowMapping) : transitionMatrix(transitionMatrix), rowMapping(rowMapping) {
+ // Intentionally left empty.
+ }
+
+ // The matrix containing the parsed transition system.
+ storm::storage::SparseMatrix<double> transitionMatrix;
+
+ // A mapping from rows of the matrix to states of the model.
+ // This resolves the nondeterministic choices inside the transition system.
+ std::vector<uint_fast64_t> rowMapping;
+ };
+
+ /*!
+ * @brief Load a nondeterministic transition system from file and create a
+ * sparse adjacency matrix whose entries represent the weights of the edges
+ */
+ static Result parseNondeterministicTransitions(std::string const &filename);
+
+ /*!
+ * @brief Load a nondeterministic transition system from file and create a
+ * sparse adjacency matrix whose entries represent the weights of the edges
+ */
+ static Result parseNondeterministicTransitionRewards(std::string const &filename, RewardMatrixInformationStruct const& rewardMatrixInformation);
+
+ private:
+
+ /*!
+ * This method does the first pass through the buffer containing the content of some transition file.
+ *
+ * It computes the overall number of nondeterministic choices, i.e. the
+ * number of rows in the matrix that should be created.
+ * It also calculates the overall number of non-zero cells, i.e. the number
+ * of elements the matrix has to hold, and the maximum node id, i.e. the
+ * number of columns of the matrix.
+ *
+ * @param buffer Buffer containing the data to scan. This is expected to be some char array.
+ * @param lineEndings The line endings that are to be used while parsing.
+ * @param insertDiagonalEntriesIfMissing A flag set iff entries on the primary diagonal of the matrix should be added in case they are missing in the parsed file.
+ * @return A structure representing the result of the first pass.
+ */
+ static FirstPassResult firstPass(char* buffer, SupportedLineEndingsEnum lineEndings, bool isRewardFile, RewardMatrixInformationStruct const& rewardMatrixInformation);
+
+ /*!
+ * The main parsing routine.
+ * Opens the given file, calls the first pass and performs the second pass, parsing the content of the file into a SparseMatrix.
+ *
+ * @param filename The path of file to be parsed.
+ * @param rewardFile A flag set iff the file to be parsed contains transition rewards.
+ * @param insertDiagonalEntriesIfMissing A flag set iff entries on the primary diagonal of the matrix should be added in case they are missing in the parsed file.
+ * @param rewardMatrixInformation A struct containing information that is used to check if the transition reward matrix fits to the rest of the model.
+ * @return A SparseMatrix containing the parsed file contents.
+ */
+ static Result parse(std::string const& filename, bool isRewardFile, RewardMatrixInformationStruct const& rewardMatrixInformation);
+
+ };
-/*!
- * @brief Contains the Result of a call to the NondeterministicSparseTransitionParser function. The first part is the resulting matrix. The second part is the row mapping.
- */
-typedef std::pair<storm::storage::SparseMatrix<double>, std::vector<uint_fast64_t>> NondeterministicSparseTransitionParserResult_t;
-
-/*!
- * @brief Load a nondeterministic transition system from file and create a
- * sparse adjacency matrix whose entries represent the weights of the edges
- */
-NondeterministicSparseTransitionParserResult_t NondeterministicSparseTransitionParser(std::string const &filename, RewardMatrixInformationStruct* rewardMatrixInformation = nullptr);
-
-} // namespace parser
+ } // namespace parser
} // namespace storm
-#endif /* STORM_PARSER_NONDETTRAPARSER_H_ */
+#endif /* STORM_PARSER_NONDETERMINISTICSPARSETRANSITIONPARSER_H__H_ */
diff --git a/src/parser/Parser.cpp b/src/parser/Parser.cpp
index 6fb26ef4b..b1b0c6e79 100644
--- a/src/parser/Parser.cpp
+++ b/src/parser/Parser.cpp
@@ -117,6 +117,29 @@ SupportedLineEndingsEnum findUsedLineEndings(std::string const& fileName, bool t
return SupportedLineEndingsEnum::Unsupported;
}
+/*!
+ * @brief Encapsulates the usage of function @strcspn to forward to the end of the line (next char is the newline character).
+ */
+char* forwardToLineEnd(char* buffer, SupportedLineEndingsEnum lineEndings) {
+ switch (lineEndings) {
+ case SupportedLineEndingsEnum::SlashN:
+ return buffer + strcspn(buffer, "\n\0");
+ break;
+ case SupportedLineEndingsEnum::SlashR:
+ return buffer + strcspn(buffer, "\r\0");
+ break;
+ case SupportedLineEndingsEnum::SlashRN:
+ return buffer + strcspn(buffer, "\r\0");
+ break;
+ default:
+ case SupportedLineEndingsEnum::Unsupported:
+ // This Line will never be reached as the Parser would have thrown already.
+ throw;
+ break;
+ }
+ return nullptr;
+}
+
/*!
* @brief Encapsulates the usage of function @strchr to forward to the next line
*/
diff --git a/src/parser/Parser.h b/src/parser/Parser.h
index e7fcf4dab..b2cfb0677 100644
--- a/src/parser/Parser.h
+++ b/src/parser/Parser.h
@@ -146,6 +146,11 @@ enum class SupportedLineEndingsEnum : unsigned short {
*/
storm::parser::SupportedLineEndingsEnum findUsedLineEndings(std::string const& fileName, bool throwOnUnsupported = false);
+/*!
+ * @brief Encapsulates the usage of function @strcspn to forward to the end of the line (next char is the newline character).
+ */
+char* forwardToLineEnd(char* buffer, storm::parser::SupportedLineEndingsEnum lineEndings);
+
/*!
* @brief Encapsulates the usage of function @strchr to forward to the next line
*/