sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Removed duplicated code in DeterministicSparseTransitionParser while still keeping it readable and the interface intact. 

Next up: Refactor the Nondeterministic*Parser.


Former-commit-id: 108eea60a0
tempestpy_adaptions
masawei 11 years ago
parent
4245b3c4e3
commit
8adee3629b
5 changed files with 166 additions and 202 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 325
      src/parser/DeterministicSparseTransitionParser.cpp
  2. 36
      src/parser/DeterministicSparseTransitionParser.h
  3. 3
      src/parser/MarkovAutomatonParser.cpp
  4. 2
      src/parser/MarkovAutomatonParser.h
  5. 2
      src/parser/MarkovAutomatonSparseTransitionParser.h

325
src/parser/DeterministicSparseTransitionParser.cpp
View File

@ -28,19 +28,18 @@ namespace storm {
namespace parser {
/*!
* @brief Perform first pass through the file and obtain number of
* non-zero cells and maximum node id.
*
* This method does the first pass through the .tra file and computes
* the number of non-zero elements.
* It also calculates the maximum node id and stores it in maxnode.
*
* @return The number of non-zero elements
* @param buf Data to scan. Is expected to be some char array.
* @param maxnode Is set to highest id of all nodes.
*/
storm::storage::SparseMatrix<double> DeterministicSparseTransitionParser::parseDeterministicTransitions(std::string const& filename, bool insertDiagonalEntriesIfMissing) {
return DeterministicSparseTransitionParser::parse(filename, false, insertDiagonalEntriesIfMissing);
}
storm::storage::SparseMatrix<double> DeterministicSparseTransitionParser::parseDeterministicTransitionRewards(std::string const& filename, RewardMatrixInformationStruct const& rewardMatrixInformation) {
return DeterministicSparseTransitionParser::parse(filename, true, false, rewardMatrixInformation);
}
DeterministicSparseTransitionParser::FirstPassResult DeterministicSparseTransitionParser::firstPass(char* buf, SupportedLineEndingsEnum lineEndings, bool insertDiagonalEntriesIfMissing) {
DeterministicSparseTransitionParser::FirstPassResult result;
// Skip the format hint if it is there.
@ -107,220 +106,156 @@ DeterministicSparseTransitionParser::FirstPassResult DeterministicSparseTransiti
return result;
}
/*!
* 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.
*/
storm::storage::SparseMatrix<double> DeterministicSparseTransitionParser::parseDeterministicTransitions(std::string const& filename, bool insertDiagonalEntriesIfMissing) {
storm::storage::SparseMatrix<double> DeterministicSparseTransitionParser::parse(std::string const& filename, bool rewardFile, bool insertDiagonalEntriesIfMissing, 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::FileIoException() << "The supplied Transition input file \"" << filename << "\" does not exist or is not readable by this process.";
}
setlocale(LC_NUMERIC, "C");
// 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. count entries that are not zero.
DeterministicSparseTransitionParser::FirstPassResult firstPass = DeterministicSparseTransitionParser::firstPass(file.data, lineEndings, insertDiagonalEntriesIfMissing);
LOG4CPLUS_INFO(logger, "First pass on " << filename << " shows " << firstPass.numberOfNonzeroEntries << " NonZeros.");
// If first pass returned zero, the file format was wrong.
if (firstPass.numberOfNonzeroEntries == 0) {
LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": empty or erroneous file format.");
throw storm::exceptions::WrongFormatException();
}
// Perform second pass.
// Skip the format hint if it is there.
buf = trimWhitespaces(buf);
if(buf[0] != '0') {
buf = storm::parser::forwardToNextLine(buf, lineEndings);
}
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.";
}
// Creating matrix builder here.
// The number of non-zero elements is computed by firstPass().
// The contents are inserted during the readout of the file, below.
// The actual matrix will be build once all contents are inserted.
storm::storage::SparseMatrixBuilder<double> resultMatrix(firstPass.highestStateIndex + 1, firstPass.highestStateIndex + 1, firstPass.numberOfNonzeroEntries);
// Find out about the used line endings.
SupportedLineEndingsEnum lineEndings = findUsedLineEndings(filename, true);
uint_fast64_t row, col, lastRow = 0;
double val;
bool fixDeadlocks = storm::settings::Settings::getInstance()->isSet("fixDeadlocks");
bool hadDeadlocks = false;
bool rowHadDiagonalEntry = false;
// Open file.
MappedFile file(filename.c_str());
char* buf = file.data;
// Perform first pass, i.e. count entries that are not zero.
// 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.
while (buf[0] != '\0') {
DeterministicSparseTransitionParser::FirstPassResult firstPass = DeterministicSparseTransitionParser::firstPass(file.data, lineEndings, insertDiagonalEntriesIfMissing);
// Read next transition.
row = checked_strtol(buf, &buf);
col = checked_strtol(buf, &buf);
val = checked_strtod(buf, &buf);
LOG4CPLUS_INFO(logger, "First pass on " << filename << " shows " << firstPass.numberOfNonzeroEntries << " NonZeros.");
// 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 << "\".");
// If first pass returned zero, the file format was wrong.
if (firstPass.numberOfNonzeroEntries == 0) {
LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": empty or erroneous file format.");
throw storm::exceptions::WrongFormatException();
}
// 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.
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;
}
// Perform second pass.
if (col == row) {
rowHadDiagonalEntry = true;
// Skip the format hint if it is there.
buf = trimWhitespaces(buf);
if(buf[0] != '0') {
buf = storm::parser::forwardToNextLine(buf, lineEndings);
}
if (col > row && !rowHadDiagonalEntry) {
if (insertDiagonalEntriesIfMissing) {
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)");
if(rewardFile) {
// 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.");
throw storm::exceptions::WrongFormatException() << "Reward matrix has more rows or columns than transition matrix.";
} else {
LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << row << " has no transition to itself.");
// 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;
}
rowHadDiagonalEntry = true;
}
resultMatrix.addNextValue(row, col, val);
buf = trimWhitespaces(buf);
}
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.");
}
}
// 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.";
return resultMatrix.build();
}
/*!
* 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.
*/
storm::storage::SparseMatrix<double> DeterministicSparseTransitionParser::parseDeterministicTransitionRewards(std::string const& filename, 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::FileIoException() << "The supplied Transition input file \"" << filename << "\" does not exist or is not readable by this process.";
}
// 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);
// Find out about the used line endings.
SupportedLineEndingsEnum lineEndings = findUsedLineEndings(filename, true);
uint_fast64_t row, col, lastRow = 0;
double val;
bool fixDeadlocks = storm::settings::Settings::getInstance()->isSet("fixDeadlocks");
bool hadDeadlocks = false;
bool rowHadDiagonalEntry = false;
// Open file.
MappedFile file(filename.c_str());
char* buf = file.data;
// Perform first pass, i.e. count entries that are not zero.
// 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.
DeterministicSparseTransitionParser::FirstPassResult firstPass = DeterministicSparseTransitionParser::firstPass(file.data, lineEndings, false);
// Different parsing routines for transition systems and transition rewards.
if(rewardFile) {
while (buf[0] != '\0') {
LOG4CPLUS_INFO(logger, "First pass on " << filename << " shows " << firstPass.numberOfNonzeroEntries << " NonZeros.");
// If first pass returned zero, the file format was wrong.
if (firstPass.numberOfNonzeroEntries == 0) {
LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": empty or erroneous file format.");
throw storm::exceptions::WrongFormatException();
}
// Perform second pass.
// Skip the format hint if it is there.
buf = trimWhitespaces(buf);
if(buf[0] != '0') {
buf = storm::parser::forwardToNextLine(buf, lineEndings);
}
// Read next transition.
row = checked_strtol(buf, &buf);
col = checked_strtol(buf, &buf);
val = checked_strtod(buf, &buf);
// 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.");
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;
}
resultMatrix.addNextValue(row, col, val);
buf = trimWhitespaces(buf);
}
} 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();
}
// 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.
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;
}
// Creating matrix builder here.
// The number of non-zero elements is computed by firstPass().
// The contents are inserted during the readout of the file, below.
// The actual matrix will be build once all contents are inserted.
storm::storage::SparseMatrixBuilder<double> resultMatrix(firstPass.highestStateIndex + 1, firstPass.highestStateIndex + 1, firstPass.numberOfNonzeroEntries);
if (col == row) {
rowHadDiagonalEntry = true;
}
uint_fast64_t row, col;
double val;
if (col > row && !rowHadDiagonalEntry) {
if (insertDiagonalEntriesIfMissing) {
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;
}
// 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.
while (buf[0] != '\0') {
resultMatrix.addNextValue(row, col, val);
buf = trimWhitespaces(buf);
}
// Read next transition.
row = checked_strtol(buf, &buf);
col = checked_strtol(buf, &buf);
val = checked_strtod(buf, &buf);
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.");
}
}
resultMatrix.addNextValue(row, col, val);
buf = trimWhitespaces(buf);
}
// 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.";
}
return resultMatrix.build();
// Finally, build the actual matrix and return it.
return resultMatrix.build();
}
} // namespace parser

