Browse Source

First part of the refactoring of Parser.h/.cpp

- Removed the RewardMatrixInformationStruct since it was only used as function argument.
|- Replaced its function by the respective results of the transition parser (for det/non-det)
- Moved the MappedFile class to separate file.
- Renamed the SupportedFileEndingsEnum enum to SupportedFileEndings.
- Whats left in Parser.*:
|- A bunch of free functions for manipulation of c-style strings, a function to read the model hint and the SupportedFileEndings enum with its recognition function.

Im not exactly sure what to do with this.
- I think the name Parser.* implies a parser base class, while it is not. Therefore: Renaming.
- The c-style string manipulation functions might also needed elsewhere. Therefore: Moving them into the utility folder/namespace.
- The model hint function would fit in the AutoParser, except for its signature (low level arguments vs. high level arguments of the AutoParser). Therefore: Either moving it to the Auto Parser or leave it as helper function with the others (c-style string handling and low level OS detection)
- The SupportedLineEndings and its assorted functions either belong to the string manipulation functions or to the MappedFile class. Therefor: Moving them accordingly.
- Once all things have moved the Parser.* will be empty. Therefore: Deletion.

Next up: Trying to decide what to do with the rest of the Parser.* and doing it.


Former-commit-id: aa7417e5e1
main
masawei 11 years ago
parent
commit
538f911283
  1. 5
      src/parser/AtomicPropositionLabelingParser.cpp
  2. 7
      src/parser/AutoParser.cpp
  3. 64
      src/parser/AutoParser.h
  4. 19
      src/parser/DeterministicModelParser.cpp
  5. 360
      src/parser/DeterministicSparseTransitionParser.cpp
  6. 14
      src/parser/DeterministicSparseTransitionParser.h
  7. 101
      src/parser/MappedFile.cpp
  8. 95
      src/parser/MappedFile.h
  9. 7
      src/parser/MarkovAutomatonSparseTransitionParser.cpp
  10. 4
      src/parser/MarkovAutomatonSparseTransitionParser.h
  11. 27
      src/parser/NondeterministicModelParser.cpp
  12. 241
      src/parser/NondeterministicSparseTransitionParser.cpp
  13. 26
      src/parser/NondeterministicSparseTransitionParser.h
  14. 132
      src/parser/Parser.cpp
  15. 199
      src/parser/Parser.h
  16. 1
      src/parser/SparseStateRewardParser.cpp

5
src/parser/AtomicPropositionLabelingParser.cpp

@ -6,12 +6,13 @@
*/ */
#include "src/parser/AtomicPropositionLabelingParser.h" #include "src/parser/AtomicPropositionLabelingParser.h"
#include "src/parser/Parser.h"
#include <cstring> #include <cstring>
#include <string> #include <string>
#include <iostream> #include <iostream>
#include "src/parser/Parser.h"
#include "src/parser/MappedFile.h"
#include "src/exceptions/WrongFormatException.h" #include "src/exceptions/WrongFormatException.h"
#include "src/exceptions/FileIoException.h" #include "src/exceptions/FileIoException.h"
@ -31,7 +32,7 @@ namespace storm {
} }
// Find out about the used line endings. // Find out about the used line endings.
SupportedLineEndingsEnum lineEndings = findUsedLineEndings(filename, true); SupportedLineEndings lineEndings = findUsedLineEndings(filename, true);
MappedFile file(filename.c_str()); MappedFile file(filename.c_str());
char* buf = file.data; char* buf = file.data;

7
src/parser/AutoParser.cpp

@ -8,6 +8,7 @@
#include "src/parser/AutoParser.h" #include "src/parser/AutoParser.h"
#include "src/parser/Parser.h" #include "src/parser/Parser.h"
#include "src/parser/MappedFile.h"
#include "src/parser/DeterministicModelParser.h" #include "src/parser/DeterministicModelParser.h"
#include "src/parser/NondeterministicModelParser.h" #include "src/parser/NondeterministicModelParser.h"
@ -68,7 +69,7 @@ namespace storm {
storm::models::ModelType hintType = storm::models::Unknown; storm::models::ModelType hintType = storm::models::Unknown;
// Find out the line endings used within the file. // Find out the line endings used within the file.
storm::parser::SupportedLineEndingsEnum lineEndings = storm::parser::findUsedLineEndings(filename); storm::parser::SupportedLineEndings lineEndings = storm::parser::findUsedLineEndings(filename);
// Open the file. // Open the file.
MappedFile file(filename.c_str()); MappedFile file(filename.c_str());
@ -90,5 +91,5 @@ namespace storm {
return hintType; return hintType;
} }
} } // namespace parser
} } // namespace storm

64
src/parser/AutoParser.h

