Browse Source

fixing test for deadlock nodes in parsers

main
gereon 13 years ago
parent
commit
0992df5c66
  1. 12
      src/parser/DeterministicSparseTransitionParser.cpp
  2. 2
      src/parser/DeterministicSparseTransitionParser.h
  3. 14
      src/parser/NonDeterministicSparseTransitionParser.cpp
  4. 2
      src/parser/NonDeterministicSparseTransitionParser.h

12
src/parser/DeterministicSparseTransitionParser.cpp

@ -44,7 +44,7 @@ namespace parser {
* @param buf Data to scan. Is expected to be some char array. * @param buf Data to scan. Is expected to be some char array.
* @param maxnode Is set to highest id of all nodes. * @param maxnode Is set to highest id of all nodes.
*/ */
uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, uint_fast64_t& maxnode) { uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, int_fast64_t& maxnode) {
uint_fast64_t non_zero = 0; uint_fast64_t non_zero = 0;
/* /*
@ -68,7 +68,7 @@ uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, uint_fas
/* /*
* Check all transitions for non-zero diagonal entrys. * Check all transitions for non-zero diagonal entrys.
*/ */
uint_fast64_t row, lastrow = 0, col; int_fast64_t row, lastrow = -1, col;
double val; double val;
maxnode = 0; maxnode = 0;
while (buf[0] != '\0') { while (buf[0] != '\0') {
@ -89,7 +89,7 @@ uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, uint_fas
* anyway) or add a self-loop (in this case, we'll need the * anyway) or add a self-loop (in this case, we'll need the
* additional transition). * additional transition).
*/ */
if (lastrow < row-1) non_zero += row - lastrow - 1; if (lastrow < row - 1) non_zero += row - lastrow - 1;
lastrow = row; lastrow = row;
/* /*
* Read probability of this transition. * Read probability of this transition.
@ -132,7 +132,7 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st
/* /*
* Perform first pass, i.e. count entries that are not zero. * Perform first pass, i.e. count entries that are not zero.
*/ */
uint_fast64_t maxnode; int_fast64_t maxnode;
uint_fast64_t non_zero = this->firstPass(file.data, maxnode); uint_fast64_t non_zero = this->firstPass(file.data, maxnode);
/* /*
* If first pass returned zero, the file format was wrong. * If first pass returned zero, the file format was wrong.
@ -170,7 +170,7 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st
} }
this->matrix->initialize(non_zero); this->matrix->initialize(non_zero);
uint_fast64_t row, lastrow = 0, col; int_fast64_t row, lastrow = -1, col;
double val; double val;
bool fixDeadlocks = storm::settings::instance()->isSet("fix-deadlocks"); bool fixDeadlocks = storm::settings::instance()->isSet("fix-deadlocks");
bool hadDeadlocks = false; bool hadDeadlocks = false;
@ -192,7 +192,7 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st
* Check if we skipped a node, i.e. if a node does not have any * Check if we skipped a node, i.e. if a node does not have any
* outgoing transitions. * outgoing transitions.
*/ */
for (uint_fast64_t node = lastrow + 1; node < row; node++) { for (int_fast64_t node = lastrow + 1; node < row; node++) {
hadDeadlocks = true; hadDeadlocks = true;
if (fixDeadlocks) { if (fixDeadlocks) {
this->matrix->addNextValue(node, node, 1); this->matrix->addNextValue(node, node, 1);

2
src/parser/DeterministicSparseTransitionParser.h

@ -26,7 +26,7 @@ class DeterministicSparseTransitionParser : public Parser {
private: private:
std::shared_ptr<storm::storage::SparseMatrix<double>> matrix; std::shared_ptr<storm::storage::SparseMatrix<double>> matrix;
uint_fast64_t firstPass(char* buf, uint_fast64_t &maxnode); uint_fast64_t firstPass(char* buf, int_fast64_t &maxnode);
}; };

14
src/parser/NonDeterministicSparseTransitionParser.cpp

@ -49,7 +49,7 @@ namespace parser {
* @param maxnode Is set to highest id of all nodes. * @param maxnode Is set to highest id of all nodes.
* @return The number of non-zero elements. * @return The number of non-zero elements.
*/ */
uint_fast64_t NonDeterministicSparseTransitionParser::firstPass(char* buf, uint_fast64_t& choices, uint_fast64_t& maxnode) { uint_fast64_t NonDeterministicSparseTransitionParser::firstPass(char* buf, uint_fast64_t& choices, int_fast64_t& maxnode) {
/* /*
* Check file header and extract number of transitions. * Check file header and extract number of transitions.
*/ */
@ -77,8 +77,8 @@ uint_fast64_t NonDeterministicSparseTransitionParser::firstPass(char* buf, uint_
/* /*
* Read all transitions. * Read all transitions.
*/ */
uint_fast64_t source, target; int_fast64_t source, target;
uint_fast64_t lastsource = 0; int_fast64_t lastsource = -1;
uint_fast64_t nonzero = 0; uint_fast64_t nonzero = 0;
double val; double val;
choices = 0; choices = 0;
@ -97,6 +97,7 @@ uint_fast64_t NonDeterministicSparseTransitionParser::firstPass(char* buf, uint_
choices++; choices++;
if (source > lastsource + 1) { if (source > lastsource + 1) {
nonzero += source - lastsource - 1; nonzero += source - lastsource - 1;
choices += source - lastsource - 1;
parsed_nonzero += source - lastsource - 1; parsed_nonzero += source - lastsource - 1;
} }
lastsource = source; lastsource = source;
@ -169,7 +170,8 @@ NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(s
/* /*
* 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.
*/ */
uint_fast64_t maxnode, choices; int_fast64_t maxnode;
uint_fast64_t choices;
uint_fast64_t nonzero = this->firstPass(file.data, choices, maxnode); uint_fast64_t nonzero = this->firstPass(file.data, choices, maxnode);
/* /*
@ -217,7 +219,7 @@ NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(s
/* /*
* Parse file content. * Parse file content.
*/ */
uint_fast64_t source, target, lastsource = 0; int_fast64_t source, target, lastsource = -1;
uint_fast64_t curRow = 0; uint_fast64_t curRow = 0;
std::string choice; std::string choice;
double val; double val;
@ -240,7 +242,7 @@ NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(s
* outgoing transitions. If so, insert a self-loop. * outgoing transitions. If so, insert a self-loop.
* Also add self-loops to rowMapping. * Also add self-loops to rowMapping.
*/ */
for (uint_fast64_t node = lastsource + 1; node < source; node++) { for (int_fast64_t node = lastsource + 1; node < source; node++) {
hadDeadlocks = true; hadDeadlocks = true;
if (fixDeadlocks) { if (fixDeadlocks) {
this->rowMapping->insert(RowMapping::value_type(curRow, std::pair<uint_fast64_t, std::string>(node, ""))); this->rowMapping->insert(RowMapping::value_type(curRow, std::pair<uint_fast64_t, std::string>(node, "")));

2
src/parser/NonDeterministicSparseTransitionParser.h

@ -35,7 +35,7 @@ class NonDeterministicSparseTransitionParser : public Parser {
std::shared_ptr<storm::storage::SparseMatrix<double>> matrix; std::shared_ptr<storm::storage::SparseMatrix<double>> matrix;
std::shared_ptr<RowMapping> rowMapping; std::shared_ptr<RowMapping> rowMapping;
uint_fast64_t firstPass(char* buf, uint_fast64_t& choices, uint_fast64_t& maxnode); uint_fast64_t firstPass(char* buf, uint_fast64_t& choices, int_fast64_t& maxnode);
}; };

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