Browse Source

some fixes to new parser, calculate maximum node number manually

tempestpy_adaptions
gereon 12 years ago
parent
commit
ea8504a84e
  1. 7
      src/parser/readLabFile.cpp
  2. 17
      src/parser/readTraFile.cpp

7
src/parser/readLabFile.cpp

@ -60,6 +60,7 @@ mrmc::models::AtomicPropositionsLabeling * readLabFile(int node_count, const cha
else cnt = 1; else cnt = 1;
} while (cnt > 0); } while (cnt > 0);
printf("node count %d\n", node_count);
mrmc::models::AtomicPropositionsLabeling* result = new mrmc::models::AtomicPropositionsLabeling(node_count, proposition_count); mrmc::models::AtomicPropositionsLabeling* result = new mrmc::models::AtomicPropositionsLabeling(node_count, proposition_count);
char proposition[128]; char proposition[128];
buf = file.data; buf = file.data;
@ -79,18 +80,20 @@ mrmc::models::AtomicPropositionsLabeling * readLabFile(int node_count, const cha
buf += 4; buf += 4;
uint_fast32_t node; uint_fast32_t node;
while (1) {
do {
node = strtol(buf, &buf, 10); node = strtol(buf, &buf, 10);
while (*buf != '\0') { while (*buf != '\0') {
cnt = strcspn(buf, sep); cnt = strcspn(buf, sep);
if (cnt == 0) buf++; if (cnt == 0) buf++;
else break; else break;
} }
if (cnt > 0) {
strncpy(proposition, buf, cnt); strncpy(proposition, buf, cnt);
proposition[cnt] = '\0'; proposition[cnt] = '\0';
result->addAtomicPropositionToState(proposition, node); result->addAtomicPropositionToState(proposition, node);
buf += cnt;
} }
buf += cnt;
} while (cnt > 0);
return result; return result;
} }

17
src/parser/readTraFile.cpp

@ -52,7 +52,7 @@ char* skipWS(char* buf)
* @return The number of non-zero elements that are not on the diagonal * @return The number of non-zero elements that are not on the diagonal
* @param buf Data to scan. Is expected to be some char array. * @param buf Data to scan. Is expected to be some char array.
*/ */
static uint_fast32_t makeFirstPass(char* buf)
static uint_fast32_t makeFirstPass(char* buf, uint_fast32_t &maxnode)
{ {
uint_fast32_t non_zero = 0; uint_fast32_t non_zero = 0;
@ -70,12 +70,15 @@ static uint_fast32_t makeFirstPass(char* buf)
/*! /*!
* check all transitions for non-zero diagonal entrys * check all transitions for non-zero diagonal entrys
*/ */
unsigned int row, col;
uint_fast32_t row, col;
double val; double val;
maxnode = 0;
while (1) while (1)
{ {
row = strtol(buf, &buf, 10); row = strtol(buf, &buf, 10);
if (row > maxnode) maxnode = row;
col = strtol(buf, &buf, 10); col = strtol(buf, &buf, 10);
if (col > maxnode) maxnode = col;
val = strtod(buf, &buf); val = strtod(buf, &buf);
if (val == 0.0) break; if (val == 0.0) break;
if (row == col) non_zero--; if (row == col) non_zero--;
@ -104,7 +107,8 @@ sparse::StaticSparseMatrix<double> * readTraFile(const char * filename) {
/*! /*!
* perform first pass, i.e. count entries that are not zero and not on the diagonal * perform first pass, i.e. count entries that are not zero and not on the diagonal
*/ */
uint_fast32_t non_zero = makeFirstPass(file.data);
uint_fast32_t maxnode;
uint_fast32_t non_zero = makeFirstPass(file.data, maxnode);
if (non_zero == 0) if (non_zero == 0)
{ {
/*! /*!
@ -120,20 +124,19 @@ sparse::StaticSparseMatrix<double> * readTraFile(const char * filename) {
* from here on, we already know that the file header is correct * from here on, we already know that the file header is correct
*/ */
char* buf = file.data; char* buf = file.data;
uint_fast32_t rows;
sparse::StaticSparseMatrix<double> *sp = NULL; sparse::StaticSparseMatrix<double> *sp = NULL;
/*! /*!
* read file header, extract number of states * read file header, extract number of states
*/ */
buf += 7; // skip "STATES " buf += 7; // skip "STATES "
rows = strtol(buf, &buf, 10);
strtol(buf, &buf, 10);
buf = skipWS(buf); buf = skipWS(buf);
buf += 12; // skip "TRANSITIONS " buf += 12; // skip "TRANSITIONS "
strtol(buf, &buf, 10); strtol(buf, &buf, 10);
pantheios::log_DEBUG("Creating matrix with ", pantheios::log_DEBUG("Creating matrix with ",
pantheios::integer(rows), " rows and ",
pantheios::integer(maxnode + 1), " maxnodes and ",
pantheios::integer(non_zero), " Non-Zero-Elements"); pantheios::integer(non_zero), " Non-Zero-Elements");
/*! /*!
@ -141,7 +144,7 @@ sparse::StaticSparseMatrix<double> * readTraFile(const char * filename) {
* Memory for diagonal elements is automatically allocated, hence only the number of non-diagonal * Memory for diagonal elements is automatically allocated, hence only the number of non-diagonal
* non-zero elements has to be specified (which is non_zero, computed by make_first_pass) * non-zero elements has to be specified (which is non_zero, computed by make_first_pass)
*/ */
sp = new sparse::StaticSparseMatrix<double>(rows);
sp = new sparse::StaticSparseMatrix<double>(maxnode + 1);
if (sp == NULL) if (sp == NULL)
{ {
/*! /*!

Loading…
Cancel
Save