@ -9,38 +9,38 @@ namespace storm {
namespace parser { namespace parser {
class AutoParser { class AutoParser {
public: public:
/*!
/*! * Checks the given files and parses the model within these files.
* Checks the given files and parses the model within these files. *
* * This parser analyzes the format hint in the first line of the transition
* This parser analyzes the format hint in the first line of the transition * file. If this is a valid format, it will use the parser for this format,
* file. If this is a valid format, it will use the parser for this format, * otherwise it will throw an exception.
* otherwise it will throw an exception. *
* * When the files are parsed successfully, a shared pointer owning the resulting model is returned.
* When the files are parsed successfully, a shared pointer owning the resulting model is returned. * The concrete model can be obtained using the as<Type>() member of the AbstractModel class.
* The concrete model can be obtained using the as<Type>() member of the AbstractModel class. *
* * @param transitionsFilename The name of the file containing the transitions of the Markov automaton.
* @param transitionsFilename The name of the file containing the transitions of the Markov automaton. * @param labelingFilename The name of the file containing the labels for the states of the Markov automaton.
* @param labelingFilename The name of the file containing the labels for the states of the Markov automaton. * @param stateRewardFilename The name of the file that contains the state reward of the Markov automaton.
* @param stateRewardFilename The name of the file that contains the state reward of the Markov automaton. * @param transitionRewardFilename The name of the file that contains the transition rewards of the Markov automaton.
* @param transitionRewardFilename The name of the file that contains the transition rewards of the Markov automaton. * @return A shared_ptr containing the resulting model.
* @return A shared_ptr containing the resulting model. */
*/ static std::shared_ptr<storm::models::AbstractModel<double>> parseModel(std::string const & transitionSystemFile,
static std::shared_ptr<storm::models::AbstractModel<double>> parseModel(std::string const & transitionSystemFile, std::string const & labelingFile,
std::string const & labelingFile, std::string const & stateRewardFile = "",
std::string const & stateRewardFile = "", std::string const & transitionRewardFile = "");
std::string const & transitionRewardFile = ""); private:
/*!
private: * Opens the given file and parses the file format hint.
*
/*! * @param filename The path and name of the file that is to be analysed.
* Opens the given file and parses the file format hint. * @return The type of the model as an enum value.
* */
* @param filename The path and name of the file that is to be analysed. static storm::models::ModelType analyzeHint(const std::string& filename);
* @return The type of the model as an enum value.
*/
static storm::models::ModelType analyzeHint(const std::string& filename);
}; };
} // namespace parser } // namespace parser

19
src/parser/DeterministicModelParser.cpp

@ -28,24 +28,25 @@ namespace parser {
*/ */
DeterministicModelParser::Result DeterministicModelParser::parseDeterministicModel(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile, std::string const & transitionRewardFile) { DeterministicModelParser::Result DeterministicModelParser::parseDeterministicModel(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile, std::string const & transitionRewardFile) {
storm::storage::SparseMatrix<double> resultTransitionSystem(std::move(storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(transitionSystemFile))); // Parse the transitions.
storm::storage::SparseMatrix<double> transitions(std::move(storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(transitionSystemFile)));
uint_fast64_t stateCount = resultTransitionSystem.getColumnCount(); uint_fast64_t stateCount = transitions.getColumnCount();
uint_fast64_t rowCount = resultTransitionSystem.getRowCount();
// Parse the state labeling.
storm::models::AtomicPropositionsLabeling labeling(std::move(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(stateCount, labelingFile))); storm::models::AtomicPropositionsLabeling labeling(std::move(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(stateCount, labelingFile)));
DeterministicModelParser::Result result(std::move(resultTransitionSystem), std::move(labeling)); // Construct the result.
DeterministicModelParser::Result result(std::move(transitions), std::move(labeling));
// Only parse state rewards of a file is given. // Only parse state rewards if a file is given.
if (stateRewardFile != "") { if (stateRewardFile != "") {
result.stateRewards.reset(storm::parser::SparseStateRewardParser::parseSparseStateReward(stateCount, stateRewardFile)); result.stateRewards = storm::parser::SparseStateRewardParser::parseSparseStateReward(stateCount, stateRewardFile);
} }
// Only parse transition rewards of a file is given. // Only parse transition rewards if a file is given.
if (transitionRewardFile != "") { if (transitionRewardFile != "") {
RewardMatrixInformationStruct rewardMatrixInfo(rowCount, stateCount, nullptr); result.transitionRewards = storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitionRewards(transitionRewardFile, result.transitionSystem);
result.transitionRewards.reset(std::move(storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitionRewards(transitionRewardFile, rewardMatrixInfo)));
} }
return result; return result;

360
src/parser/DeterministicSparseTransitionParser.cpp

@ -15,7 +15,7 @@
#include <string> #include <string>
#include "src/utility/constants.h" #include "src/utility/constants.h"
#include "src/parser/MappedFile.h"
#include "src/exceptions/FileIoException.h" #include "src/exceptions/FileIoException.h"
#include "src/exceptions/WrongFormatException.h" #include "src/exceptions/WrongFormatException.h"
#include "src/settings/Settings.h" #include "src/settings/Settings.h"
@ -25,241 +25,239 @@
extern log4cplus::Logger logger; extern log4cplus::Logger logger;
namespace storm { namespace storm {
namespace parser {
namespace parser { storm::storage::SparseMatrix<double> DeterministicSparseTransitionParser::parseDeterministicTransitions(std::string const& filename) {
storm::storage::SparseMatrix<double> DeterministicSparseTransitionParser::parseDeterministicTransitions(std::string const& filename, bool insertDiagonalEntriesIfMissing) { storm::storage::SparseMatrix<double> emptyMatrix;
RewardMatrixInformationStruct nullInformation; return DeterministicSparseTransitionParser::parse(filename, false, emptyMatrix);
}
return DeterministicSparseTransitionParser::parse(filename, false, nullInformation, insertDiagonalEntriesIfMissing); storm::storage::SparseMatrix<double> DeterministicSparseTransitionParser::parseDeterministicTransitionRewards(std::string const& filename, storm::storage::SparseMatrix<double> const & transitionMatrix) {
}
storm::storage::SparseMatrix<double> DeterministicSparseTransitionParser::parseDeterministicTransitionRewards(std::string const& filename, RewardMatrixInformationStruct const& rewardMatrixInformation) { return DeterministicSparseTransitionParser::parse(filename, true, transitionMatrix);
}
return DeterministicSparseTransitionParser::parse(filename, true, rewardMatrixInformation); storm::storage::SparseMatrix<double> DeterministicSparseTransitionParser::parse(std::string const& filename, bool isRewardFile, storm::storage::SparseMatrix<double> const & transitionMatrix) {
} // Enforce locale where decimal point is '.'.
setlocale(LC_NUMERIC, "C");
DeterministicSparseTransitionParser::FirstPassResult DeterministicSparseTransitionParser::firstPass(char* buf, SupportedLineEndingsEnum lineEndings, bool insertDiagonalEntriesIfMissing) { if (!fileExistsAndIsReadable(filename.c_str())) {
LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": File does not exist or is not readable.");
throw storm::exceptions::FileIoException() << "The supplied Transition input file \"" << filename << "\" does not exist or is not readable by this process.";
}
DeterministicSparseTransitionParser::FirstPassResult result; // Find out about the used line endings.
SupportedLineEndings lineEndings = findUsedLineEndings(filename, true);
// Skip the format hint if it is there. // Open file.
buf = trimWhitespaces(buf); MappedFile file(filename.c_str());
if(buf[0] < '0' || buf[0] > '9') { char* buf = file.data;
buf = storm::parser::forwardToNextLine(buf, lineEndings);
}
// Check all transitions for non-zero diagonal entries and deadlock states. // Perform first pass, i.e. count entries that are not zero.
uint_fast64_t row, col, lastRow = 0; bool insertDiagonalEntriesIfMissing = !isRewardFile;
bool rowHadDiagonalEntry = false; DeterministicSparseTransitionParser::FirstPassResult firstPass = DeterministicSparseTransitionParser::firstPass(file.data, lineEndings, insertDiagonalEntriesIfMissing);
while (buf[0] != '\0') {
// Read the transition. LOG4CPLUS_INFO(logger, "First pass on " << filename << " shows " << firstPass.numberOfNonzeroEntries << " NonZeros.");
row = checked_strtol(buf, &buf);
col = checked_strtol(buf, &buf);
// The actual read value is not needed here.
checked_strtod(buf, &buf);
// Compensate for missing diagonal entries if desired. // If first pass returned zero, the file format was wrong.
if (insertDiagonalEntriesIfMissing) { if (firstPass.numberOfNonzeroEntries == 0) {
if (lastRow != row) { LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": empty or erroneous file format.");
if(!rowHadDiagonalEntry) { throw storm::exceptions::WrongFormatException();
++result.numberOfNonzeroEntries;
} }
// Compensate for missing rows. // Perform second pass.
for (uint_fast64_t skippedRow = lastRow + 1; skippedRow < row; ++skippedRow) { // Skip the format hint if it is there.
++result.numberOfNonzeroEntries; buf = trimWhitespaces(buf);
if(buf[0] < '0' || buf[0] > '9') {
buf = storm::parser::forwardToNextLine(buf, lineEndings);
} }
lastRow = row;
rowHadDiagonalEntry = false;
}
if (col == row) { if(isRewardFile) {
rowHadDiagonalEntry = true; // The reward matrix should match the size of the transition matrix.
} if (firstPass.highestStateIndex + 1 > transitionMatrix.getRowCount() || firstPass.highestStateIndex + 1 > transitionMatrix.getColumnCount()) {
LOG4CPLUS_ERROR(logger, "Reward matrix has more rows or columns than transition matrix.");
throw storm::exceptions::WrongFormatException() << "Reward matrix has more rows or columns than transition matrix.";
} else {
// If we found the right number of states or less, we set it to the number of states represented by the transition matrix.
firstPass.highestStateIndex = transitionMatrix.getRowCount() - 1;
}
}
if (col > row && !rowHadDiagonalEntry) { // Creating matrix builder here.
rowHadDiagonalEntry = true; // The actual matrix will be build once all contents are inserted.
++result.numberOfNonzeroEntries; storm::storage::SparseMatrixBuilder<double> resultMatrix(firstPass.highestStateIndex + 1, firstPass.highestStateIndex + 1, firstPass.numberOfNonzeroEntries);
}
}
// Check if a higher state id was found. uint_fast64_t row, col, lastRow = 0;
if (row > result.highestStateIndex) result.highestStateIndex = row; double val;
if (col > result.highestStateIndex) result.highestStateIndex = col; bool fixDeadlocks = storm::settings::Settings::getInstance()->isSet("fixDeadlocks");
bool hadDeadlocks = false;
bool rowHadDiagonalEntry = false;
++result.numberOfNonzeroEntries;
buf = trimWhitespaces(buf);
}
if(insertDiagonalEntriesIfMissing) { // Read all transitions from file. Note that we assume that the
if (!rowHadDiagonalEntry) { // transitions are listed in canonical order, otherwise this will not
++result.numberOfNonzeroEntries; // work, i.e. the values in the matrix will be at wrong places.
}
//Compensate for missing rows at the end of the file. // Different parsing routines for transition systems and transition rewards.
for (uint_fast64_t skippedRow = (uint_fast64_t)(lastRow + 1); skippedRow <= result.highestStateIndex; ++skippedRow) { if(isRewardFile) {
++result.numberOfNonzeroEntries; while (buf[0] != '\0') {
}
}
return result; // Read next transition.
} row = checked_strtol(buf, &buf);
col = checked_strtol(buf, &buf);
val = checked_strtod(buf, &buf);
storm::storage::SparseMatrix<double> DeterministicSparseTransitionParser::parse(std::string const& filename, bool isRewardFile, RewardMatrixInformationStruct const& rewardMatrixInformation, bool insertDiagonalEntriesIfMissing) { resultMatrix.addNextValue(row, col, val);
// Enforce locale where decimal point is '.'. buf = trimWhitespaces(buf);
setlocale(LC_NUMERIC, "C"); }
} else {
while (buf[0] != '\0') {
// Read next transition.
row = checked_strtol(buf, &buf);
col = checked_strtol(buf, &buf);
val = checked_strtod(buf, &buf);
// Read probability of this transition.
// Check, if the value is a probability, i.e. if it is between 0 and 1.
if ((val < 0.0) || (val > 1.0)) {
LOG4CPLUS_ERROR(logger, "Expected a positive probability but got \"" << val << "\".");
throw storm::exceptions::WrongFormatException();
}
if (!fileExistsAndIsReadable(filename.c_str())) { // Test if we moved to a new row.
LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": File does not exist or is not readable."); // Handle all incomplete or skipped rows.
throw storm::exceptions::FileIoException() << "The supplied Transition input file \"" << filename << "\" does not exist or is not readable by this process."; if (lastRow != row) {
} if (!rowHadDiagonalEntry) {
if (insertDiagonalEntriesIfMissing) {
resultMatrix.addNextValue(lastRow, lastRow, storm::utility::constantZero<double>());
LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << lastRow << " has no transition to itself. Inserted a 0-transition. (1)");
} else {
LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << lastRow << " has no transition to itself.");
}
// No increment for lastRow.
rowHadDiagonalEntry = true;
}
for (uint_fast64_t skippedRow = lastRow + 1; skippedRow < row; ++skippedRow) {
hadDeadlocks = true;
if (fixDeadlocks) {
resultMatrix.addNextValue(skippedRow, skippedRow, storm::utility::constantOne<double>());
rowHadDiagonalEntry = true;
LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << skippedRow << " has no outgoing transitions. A self-loop was inserted.");
} else {
LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": state " << skippedRow << " has no outgoing transitions.");
// Before throwing the appropriate exception we will give notice of all deadlock states.
}
}
lastRow = row;
rowHadDiagonalEntry = false;
}
// Find out about the used line endings. if (col == row) {
SupportedLineEndingsEnum lineEndings = findUsedLineEndings(filename, true); rowHadDiagonalEntry = true;
}
// Open file. if (col > row && !rowHadDiagonalEntry) {
MappedFile file(filename.c_str()); if (insertDiagonalEntriesIfMissing) {
char* buf = file.data; resultMatrix.addNextValue(row, row, storm::utility::constantZero<double>());
LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << row << " has no transition to itself. Inserted a 0-transition. (2)");
} else {
LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << row << " has no transition to itself.");
}
rowHadDiagonalEntry = true;
}
// Perform first pass, i.e. count entries that are not zero. resultMatrix.addNextValue(row, col, val);
buf = trimWhitespaces(buf);
}
DeterministicSparseTransitionParser::FirstPassResult firstPass = DeterministicSparseTransitionParser::firstPass(file.data, lineEndings, insertDiagonalEntriesIfMissing); if (!rowHadDiagonalEntry) {
if (insertDiagonalEntriesIfMissing) {
resultMatrix.addNextValue(lastRow, lastRow, storm::utility::constantZero<double>());
LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << lastRow << " has no transition to itself. Inserted a 0-transition. (3)");
} else {
LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << lastRow << " has no transition to itself.");
}
}
LOG4CPLUS_INFO(logger, "First pass on " << filename << " shows " << firstPass.numberOfNonzeroEntries << " NonZeros."); // If we encountered deadlock and did not fix them, now is the time to throw the exception.
if (!fixDeadlocks && hadDeadlocks) throw storm::exceptions::WrongFormatException() << "Some of the nodes had deadlocks. You can use --fixDeadlocks to insert self-loops on the fly.";
}
// If first pass returned zero, the file format was wrong. // Finally, build the actual matrix and return it.
if (firstPass.numberOfNonzeroEntries == 0) { return resultMatrix.build();
LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": empty or erroneous file format.");
throw storm::exceptions::WrongFormatException();
} }
// Perform second pass. DeterministicSparseTransitionParser::FirstPassResult DeterministicSparseTransitionParser::firstPass(char* buf, SupportedLineEndings lineEndings, bool insertDiagonalEntriesIfMissing) {
// Skip the format hint if it is there. DeterministicSparseTransitionParser::FirstPassResult result;
buf = trimWhitespaces(buf);
if(buf[0] < '0' || buf[0] > '9') {
buf = storm::parser::forwardToNextLine(buf, lineEndings);
}
if(isRewardFile) { // Skip the format hint if it is there.
// The reward matrix should match the size of the transition matrix. buf = trimWhitespaces(buf);
if (firstPass.highestStateIndex + 1 > rewardMatrixInformation.rowCount || firstPass.highestStateIndex + 1 > rewardMatrixInformation.columnCount) { if(buf[0] < '0' || buf[0] > '9') {
LOG4CPLUS_ERROR(logger, "Reward matrix has more rows or columns than transition matrix."); buf = storm::parser::forwardToNextLine(buf, lineEndings);
throw storm::exceptions::WrongFormatException() << "Reward matrix has more rows or columns than transition matrix.";
} else {
// If we found the right number of states or less, we set it to the number of states represented by the transition matrix.
firstPass.highestStateIndex = rewardMatrixInformation.rowCount - 1;
} }
}
// Creating matrix builder here.
// The actual matrix will be build once all contents are inserted.
storm::storage::SparseMatrixBuilder<double> resultMatrix(firstPass.highestStateIndex + 1, firstPass.highestStateIndex + 1, firstPass.numberOfNonzeroEntries);
uint_fast64_t row, col, lastRow = 0; // Check all transitions for non-zero diagonal entries and deadlock states.
double val; uint_fast64_t row, col, lastRow = 0;
bool fixDeadlocks = storm::settings::Settings::getInstance()->isSet("fixDeadlocks"); bool rowHadDiagonalEntry = false;
bool hadDeadlocks = false;
bool rowHadDiagonalEntry = false;
// Read all transitions from file. Note that we assume that the
// transitions are listed in canonical order, otherwise this will not
// work, i.e. the values in the matrix will be at wrong places.
// Different parsing routines for transition systems and transition rewards.
if(isRewardFile) {
while (buf[0] != '\0') {
// Read next transition.
row = checked_strtol(buf, &buf);
col = checked_strtol(buf, &buf);
val = checked_strtod(buf, &buf);
resultMatrix.addNextValue(row, col, val);
buf = trimWhitespaces(buf);
}
} else {
while (buf[0] != '\0') { while (buf[0] != '\0') {
// Read next transition. // Read the transition.
row = checked_strtol(buf, &buf); row = checked_strtol(buf, &buf);
col = checked_strtol(buf, &buf); col = checked_strtol(buf, &buf);
val = checked_strtod(buf, &buf); // The actual read value is not needed here.
checked_strtod(buf, &buf);
// Read probability of this transition. // Compensate for missing diagonal entries if desired.
// Check, if the value is a probability, i.e. if it is between 0 and 1. if (insertDiagonalEntriesIfMissing) {
if ((val < 0.0) || (val > 1.0)) { if (lastRow != row) {
LOG4CPLUS_ERROR(logger, "Expected a positive probability but got \"" << val << "\"."); if(!rowHadDiagonalEntry) {
throw storm::exceptions::WrongFormatException(); ++result.numberOfNonzeroEntries;
}
// Test if we moved to a new row.
// Handle all incomplete or skipped rows.
if (lastRow != row) {
if (!rowHadDiagonalEntry) {
if (insertDiagonalEntriesIfMissing) {
resultMatrix.addNextValue(lastRow, lastRow, storm::utility::constantZero<double>());
LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << lastRow << " has no transition to itself. Inserted a 0-transition. (1)");
} else {
LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << lastRow << " has no transition to itself.");
} }
// No increment for lastRow. // Compensate for missing rows.
rowHadDiagonalEntry = true; for (uint_fast64_t skippedRow = lastRow + 1; skippedRow < row; ++skippedRow) {
} ++result.numberOfNonzeroEntries;
for (uint_fast64_t skippedRow = lastRow + 1; skippedRow < row; ++skippedRow) {
hadDeadlocks = true;
if (fixDeadlocks) {
resultMatrix.addNextValue(skippedRow, skippedRow, storm::utility::constantOne<double>());
rowHadDiagonalEntry = true;
LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << skippedRow << " has no outgoing transitions. A self-loop was inserted.");
} else {
LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": state " << skippedRow << " has no outgoing transitions.");
// Before throwing the appropriate exception we will give notice of all deadlock states.
} }
lastRow = row;
rowHadDiagonalEntry = false;
} }
lastRow = row;
rowHadDiagonalEntry = false;
}
if (col == row) { if (col == row) {
rowHadDiagonalEntry = true; rowHadDiagonalEntry = true;
} }
if (col > row && !rowHadDiagonalEntry) { if (col > row && !rowHadDiagonalEntry) {
if (insertDiagonalEntriesIfMissing) { rowHadDiagonalEntry = true;
resultMatrix.addNextValue(row, row, storm::utility::constantZero<double>()); ++result.numberOfNonzeroEntries;
LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << row << " has no transition to itself. Inserted a 0-transition. (2)");
} else {
LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << row << " has no transition to itself.");
} }
rowHadDiagonalEntry = true;
} }
resultMatrix.addNextValue(row, col, val); // Check if a higher state id was found.
if (row > result.highestStateIndex) result.highestStateIndex = row;
if (col > result.highestStateIndex) result.highestStateIndex = col;
++result.numberOfNonzeroEntries;
buf = trimWhitespaces(buf); buf = trimWhitespaces(buf);
} }
if (!rowHadDiagonalEntry) { if(insertDiagonalEntriesIfMissing) {
if (insertDiagonalEntriesIfMissing) { if (!rowHadDiagonalEntry) {
resultMatrix.addNextValue(lastRow, lastRow, storm::utility::constantZero<double>()); ++result.numberOfNonzeroEntries;
LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << lastRow << " has no transition to itself. Inserted a 0-transition. (3)"); }
} else { //Compensate for missing rows at the end of the file.
LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << lastRow << " has no transition to itself."); for (uint_fast64_t skippedRow = (uint_fast64_t)(lastRow + 1); skippedRow <= result.highestStateIndex; ++skippedRow) {
++result.numberOfNonzeroEntries;
} }
} }
// If we encountered deadlock and did not fix them, now is the time to throw the exception. return result;
if (!fixDeadlocks && hadDeadlocks) throw storm::exceptions::WrongFormatException() << "Some of the nodes had deadlocks. You can use --fixDeadlocks to insert self-loops on the fly.";
} }
// Finally, build the actual matrix and return it. } // namespace parser
return resultMatrix.build();
}
} // namespace parser
} // namespace storm } // namespace storm