36
src/parser/DeterministicSparseTransitionParser.h
View File

@ -27,21 +27,35 @@ public:
};
/*!
* @brief Load a deterministic transition system from file and create a
* sparse adjacency matrix whose entries represent the weights of the edges
* Load a deterministic transition system from file and create a
* sparse adjacency matrix whose entries represent the weights of the edges.
*
* @param filename The path of file to be parsed.
* @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.
*/
static storm::storage::SparseMatrix<double> parseDeterministicTransitions(std::string const& filename, bool insertDiagonalEntriesIfMissing = true);
/*!
* @brief Load the transition rewards for a deterministic transition system from file and create a
* sparse adjacency matrix whose entries represent the rewards of the respective transitions.
* Load the transition rewards for a deterministic transition system from file and create a
* sparse adjacency matrix whose entries represent the rewards of the respective transitions.
*/
/*!
* Load the transition rewards for a deterministic transition system from file and create a
* sparse adjacency matrix whose entries represent the rewards of the respective transitions.
*
* @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.
* @return A SparseMatrix containing the parsed transition rewards.
*/
static storm::storage::SparseMatrix<double> parseDeterministicTransitionRewards(std::string const& filename, RewardMatrixInformationStruct const& rewardMatrixInformation);
private:
/*
* Performs the first pass on the input pointed to by the given buffer.
* Performs the first pass on the input pointed to by the given buffer to obtain the number of
* transitions and the maximum node id.
*
* @param buffer The buffer that cointains the input.
* @param lineEndings The line endings that are to be used while parsing.
@ -50,6 +64,18 @@ private:
*/
static FirstPassResult firstPass(char* buffer, SupportedLineEndingsEnum lineEndings, bool insertDiagonalEntriesIfMissing = true);
/*
* 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 storm::storage::SparseMatrix<double> parse(std::string const& filename, bool rewardFile, bool insertDiagonalEntriesIfMissing = false, RewardMatrixInformationStruct const& rewardMatrixInformation = nullptr);
};
} // namespace parser

3
src/parser/MarkovAutomatonParser.cpp
View File

@ -18,16 +18,19 @@ storm::models::MarkovAutomaton<double> MarkovAutomatonParser::parseMarkovAutomat
// Parse the state labeling.
storm::models::AtomicPropositionsLabeling resultLabeling(storm::parser::AtomicPropositionLabelingParser(transitionMatrix.getColumnCount(), labelingFilename));
// If given, parse the state rewards file.
boost::optional<std::vector<double>> stateRewards;
if (stateRewardFilename != "") {
stateRewards.reset(storm::parser::SparseStateRewardParser::parseSparseStateReward(transitionMatrix.getColumnCount(), stateRewardFilename));
}
// Since Markov Automata do not support transition rewards no path should be given here.
if (transitionRewardFilename != "") {
LOG4CPLUS_ERROR(logger, "Transition rewards are unsupported for Markov automata.");
throw storm::exceptions::WrongFormatException() << "Transition rewards are unsupported for Markov automata.";
}
// Put the pieces together to generate the Markov Automaton.
storm::models::MarkovAutomaton<double> resultingAutomaton(std::move(transitionMatrix), std::move(resultLabeling), std::move(transitionResult.nondeterministicChoiceIndices), std::move(transitionResult.markovianStates), std::move(transitionResult.exitRates), std::move(stateRewards), boost::optional<storm::storage::SparseMatrix<double>>(), boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>());
return resultingAutomaton;

2
src/parser/MarkovAutomatonParser.h
View File

@ -20,7 +20,7 @@ public:
* @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 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. This should be empty as transition rewards are not supported by Markov Automata.
*/
static storm::models::MarkovAutomaton<double> parseMarkovAutomaton(std::string const& transitionsFilename, std::string const& labelingFilename, std::string const& stateRewardFilename, std::string const& transitionRewardFilename);
};

2
src/parser/MarkovAutomatonSparseTransitionParser.h
View File

@ -30,7 +30,7 @@ public:
// The highest state index that appears in the model.
uint_fast64_t highestStateIndex;
// The total number of choices in the model.
// The total number of nondeterministic choices in the model.
uint_fast64_t numberOfChoices;
};

Write Preview
Loading…
Cancel
Save