14
src/parser/DeterministicSparseTransitionParser.h

@ -34,7 +34,7 @@ public:
* @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 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 SparseMatrix containing the parsed transition system. * @return A SparseMatrix containing the parsed transition system.
*/ */
static storm::storage::SparseMatrix<double> parseDeterministicTransitions(std::string const& filename, bool insertDiagonalEntriesIfMissing = true); static storm::storage::SparseMatrix<double> parseDeterministicTransitions(std::string const& filename);
/*! /*!
* Load the transition rewards for a deterministic transition system from file and create a * Load the transition rewards for a deterministic transition system from file and create a
@ -46,10 +46,11 @@ public:
* sparse adjacency matrix whose entries represent the rewards of the respective transitions. * sparse adjacency matrix whose entries represent the rewards of the respective transitions.
* *
* @param filename The path of file to be parsed. * @param filename The path of file to be parsed.
* @param rewardMatrixInformation A struct containing information that is used to check if the transition reward matrix fits to the rest of the model. * @param transitionMatrix The transition matrix of the model in which the reward matrix is to be used in.
* The dimensions (rows and columns) of the two matrices should match.
* @return A SparseMatrix containing the parsed transition rewards. * @return A SparseMatrix containing the parsed transition rewards.
*/ */
static storm::storage::SparseMatrix<double> parseDeterministicTransitionRewards(std::string const& filename, RewardMatrixInformationStruct const& rewardMatrixInformation); static storm::storage::SparseMatrix<double> parseDeterministicTransitionRewards(std::string const& filename, storm::storage::SparseMatrix<double> const & transitionMatrix);
private: private:
@ -62,7 +63,7 @@ private:
* @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 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. * @return A structure representing the result of the first pass.
*/ */
static FirstPassResult firstPass(char* buffer, SupportedLineEndingsEnum lineEndings, bool insertDiagonalEntriesIfMissing = true); static FirstPassResult firstPass(char* buffer, SupportedLineEndings lineEndings, bool insertDiagonalEntriesIfMissing = true);
/* /*
* The main parsing routine. * The main parsing routine.
@ -71,10 +72,11 @@ private:
* @param filename The path of file to be parsed. * @param filename The path of file to be parsed.
* @param rewardFile A flag set iff the file to be parsed contains transition rewards. * @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 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. * @param transitionMatrix The transition matrix of the model in which the reward matrix is to be used in.
* The dimensions (rows and columns) of the two matrices should match.
* @return A SparseMatrix containing the parsed file contents. * @return A SparseMatrix containing the parsed file contents.
*/ */
static storm::storage::SparseMatrix<double> parse(std::string const& filename, bool isRewardFile, RewardMatrixInformationStruct const& rewardMatrixInformation, bool insertDiagonalEntriesIfMissing = false); static storm::storage::SparseMatrix<double> parse(std::string const& filename, bool isRewardFile, storm::storage::SparseMatrix<double> const & transitionMatrix);
}; };

101
src/parser/MappedFile.cpp

@ -0,0 +1,101 @@
/*
* MappedFile.cpp
*
* Created on: Jan 21, 2014
* Author: Manuel Sascha Weiand
*/
#include "src/parser/MappedFile.h"
#include <fstream>
#include <cstring>
#include <fcntl.h>
#include <iostream>
#include <string>
#include <boost/integer/integer_mask.hpp>
#include "src/exceptions/FileIoException.h"
#include "log4cplus/logger.h"
#include "log4cplus/loggingmacros.h"
extern log4cplus::Logger logger;
namespace storm {
namespace parser {
MappedFile::MappedFile(const char* filename) {
#if defined LINUX || defined MACOSX
/*
* Do file mapping for reasonable systems.
* stat64(), open(), mmap()
*/
#ifdef MACOSX
if (stat(filename, &(this->st)) != 0) {
#else
if (stat64(filename, &(this->st)) != 0) {
#endif
LOG4CPLUS_ERROR(logger, "Error in stat(" << filename << "): Probably, this file does not exist.");
throw exceptions::FileIoException() << "MappedFile Error in stat(): Probably, this file does not exist.";
}
this->file = open(filename, O_RDONLY);
if (this->file < 0) {
LOG4CPLUS_ERROR(logger, "Error in open(" << filename << "): Probably, we may not read this file.");
throw exceptions::FileIoException() << "MappedFile Error in open(): Probably, we may not read this file.";
}
this->data = reinterpret_cast<char*>(mmap(NULL, this->st.st_size, PROT_READ, MAP_PRIVATE, this->file, 0));
if (this->data == reinterpret_cast<char*>(-1)) {
close(this->file);
LOG4CPLUS_ERROR(logger, "Error in mmap(" << filename << "): " << std::strerror(errno));
throw exceptions::FileIoException() << "MappedFile Error in mmap(): " << std::strerror(errno);
}
this->dataend = this->data + this->st.st_size;
#elif defined WINDOWS
/*
* Do file mapping for windows.
* _stat64(), CreateFile(), CreateFileMapping(), MapViewOfFile()
*/
if (_stat64(filename, &(this->st)) != 0) {
LOG4CPLUS_ERROR(logger, "Error in _stat(" << filename << "): Probably, this file does not exist.");
throw exceptions::FileIoException("MappedFile Error in stat(): Probably, this file does not exist.");
}
this->file = CreateFileA(filename, GENERIC_READ, 0, NULL, OPEN_ALWAYS, FILE_ATTRIBUTE_NORMAL, NULL);
if (this->file == INVALID_HANDLE_VALUE) {
LOG4CPLUS_ERROR(logger, "Error in CreateFileA(" << filename << "): Probably, we may not read this file.");
throw exceptions::FileIoException("MappedFile Error in CreateFileA(): Probably, we may not read this file.");
}
this->mapping = CreateFileMappingA(this->file, NULL, PAGE_READONLY, (DWORD)(st.st_size >> 32), (DWORD)st.st_size, NULL);
if (this->mapping == NULL) {
CloseHandle(this->file);
LOG4CPLUS_ERROR(logger, "Error in CreateFileMappingA(" << filename << ").");
throw exceptions::FileIoException("MappedFile Error in CreateFileMappingA().");
}
this->data = static_cast<char*>(MapViewOfFile(this->mapping, FILE_MAP_READ, 0, 0, this->st.st_size));
if (this->data == NULL) {
CloseHandle(this->mapping);
CloseHandle(this->file);
LOG4CPLUS_ERROR(logger, "Error in MapViewOfFile(" << filename << ").");
throw exceptions::FileIoException("MappedFile Error in MapViewOfFile().");
}
this->dataend = this->data + this->st.st_size;
#endif
}
MappedFile::~MappedFile() {
#if defined LINUX || defined MACOSX
munmap(this->data, this->st.st_size);
close(this->file);
#elif defined WINDOWS
CloseHandle(this->mapping);
CloseHandle(this->file);
#endif
}
} // namespace parser
} // namespace storm

95
src/parser/MappedFile.h

@ -0,0 +1,95 @@
/*
* MappedFile.h
*
* Created on: Jan 21, 2014
* Author: Manuel Sascha Weiand
*/
#ifndef STORM_PARSER_MAPPEDFILE_H_
#define STORM_PARSER_MAPPEDFILE_H_
#include <sys/stat.h>
#include "src/utility/OsDetection.h"
namespace storm {
namespace parser {
/*!
* @brief Opens a file and maps it to memory providing a char*
* containing the file content.
*
* This class is a very simple interface to read files efficiently.
* The given file is opened and mapped to memory using mmap().
* The public member data is a pointer to the actual file content.
* Using this method, the kernel will take care of all buffering. This is
* most probably much more efficient than doing this manually.
*/
#if !defined LINUX && !defined MACOSX && !defined WINDOWS
#error Platform not supported
#endif
class MappedFile {
public:
/*!
* Constructor of MappedFile.
* Will stat the given file, open it and map it to memory.
* If anything of this fails, an appropriate exception is raised
* and a log entry is written.
* @param filename file to be opened
*/
MappedFile(const char* filename);
/*!
* Destructor of MappedFile.
* Will unmap the data and close the file.
*/
~MappedFile();
/*!
* @brief pointer to actual file content.
*/
char* data;
/*!
* @brief pointer to end of file content.
*/
char* dataend;
private:
#if defined LINUX || defined MACOSX
/*!
* @brief file descriptor obtained by open().
*/
int file;
#elif defined WINDOWS
HANDLE file;
HANDLE mapping;
#endif
#if defined LINUX
/*!
* @brief stat information about the file.
*/
struct stat64 st;
#elif defined MACOSX
/*!
* @brief stat information about the file.
*/
struct stat st;
#elif defined WINDOWS
/*!
* @brief stat information about the file.
*/
struct __stat64 st;
#endif
};
} // namespace parser
} // namespace storm
#endif /* STORM_PARSER_MAPPEDFILE_H_ */

7
src/parser/MarkovAutomatonSparseTransitionParser.cpp

@ -2,12 +2,13 @@
#include "src/settings/Settings.h" #include "src/settings/Settings.h"
#include "src/exceptions/WrongFormatException.h" #include "src/exceptions/WrongFormatException.h"
#include "MappedFile.h"
namespace storm { namespace storm {
namespace parser { namespace parser {
MarkovAutomatonSparseTransitionParser::FirstPassResult MarkovAutomatonSparseTransitionParser::firstPass(char* buf, SupportedLineEndingsEnum lineEndings) { MarkovAutomatonSparseTransitionParser::FirstPassResult MarkovAutomatonSparseTransitionParser::firstPass(char* buf, SupportedLineEndings lineEndings) {
MarkovAutomatonSparseTransitionParser::FirstPassResult result; MarkovAutomatonSparseTransitionParser::FirstPassResult result;
bool fixDeadlocks = storm::settings::Settings::getInstance()->isSet("fixDeadlocks"); bool fixDeadlocks = storm::settings::Settings::getInstance()->isSet("fixDeadlocks");
@ -142,7 +143,7 @@ MarkovAutomatonSparseTransitionParser::FirstPassResult MarkovAutomatonSparseTran
return result; return result;
} }
MarkovAutomatonSparseTransitionParser::ResultType MarkovAutomatonSparseTransitionParser::secondPass(char* buf, SupportedLineEndingsEnum lineEndings, FirstPassResult const& firstPassResult) { MarkovAutomatonSparseTransitionParser::ResultType MarkovAutomatonSparseTransitionParser::secondPass(char* buf, SupportedLineEndings lineEndings, FirstPassResult const& firstPassResult) {
ResultType result(firstPassResult); ResultType result(firstPassResult);
bool fixDeadlocks = storm::settings::Settings::getInstance()->isSet("fixDeadlocks"); bool fixDeadlocks = storm::settings::Settings::getInstance()->isSet("fixDeadlocks");
@ -252,7 +253,7 @@ MarkovAutomatonSparseTransitionParser::ResultType MarkovAutomatonSparseTransitio
} }
// Determine used line endings. // Determine used line endings.
SupportedLineEndingsEnum lineEndings = findUsedLineEndings(filename, true); SupportedLineEndings lineEndings = findUsedLineEndings(filename, true);
// Open file and prepare pointer to buffer. // Open file and prepare pointer to buffer.
MappedFile file(filename.c_str()); MappedFile file(filename.c_str());

4
src/parser/MarkovAutomatonSparseTransitionParser.h

@ -80,7 +80,7 @@ private:
* @param lineEndings The line endings that are to be used while parsing. * @param lineEndings The line endings that are to be used while parsing.
* @return A structure representing the result of the first pass. * @return A structure representing the result of the first pass.
*/ */
static FirstPassResult firstPass(char* buffer, SupportedLineEndingsEnum lineEndings); static FirstPassResult firstPass(char* buffer, SupportedLineEndings lineEndings);
/* /*
* Performs the second pass on the input pointed to by the given buffer with the information of the first pass. * Performs the second pass on the input pointed to by the given buffer with the information of the first pass.
@ -90,7 +90,7 @@ private:
* @param firstPassResult The result of the first pass performed on the same input. * @param firstPassResult The result of the first pass performed on the same input.
* @return A structure representing the result of the second pass. * @return A structure representing the result of the second pass.
*/ */
static ResultType secondPass(char* buffer, SupportedLineEndingsEnum lineEndings, FirstPassResult const& firstPassResult); static ResultType secondPass(char* buffer, SupportedLineEndings lineEndings, FirstPassResult const& firstPassResult);
}; };
} // namespace parser } // namespace parser

27
src/parser/NondeterministicModelParser.cpp

@ -29,26 +29,31 @@ namespace storm {
NondeterministicModelParser::Result NondeterministicModelParser::parseNondeterministicModel(std::string const & transitionSystemFile, std::string const & labelingFile, NondeterministicModelParser::Result NondeterministicModelParser::parseNondeterministicModel(std::string const & transitionSystemFile, std::string const & labelingFile,
std::string const & stateRewardFile, std::string const & transitionRewardFile) { std::string const & stateRewardFile, std::string const & transitionRewardFile) {
NondeterministicSparseTransitionParser::Result transitionParserResult(std::move(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions(transitionSystemFile))); // Parse the transitions.
storm::storage::SparseMatrix<double> transitions(std::move(transitionParserResult.transitionMatrix)); NondeterministicSparseTransitionParser::Result transitions(std::move(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions(transitionSystemFile)));
uint_fast64_t stateCount = transitions.getColumnCount(); uint_fast64_t stateCount = transitions.transitionMatrix.getColumnCount();
uint_fast64_t rowCount = transitions.getRowCount();
// Parse the state labeling.
storm::models::AtomicPropositionsLabeling labeling(std::move(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(stateCount, labelingFile))); storm::models::AtomicPropositionsLabeling labeling(std::move(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(stateCount, labelingFile)));
Result result(std::move(transitions), std::move(transitionParserResult.rowMapping), std::move(labeling)); // Only parse state rewards if a file is given.
boost::optional<std::vector<double>> stateRewards;
// Only parse state rewards of a file is given.
if (stateRewardFile != "") { if (stateRewardFile != "") {
result.stateRewards.reset(storm::parser::SparseStateRewardParser::parseSparseStateReward(stateCount, stateRewardFile)); stateRewards = storm::parser::SparseStateRewardParser::parseSparseStateReward(stateCount, stateRewardFile);
} }
// Only parse transition rewards of a file is given. // Only parse transition rewards if a file is given.
boost::optional<storm::storage::SparseMatrix<double>> transitionRewards;
if (transitionRewardFile != "") { if (transitionRewardFile != "") {
RewardMatrixInformationStruct rewardMatrixInfo(rowCount, stateCount, &result.rowMapping); transitionRewards = storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitionRewards(transitionRewardFile, transitions).transitionMatrix;
result.transitionRewards.reset(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitionRewards(transitionRewardFile, rewardMatrixInfo).transitionMatrix);
} }
// Construct the result.
Result result(std::move(transitions.transitionMatrix), std::move(transitions.rowMapping), std::move(labeling));
result.stateRewards = stateRewards;
result.transitionRewards = transitionRewards;
return result; return result;
} }

241
src/parser/NondeterministicSparseTransitionParser.cpp

@ -9,6 +9,7 @@
#include <string> #include <string>
#include "src/parser/MappedFile.h"
#include "src/settings/Settings.h" #include "src/settings/Settings.h"
#include "src/exceptions/FileIoException.h" #include "src/exceptions/FileIoException.h"
#include "src/exceptions/WrongFormatException.h" #include "src/exceptions/WrongFormatException.h"
@ -22,125 +23,17 @@ namespace storm {
NondeterministicSparseTransitionParser::Result NondeterministicSparseTransitionParser::parseNondeterministicTransitions(std::string const& filename) { NondeterministicSparseTransitionParser::Result NondeterministicSparseTransitionParser::parseNondeterministicTransitions(std::string const& filename) {
RewardMatrixInformationStruct nullInformation; Result emptyResult;
return NondeterministicSparseTransitionParser::parse(filename, false, nullInformation); return NondeterministicSparseTransitionParser::parse(filename, false, emptyResult);
} }
NondeterministicSparseTransitionParser::Result NondeterministicSparseTransitionParser::parseNondeterministicTransitionRewards(std::string const& filename, RewardMatrixInformationStruct const& rewardMatrixInformation) { NondeterministicSparseTransitionParser::Result NondeterministicSparseTransitionParser::parseNondeterministicTransitionRewards(std::string const& filename, Result const & modelInformation) {
return NondeterministicSparseTransitionParser::parse(filename, true, rewardMatrixInformation); return NondeterministicSparseTransitionParser::parse(filename, true, modelInformation);
} }
NondeterministicSparseTransitionParser::FirstPassResult NondeterministicSparseTransitionParser::firstPass(char* buf, SupportedLineEndingsEnum lineEndings, bool isRewardFile, RewardMatrixInformationStruct const& rewardMatrixInformation) { NondeterministicSparseTransitionParser::Result NondeterministicSparseTransitionParser::parse(std::string const &filename, bool isRewardFile, Result const & modelInformation) {
// 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 all transitions.
uint_fast64_t source = 0, target = 0, choice = 0, lastchoice = 0, lastsource = 0;
double val = 0.0;
NondeterministicSparseTransitionParser::FirstPassResult result;
// Since the first line is already a new choice but is not covered below, that has to be covered here.
result.choices = 1;
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 > result.highestStateIndex) {
result.highestStateIndex = source;
}
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;
}
// 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;
}
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 (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]);
}
}
return result;
}
NondeterministicSparseTransitionParser::Result NondeterministicSparseTransitionParser::parse(std::string const &filename, bool isRewardFile, RewardMatrixInformationStruct const& rewardMatrixInformation) {
// Enforce locale where decimal point is '.'. // Enforce locale where decimal point is '.'.
setlocale(LC_NUMERIC, "C"); setlocale(LC_NUMERIC, "C");
@ -151,14 +44,14 @@ namespace storm {
} }
// Find out about the used line endings. // Find out about the used line endings.
SupportedLineEndingsEnum lineEndings = findUsedLineEndings(filename, true); SupportedLineEndings lineEndings = findUsedLineEndings(filename, true);
// Open file. // Open file.
MappedFile file(filename.c_str()); MappedFile file(filename.c_str());
char* buf = file.data; char* buf = file.data;
// Perform first pass, i.e. obtain number of columns, rows and non-zero elements. // Perform first pass, i.e. obtain number of columns, rows and non-zero elements.
NondeterministicSparseTransitionParser::FirstPassResult firstPass = NondeterministicSparseTransitionParser::firstPass(file.data, lineEndings, isRewardFile, rewardMatrixInformation); NondeterministicSparseTransitionParser::FirstPassResult firstPass = NondeterministicSparseTransitionParser::firstPass(file.data, lineEndings, isRewardFile, modelInformation);
// If first pass returned zero, the file format was wrong. // If first pass returned zero, the file format was wrong.
if (firstPass.numberOfNonzeroEntries == 0) { if (firstPass.numberOfNonzeroEntries == 0) {
@ -176,14 +69,14 @@ namespace storm {
if (isRewardFile) { if (isRewardFile) {
// The reward matrix should match the size of the transition matrix. // The reward matrix should match the size of the transition matrix.
if (firstPass.choices > rewardMatrixInformation.rowCount || (uint_fast64_t)(firstPass.highestStateIndex + 1) > rewardMatrixInformation.columnCount) { if (firstPass.choices > modelInformation.transitionMatrix.getRowCount() || (uint_fast64_t)(firstPass.highestStateIndex + 1) > modelInformation.transitionMatrix.getColumnCount()) {
LOG4CPLUS_ERROR(logger, "Reward matrix size exceeds transition matrix size."); LOG4CPLUS_ERROR(logger, "Reward matrix size exceeds transition matrix size.");
throw storm::exceptions::WrongFormatException() << "Reward matrix size exceeds transition matrix size."; throw storm::exceptions::WrongFormatException() << "Reward matrix size exceeds transition matrix size.";
} else if (firstPass.choices != rewardMatrixInformation.rowCount) { } else if (firstPass.choices != modelInformation.transitionMatrix.getRowCount()) {
LOG4CPLUS_ERROR(logger, "Reward matrix row count does not match transition matrix row count."); 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."; throw storm::exceptions::WrongFormatException() << "Reward matrix row count does not match transition matrix row count.";
} else { } else {
firstPass.highestStateIndex = rewardMatrixInformation.columnCount - 1; firstPass.highestStateIndex = modelInformation.transitionMatrix.getColumnCount() - 1;
} }
} }
@ -214,13 +107,13 @@ namespace storm {
// If we have switched the source state, we possibly need to insert the rows of the last // If we have switched the source state, we possibly need to insert the rows of the last
// source state. // source state.
if (source != lastsource) { if (source != lastsource) {
curRow += ((*rewardMatrixInformation.nondeterministicChoiceIndices)[lastsource + 1] - (*rewardMatrixInformation.nondeterministicChoiceIndices)[lastsource]) -(lastchoice + 1); curRow += ((modelInformation.rowMapping)[lastsource + 1] - (modelInformation.rowMapping)[lastsource]) -(lastchoice + 1);
} }
// If we skipped some states, we need to reserve empty rows for all their nondeterministic // If we skipped some states, we need to reserve empty rows for all their nondeterministic
// choices. // choices.
for (uint_fast64_t i = lastsource + 1; i < source; ++i) { for (uint_fast64_t i = lastsource + 1; i < source; ++i) {
curRow += ((*rewardMatrixInformation.nondeterministicChoiceIndices)[i + 1] - (*rewardMatrixInformation.nondeterministicChoiceIndices)[i]); curRow += ((modelInformation.rowMapping)[i + 1] - (modelInformation.rowMapping)[i]);
} }
// If we advanced to the next state, but skipped some choices, we have to reserve rows // If we advanced to the next state, but skipped some choices, we have to reserve rows
@ -279,5 +172,113 @@ namespace storm {
return NondeterministicSparseTransitionParser::Result(matrixBuilder.build(), rowMapping); return NondeterministicSparseTransitionParser::Result(matrixBuilder.build(), rowMapping);
} }
NondeterministicSparseTransitionParser::FirstPassResult NondeterministicSparseTransitionParser::firstPass(char* buf, SupportedLineEndings lineEndings, bool isRewardFile, Result const & modelInformation) {
// 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 all transitions.
uint_fast64_t source = 0, target = 0, choice = 0, lastchoice = 0, lastsource = 0;
double val = 0.0;
NondeterministicSparseTransitionParser::FirstPassResult result;
// Since the first line is already a new choice but is not covered below, that has to be covered here.
result.choices = 1;
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 > result.highestStateIndex) {
result.highestStateIndex = source;
}
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 += ((modelInformation.rowMapping)[lastsource + 1] - (modelInformation.rowMapping)[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 += ((modelInformation.rowMapping)[i + 1] - (modelInformation.rowMapping)[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;
}
// 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;
}
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 (isRewardFile) {
// If not all rows were filled for the last state, we need to insert them.
result.choices += ((modelInformation.rowMapping)[lastsource + 1] - (modelInformation.rowMapping)[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 < modelInformation.rowMapping.size() - 1; ++i) {
result.choices += ((modelInformation.rowMapping)[i + 1] - (modelInformation.rowMapping)[i]);
}
}
return result;
}
} // namespace parser } // namespace parser
} // namespace storm } // namespace storm

26
src/parser/NondeterministicSparseTransitionParser.h

@ -39,6 +39,12 @@ namespace storm {
*/ */
struct Result { struct Result {
// Constructs an empty Result.
Result() : transitionMatrix(), rowMapping() {
// Intentionally left empty.
}
// Constructs a Result, initializing its members with the given values.
Result(storm::storage::SparseMatrix<double> transitionMatrix, std::vector<uint_fast64_t> rowMapping) : transitionMatrix(transitionMatrix), rowMapping(rowMapping) { Result(storm::storage::SparseMatrix<double> transitionMatrix, std::vector<uint_fast64_t> rowMapping) : transitionMatrix(transitionMatrix), rowMapping(rowMapping) {
// Intentionally left empty. // Intentionally left empty.
} }
@ -52,16 +58,22 @@ namespace storm {
}; };
/*! /*!
* @brief Load a nondeterministic transition system from file and create a * @brief Load a nondeterministic transition system from file and create a
* sparse adjacency matrix whose entries represent the weights of the edges * sparse adjacency matrix whose entries represent the weights of the edges
*
* @param filename The path of file to be parsed.
*/ */
static Result parseNondeterministicTransitions(std::string const &filename); static Result parseNondeterministicTransitions(std::string const & filename);
/*! /*!
* @brief Load a nondeterministic transition system from file and create a * @brief Load a nondeterministic transition system from file and create a
* sparse adjacency matrix whose entries represent the weights of the edges * sparse adjacency matrix whose entries represent the weights of the edges
*
* @param filename The path of file to be parsed.
* @param modelInformation The information about the transition structure of nondeterministic model in which the transition rewards shall be used.
* @return A struct containing the parsed file contents, i.e. the transition reward matrix and the mapping between its rows and the states of the model.
*/ */
static Result parseNondeterministicTransitionRewards(std::string const &filename, RewardMatrixInformationStruct const& rewardMatrixInformation); static Result parseNondeterministicTransitionRewards(std::string const & filename, Result const & modelInformation);
private: private:
@ -79,7 +91,7 @@ namespace storm {
* @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 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. * @return A structure representing the result of the first pass.
*/ */
static FirstPassResult firstPass(char* buffer, SupportedLineEndingsEnum lineEndings, bool isRewardFile, RewardMatrixInformationStruct const& rewardMatrixInformation); static FirstPassResult firstPass(char* buffer, SupportedLineEndings lineEndings, bool isRewardFile, Result const & modelInformation);
/*! /*!
* The main parsing routine. * The main parsing routine.
@ -88,10 +100,10 @@ namespace storm {
* @param filename The path of file to be parsed. * @param filename The path of file to be parsed.
* @param rewardFile A flag set iff the file to be parsed contains transition rewards. * @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 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. * @param modelInformation 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. * @return A SparseMatrix containing the parsed file contents.
*/ */
static Result parse(std::string const& filename, bool isRewardFile, RewardMatrixInformationStruct const& rewardMatrixInformation); static Result parse(std::string const& filename, bool isRewardFile, Result const & modelInformation);
}; };

132
src/parser/Parser.cpp

@ -11,6 +11,7 @@
#include "src/exceptions/FileIoException.h" #include "src/exceptions/FileIoException.h"
#include "src/exceptions/WrongFormatException.h" #include "src/exceptions/WrongFormatException.h"
#include "src/utility/OsDetection.h" #include "src/utility/OsDetection.h"
#include "src/parser/MappedFile.h"
#include "log4cplus/logger.h" #include "log4cplus/logger.h"
#include "log4cplus/loggingmacros.h" #include "log4cplus/loggingmacros.h"
@ -91,7 +92,7 @@ char* trimWhitespaces(char* buf) {
/*! /*!
* @briefs Analyzes the given file and tries to find out the used file endings. * @briefs Analyzes the given file and tries to find out the used file endings.
*/ */
SupportedLineEndingsEnum findUsedLineEndings(std::string const& fileName, bool throwOnUnsupported) { SupportedLineEndings findUsedLineEndings(std::string const& fileName, bool throwOnUnsupported) {
MappedFile fileMap(fileName.c_str()); MappedFile fileMap(fileName.c_str());
char* buf = nullptr; char* buf = nullptr;
char* const bufferEnd = fileMap.dataend; char* const bufferEnd = fileMap.dataend;
@ -100,11 +101,11 @@ SupportedLineEndingsEnum findUsedLineEndings(std::string const& fileName, bool t
if (*buf == '\r') { if (*buf == '\r') {
// check for following \n // check for following \n
if (((buf + sizeof(char)) < bufferEnd) && (*(buf + sizeof(char)) == '\n')) { if (((buf + sizeof(char)) < bufferEnd) && (*(buf + sizeof(char)) == '\n')) {
return SupportedLineEndingsEnum::SlashRN; return SupportedLineEndings::SlashRN;
} }
return SupportedLineEndingsEnum::SlashR; return SupportedLineEndings::SlashR;
} else if (*buf == '\n') { } else if (*buf == '\n') {
return SupportedLineEndingsEnum::SlashN; return SupportedLineEndings::SlashN;
} }
} }
@ -114,25 +115,25 @@ SupportedLineEndingsEnum findUsedLineEndings(std::string const& fileName, bool t
} }
LOG4CPLUS_WARN(logger, "Error while parsing \"" << fileName << "\": Unsupported or unknown line-endings. Please use either of \\r, \\n or \\r\\n"); LOG4CPLUS_WARN(logger, "Error while parsing \"" << fileName << "\": Unsupported or unknown line-endings. Please use either of \\r, \\n or \\r\\n");
return SupportedLineEndingsEnum::Unsupported; return SupportedLineEndings::Unsupported;
} }
/*! /*!
* @brief Encapsulates the usage of function @strcspn to forward to the end of the line (next char is the newline character). * @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) { char* forwardToLineEnd(char* buffer, SupportedLineEndings lineEndings) {
switch (lineEndings) { switch (lineEndings) {
case SupportedLineEndingsEnum::SlashN: case SupportedLineEndings::SlashN:
return buffer + strcspn(buffer, "\n\0"); return buffer + strcspn(buffer, "\n\0");
break; break;
case SupportedLineEndingsEnum::SlashR: case SupportedLineEndings::SlashR:
return buffer + strcspn(buffer, "\r\0"); return buffer + strcspn(buffer, "\r\0");
break; break;
case SupportedLineEndingsEnum::SlashRN: case SupportedLineEndings::SlashRN:
return buffer + strcspn(buffer, "\r\0"); return buffer + strcspn(buffer, "\r\0");
break; break;
default: default:
case SupportedLineEndingsEnum::Unsupported: case SupportedLineEndings::Unsupported:
// This Line will never be reached as the Parser would have thrown already. // This Line will never be reached as the Parser would have thrown already.
throw; throw;
break; break;
@ -143,19 +144,19 @@ char* forwardToLineEnd(char* buffer, SupportedLineEndingsEnum lineEndings) {
/*! /*!
* @brief Encapsulates the usage of function @strchr to forward to the next line * @brief Encapsulates the usage of function @strchr to forward to the next line
*/ */
char* forwardToNextLine(char* buffer, SupportedLineEndingsEnum lineEndings) { char* forwardToNextLine(char* buffer, SupportedLineEndings lineEndings) {
switch (lineEndings) { switch (lineEndings) {
case SupportedLineEndingsEnum::SlashN: case SupportedLineEndings::SlashN:
return strchr(buffer, '\n') + 1; return strchr(buffer, '\n') + 1;
break; break;
case SupportedLineEndingsEnum::SlashR: case SupportedLineEndings::SlashR:
return strchr(buffer, '\r') + 1; return strchr(buffer, '\r') + 1;
break; break;
case SupportedLineEndingsEnum::SlashRN: case SupportedLineEndings::SlashRN:
return strchr(buffer, '\r') + 2; return strchr(buffer, '\r') + 2;
break; break;
default: default:
case SupportedLineEndingsEnum::Unsupported: case SupportedLineEndings::Unsupported:
// This Line will never be reached as the Parser would have thrown already. // This Line will never be reached as the Parser would have thrown already.
throw; throw;
break; break;
@ -168,26 +169,26 @@ char* forwardToNextLine(char* buffer, SupportedLineEndingsEnum lineEndings) {
* @param targetBuffer The Target for the hint, must be at least 64 bytes long * @param targetBuffer The Target for the hint, must be at least 64 bytes long
* @param buffer The Source Buffer from which the Model Hint will be read * @param buffer The Source Buffer from which the Model Hint will be read
*/ */
void scanForModelHint(char* targetBuffer, uint_fast64_t targetBufferSize, char const* buffer, SupportedLineEndingsEnum lineEndings) { void scanForModelHint(char* targetBuffer, uint_fast64_t targetBufferSize, char const* buffer, SupportedLineEndings lineEndings) {
if (targetBufferSize <= 4) { if (targetBufferSize <= 4) {
throw; throw;
} }
switch (lineEndings) { switch (lineEndings) {
case SupportedLineEndingsEnum::SlashN: case SupportedLineEndings::SlashN:
#ifdef WINDOWS #ifdef WINDOWS
sscanf_s(buffer, "%60s\n", targetBuffer, targetBufferSize); sscanf_s(buffer, "%60s\n", targetBuffer, targetBufferSize);
#else #else
sscanf(buffer, "%60s\n", targetBuffer); sscanf(buffer, "%60s\n", targetBuffer);
#endif #endif
break; break;
case SupportedLineEndingsEnum::SlashR: case SupportedLineEndings::SlashR:
#ifdef WINDOWS #ifdef WINDOWS
sscanf_s(buffer, "%60s\r", targetBuffer, sizeof(targetBufferSize)); sscanf_s(buffer, "%60s\r", targetBuffer, sizeof(targetBufferSize));
#else #else
sscanf(buffer, "%60s\r", targetBuffer); sscanf(buffer, "%60s\r", targetBuffer);
#endif #endif
break; break;
case SupportedLineEndingsEnum::SlashRN: case SupportedLineEndings::SlashRN:
#ifdef WINDOWS #ifdef WINDOWS
sscanf_s(buffer, "%60s\r\n", targetBuffer, sizeof(targetBufferSize)); sscanf_s(buffer, "%60s\r\n", targetBuffer, sizeof(targetBufferSize));
#else #else
@ -195,7 +196,7 @@ void scanForModelHint(char* targetBuffer, uint_fast64_t targetBufferSize, char c
#endif #endif
break; break;
default: default:
case SupportedLineEndingsEnum::Unsupported: case SupportedLineEndings::Unsupported:
// This Line will never be reached as the Parser would have thrown already. // This Line will never be reached as the Parser would have thrown already.
throw; throw;
break; break;
@ -205,13 +206,13 @@ void scanForModelHint(char* targetBuffer, uint_fast64_t targetBufferSize, char c
/*! /*!
* @brief Returns the matching Separator-String in the format of "BLANK\t\NEWLINESYMBOL(S)\0 * @brief Returns the matching Separator-String in the format of "BLANK\t\NEWLINESYMBOL(S)\0
*/ */
void getMatchingSeparatorString(char* targetBuffer, uint_fast64_t targetBufferSize, SupportedLineEndingsEnum lineEndings) { void getMatchingSeparatorString(char* targetBuffer, uint_fast64_t targetBufferSize, SupportedLineEndings lineEndings) {
if (targetBufferSize < 5) { if (targetBufferSize < 5) {
LOG4CPLUS_ERROR(logger, "getMatchingSeparatorString: The passed Target Buffer is too small."); LOG4CPLUS_ERROR(logger, "getMatchingSeparatorString: The passed Target Buffer is too small.");
throw; throw;
} }
switch (lineEndings) { switch (lineEndings) {
case SupportedLineEndingsEnum::SlashN: { case SupportedLineEndings::SlashN: {
char source[] = " \n\t"; char source[] = " \n\t";
#ifdef WINDOWS #ifdef WINDOWS
strncpy(targetBuffer, targetBufferSize, source, sizeof(source)); strncpy(targetBuffer, targetBufferSize, source, sizeof(source));
@ -220,7 +221,7 @@ void getMatchingSeparatorString(char* targetBuffer, uint_fast64_t targetBufferSi
#endif #endif
break; break;
} }
case SupportedLineEndingsEnum::SlashR: { case SupportedLineEndings::SlashR: {
char source[] = " \r\t"; char source[] = " \r\t";
#ifdef WINDOWS #ifdef WINDOWS
strncpy(targetBuffer, targetBufferSize, source, sizeof(source)); strncpy(targetBuffer, targetBufferSize, source, sizeof(source));
@ -229,7 +230,7 @@ void getMatchingSeparatorString(char* targetBuffer, uint_fast64_t targetBufferSi
#endif #endif
break; break;
} }
case SupportedLineEndingsEnum::SlashRN: { case SupportedLineEndings::SlashRN: {
char source[] = " \r\n\t"; char source[] = " \r\n\t";
#ifdef WINDOWS #ifdef WINDOWS
strncpy(targetBuffer, targetBufferSize, source, sizeof(source)); strncpy(targetBuffer, targetBufferSize, source, sizeof(source));
@ -239,7 +240,7 @@ void getMatchingSeparatorString(char* targetBuffer, uint_fast64_t targetBufferSi
break; break;
} }
default: default:
case SupportedLineEndingsEnum::Unsupported: case SupportedLineEndings::Unsupported:
// This Line will never be reached as the Parser would have thrown already. // This Line will never be reached as the Parser would have thrown already.
LOG4CPLUS_ERROR(logger, "getMatchingSeparatorString: The passed lineEndings were Unsupported. Check your input file."); LOG4CPLUS_ERROR(logger, "getMatchingSeparatorString: The passed lineEndings were Unsupported. Check your input file.");
throw; throw;
@ -247,87 +248,6 @@ void getMatchingSeparatorString(char* targetBuffer, uint_fast64_t targetBufferSi
} }
} }
/*!
* Will stat the given file, open it and map it to memory.
* If anything of this fails, an appropriate exception is raised
* and a log entry is written.
* @param filename file to be opened
*/
MappedFile::MappedFile(const char* filename) {
#if defined LINUX || defined MACOSX
/*
* Do file mapping for reasonable systems.
* stat64(), open(), mmap()
*/
#ifdef MACOSX
if (stat(filename, &(this->st)) != 0) {
#else
if (stat64(filename, &(this->st)) != 0) {
#endif
LOG4CPLUS_ERROR(logger, "Error in stat(" << filename << "): Probably, this file does not exist.");
throw exceptions::FileIoException() << "MappedFile Error in stat(): Probably, this file does not exist.";
}
this->file = open(filename, O_RDONLY);
if (this->file < 0) {
LOG4CPLUS_ERROR(logger, "Error in open(" << filename << "): Probably, we may not read this file.");
throw exceptions::FileIoException() << "MappedFile Error in open(): Probably, we may not read this file.";
}
this->data = reinterpret_cast<char*>(mmap(NULL, this->st.st_size, PROT_READ, MAP_PRIVATE, this->file, 0));
if (this->data == reinterpret_cast<char*>(-1)) {
close(this->file);
LOG4CPLUS_ERROR(logger, "Error in mmap(" << filename << "): " << std::strerror(errno));
throw exceptions::FileIoException() << "MappedFile Error in mmap(): " << std::strerror(errno);
}
this->dataend = this->data + this->st.st_size;
#elif defined WINDOWS
/*
* Do file mapping for windows.
* _stat64(), CreateFile(), CreateFileMapping(), MapViewOfFile()
*/
if (_stat64(filename, &(this->st)) != 0) {
LOG4CPLUS_ERROR(logger, "Error in _stat(" << filename << "): Probably, this file does not exist.");
throw exceptions::FileIoException("MappedFile Error in stat(): Probably, this file does not exist.");
}
this->file = CreateFileA(filename, GENERIC_READ, 0, NULL, OPEN_ALWAYS, FILE_ATTRIBUTE_NORMAL, NULL);
if (this->file == INVALID_HANDLE_VALUE) {
LOG4CPLUS_ERROR(logger, "Error in CreateFileA(" << filename << "): Probably, we may not read this file.");
throw exceptions::FileIoException("MappedFile Error in CreateFileA(): Probably, we may not read this file.");
}
this->mapping = CreateFileMappingA(this->file, NULL, PAGE_READONLY, (DWORD)(st.st_size >> 32), (DWORD)st.st_size, NULL);
if (this->mapping == NULL) {
CloseHandle(this->file);
LOG4CPLUS_ERROR(logger, "Error in CreateFileMappingA(" << filename << ").");
throw exceptions::FileIoException("MappedFile Error in CreateFileMappingA().");
}
this->data = static_cast<char*>(MapViewOfFile(this->mapping, FILE_MAP_READ, 0, 0, this->st.st_size));
if (this->data == NULL) {
CloseHandle(this->mapping);
CloseHandle(this->file);
LOG4CPLUS_ERROR(logger, "Error in MapViewOfFile(" << filename << ").");
throw exceptions::FileIoException("MappedFile Error in MapViewOfFile().");
}
this->dataend = this->data + this->st.st_size;
#endif
}
/*!
* Will unmap the data and close the file.
*/
MappedFile::~MappedFile() {
#if defined LINUX || defined MACOSX
munmap(this->data, this->st.st_size);
close(this->file);
#elif defined WINDOWS
CloseHandle(this->mapping);
CloseHandle(this->file);
#endif
}
} // namespace parser } // namespace parser
} // namespace storm } // namespace storm

199
src/parser/Parser.h

@ -16,161 +16,78 @@
namespace storm { namespace storm {
/*!
* @brief Contains all file parser and helper classes.
*
* This namespace contains everything needed to load data files (like
* atomic propositions, transition systems, formulas, ...) including
* methods for efficient file access (see MappedFile).
*/
namespace parser {
struct RewardMatrixInformationStruct {
RewardMatrixInformationStruct() : rowCount(0), columnCount(0), nondeterministicChoiceIndices(nullptr) {
// Intentionally left empty.
}
RewardMatrixInformationStruct(uint_fast64_t rowCount, uint_fast64_t columnCount, std::vector<uint_fast64_t> const * const nondeterministicChoiceIndices)
: rowCount(rowCount), columnCount(columnCount), nondeterministicChoiceIndices(nondeterministicChoiceIndices) {
// Intentionally left empty.
}
uint_fast64_t rowCount;
uint_fast64_t columnCount;
std::vector<uint_fast64_t> const * const nondeterministicChoiceIndices;
};
/*!
* @brief Opens a file and maps it to memory providing a char*
* containing the file content.
*
* This class is a very simple interface to read files efficiently.
* The given file is opened and mapped to memory using mmap().
* The public member data is a pointer to the actual file content.
* Using this method, the kernel will take care of all buffering. This is
* most probably much more efficient than doing this manually.
*/
#if !defined LINUX && !defined MACOSX && !defined WINDOWS
#error Platform not supported
#endif
class MappedFile {
private:
#if defined LINUX || defined MACOSX
/*!
* @brief file descriptor obtained by open().
*/
int file;
#elif defined WINDOWS
HANDLE file;
HANDLE mapping;
#endif
#if defined LINUX
/*!
* @brief stat information about the file.
*/
struct stat64 st;
#elif defined MACOSX
/*!
* @brief stat information about the file.
*/
struct stat st;
#elif defined WINDOWS
/*!
* @brief stat information about the file.
*/
struct __stat64 st;
#endif
public:
/*!
* @brief pointer to actual file content.
*/
char* data;
/*!
* @brief pointer to end of file content.
*/
char* dataend;
/*! /*!
* @brief Constructor of MappedFile. * @brief Contains all file parsers and helper classes.
*
* This namespace contains everything needed to load data files (like
* atomic propositions, transition systems, formulas, etc.) including
* methods for efficient file access (see MappedFile).
*/ */
MappedFile(const char* filename); namespace parser {
/*! /*!
* @brief Destructor of MappedFile. * @brief Parses integer and checks, if something has been parsed.
*/ */
~MappedFile(); uint_fast64_t checked_strtol(const char* str, char** end);
};
/*!
* @brief Parses integer and checks, if something has been parsed.
*/
uint_fast64_t checked_strtol(const char* str, char** end);
/*!
* @brief Parses floating point and checks, if something has been parsed.
*/
double checked_strtod(const char* str, char** end);
/*!
* @brief Skips all non whitespace characters until the next whitespace.
*/
char* skipWord(char* buf);
/*! /*!
* @brief Skips common whitespaces in a string. * @brief Parses floating point and checks, if something has been parsed.
*/ */
char* trimWhitespaces(char* buf); double checked_strtod(const char* str, char** end);
/*! /*!
* @brief Tests whether the given file exists and is readable. * @brief Skips all non whitespace characters until the next whitespace.
*/ */
bool fileExistsAndIsReadable(const char* fileName); char* skipWord(char* buf);
/*! /*!
* @brief Enum Class Type containing all supported file endings. * @brief Skips common whitespaces in a string.
*/ */
enum class SupportedLineEndingsEnum : unsigned short { char* trimWhitespaces(char* buf);
Unsupported = 0,
SlashR,
SlashN,
SlashRN
};
/*!
* @briefs Analyzes the given file and tries to find out the used line endings.
*/
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). * @brief Tests whether the given file exists and is readable.
*/ */
char* forwardToLineEnd(char* buffer, storm::parser::SupportedLineEndingsEnum lineEndings); bool fileExistsAndIsReadable(const char* fileName);
/*! /*!
* @brief Encapsulates the usage of function @strchr to forward to the next line * @brief Enum Class Type containing all supported file endings.
*/ */
char* forwardToNextLine(char* buffer, storm::parser::SupportedLineEndingsEnum lineEndings); enum class SupportedLineEndings : unsigned short {
Unsupported = 0,
SlashR,
SlashN,
SlashRN
};
/*! /*!
* @brief Encapsulates the usage of function @sscanf to scan for the model type hint * @briefs Analyzes the given file and tries to find out the used line endings.
* @param targetBuffer The Target for the hint, should be at least 64 bytes long */
* @param buffer The Source Buffer from which the Model Hint will be read storm::parser::SupportedLineEndings findUsedLineEndings(std::string const& fileName, bool throwOnUnsupported = false);
*/ /*!
void scanForModelHint(char* targetBuffer, uint_fast64_t targetBufferSize, char const* buffer, storm::parser::SupportedLineEndingsEnum lineEndings); * @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::SupportedLineEndings lineEndings);
/*! /*!
* @brief Returns the matching Separator-String in the format of "BLANK\t\NEWLINESYMBOL(S)\0 * @brief Encapsulates the usage of function @strchr to forward to the next line
*/ */
void getMatchingSeparatorString(char* targetBuffer, uint_fast64_t targetBufferSize, storm::parser::SupportedLineEndingsEnum lineEndings); char* forwardToNextLine(char* buffer, storm::parser::SupportedLineEndings lineEndings);
} // namespace parser /*!
* @brief Encapsulates the usage of function @sscanf to scan for the model type hint
* @param targetBuffer The Target for the hint, should be at least 64 bytes long
* @param buffer The Source Buffer from which the Model Hint will be read
*/
void scanForModelHint(char* targetBuffer, uint_fast64_t targetBufferSize, char const* buffer, storm::parser::SupportedLineEndings lineEndings);
/*!
* @brief Returns the matching Separator-String in the format of "BLANK\t\NEWLINESYMBOL(S)\0
*/
void getMatchingSeparatorString(char* targetBuffer, uint_fast64_t targetBufferSize, storm::parser::SupportedLineEndings lineEndings);
} // namespace parser
} // namespace storm } // namespace storm
#endif /* STORM_PARSER_PARSER_H_ */ #endif /* STORM_PARSER_PARSER_H_ */

1
src/parser/SparseStateRewardParser.cpp

@ -12,6 +12,7 @@
#include "src/exceptions/WrongFormatException.h" #include "src/exceptions/WrongFormatException.h"
#include "src/exceptions/FileIoException.h" #include "src/exceptions/FileIoException.h"
#include "src/parser/Parser.h" #include "src/parser/Parser.h"
#include "src/parser/MappedFile.h"
#include "log4cplus/logger.h" #include "log4cplus/logger.h"
#include "log4cplus/loggingmacros.h" #include "log4cplus/loggingmacros.h"
extern log4cplus::Logger logger; extern log4cplus::Logger logger;

|||||||
100:0
Loading…
Cancel
Save