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

The DeterministicSparseTransitionParser.cpp was still broken, rewrote it in a simpler and more convenient way. 

All Deterministic Tests complete now.
tempestpy_adaptions
PBerger 12 years ago
parent
02cb1a2418
commit
a598d3751c
3 changed files with 91 additions and 86 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. 123
      src/parser/DeterministicSparseTransitionParser.cpp
  2. 2
      test/parser/ParseDtmcTest.cpp
  3. 52
      test/parser/ReadTraFileTest.cpp

123
src/parser/DeterministicSparseTransitionParser.cpp
View File

@ -46,7 +46,7 @@ namespace parser {
*/
uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, int_fast64_t& maxnode) {
uint_fast64_t nonZeroEntryCount = 0;
uint_fast64_t inputFileNonZeroEntryCount = 0;
/*
* Check file header and extract number of transitions.
*/
@ -63,12 +63,13 @@ uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, int_fast
return 0;
}
buf += 12; // skip "TRANSITIONS "
if ((nonZeroEntryCount = strtol(buf, &buf, 10)) == 0) return 0;
if ((inputFileNonZeroEntryCount = strtol(buf, &buf, 10)) == 0) return 0;
/*
* Check all transitions for non-zero diagonal entries and deadlock states.
*/
int_fast64_t row, lastRow = -1, col;
uint_fast64_t readTransitionCount = 0;
bool rowHadDiagonalEntry = false;
double val;
maxnode = 0;
@ -79,24 +80,24 @@ uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, int_fast
row = checked_strtol(buf, &buf);
col = checked_strtol(buf, &buf);
/*
* If we have switched to the next row, we need to clear the information about
* the diagonal entry.
*/
if (row != lastRow) {
/*
* If the last row did have transitions, but no diagonal element, we need to insert
* it as well.
*/
if (!rowHadDiagonalEntry && lastRow != -1) {
++nonZeroEntryCount;
}
rowHadDiagonalEntry = false;
}
if (lastRow != row) {
if ((lastRow != -1) && (!rowHadDiagonalEntry)) {
++nonZeroEntryCount;
rowHadDiagonalEntry = true;
}
for (int_fast64_t skippedRow = lastRow + 1; skippedRow < row; ++skippedRow) {
++nonZeroEntryCount;
}
lastRow = row;
rowHadDiagonalEntry = false;
}
if (row == col) {
rowHadDiagonalEntry = true;
}
if (col == row) {
rowHadDiagonalEntry = true;
} else if (col > row && !rowHadDiagonalEntry) {
rowHadDiagonalEntry = true;
++nonZeroEntryCount;
}
/*
* Check if one is larger than the current maximum id.
@ -104,17 +105,6 @@ uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, int_fast
if (row > maxnode) maxnode = row;
if (col > maxnode) maxnode = col;
/*
* Check if a node was skipped, i.e. if a node has no outgoing
* transitions. If so, increase non_zero, as the second pass will
* either throw an exception (in this case, it doesn't matter
* anyway) or add a self-loop (in this case, we'll need the
* additional transition).
*/
if (lastRow < row - 1) {
nonZeroEntryCount += row - lastRow - 1;
}
lastRow = row;
/*
* Read probability of this transition.
* Check, if the value is a probability, i.e. if it is between 0 and 1.
@ -124,6 +114,8 @@ uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, int_fast
LOG4CPLUS_ERROR(logger, "Expected a positive probability but got \"" << val << "\".");
return 0;
}
++nonZeroEntryCount;
++readTransitionCount;
buf = trimWhitespaces(buf);
}
@ -131,6 +123,11 @@ uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, int_fast
++nonZeroEntryCount;
}
if (inputFileNonZeroEntryCount != readTransitionCount) {
LOG4CPLUS_ERROR(logger, "Input File TRANSITIONS line stated " << inputFileNonZeroEntryCount << " but there were " << readTransitionCount << " transitions afterwards.");
return 0;
}
return nonZeroEntryCount;
}
@ -162,6 +159,9 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st
*/
int_fast64_t maxStateId;
uint_fast64_t nonZeroEntryCount = this->firstPass(file.data, maxStateId);
LOG4CPLUS_INFO(logger, "First pass on " << filename << " shows " << nonZeroEntryCount << " NonZeros.");
/*
* If first pass returned zero, the file format was wrong.
*/
@ -217,56 +217,55 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st
col = checked_strtol(buf, &buf);
val = checked_strtod(buf, &buf);
if (row != lastRow) {
/*
* If the previous row did not have a diagonal entry, we need to insert it.
*/
if (!rowHadDiagonalEntry && lastRow != -1) {
this->matrix->addNextValue(lastRow, lastRow, storm::utility::constGetZero<double>());
if (lastRow != row) {
if ((lastRow != -1) && (!rowHadDiagonalEntry)) {
if (insertDiagonalEntriesIfMissing) {
this->matrix->addNextValue(lastRow, lastRow, storm::utility::constGetZero<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;
}
rowHadDiagonalEntry = false;
}
/*
* Check if we skipped a state entirely, i.e. a state does not have any
* outgoing transitions.
*/
if ((lastRow + 1) < row) {
for (int_fast64_t state = lastRow + 1; state < row; ++state) {
for (int_fast64_t skippedRow = lastRow + 1; skippedRow < row; ++skippedRow) {
hadDeadlocks = true;
if (fixDeadlocks) {
this->matrix->addNextValue(state, state, storm::utility::constGetOne<double>());
LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << state << " has no outgoing transitions. A self-loop was inserted.");
this->matrix->addNextValue(skippedRow, skippedRow, storm::utility::constGetOne<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 " << state << " has no outgoing transitions.");
LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": state " << skippedRow << " has no outgoing transitions.");
// FIXME Why no exception at this point? This will break the App.
}
}
lastRow = row;
rowHadDiagonalEntry = false;
}
// Insert the missing diagonal value here, because the input skipped it.
if (col > row && !rowHadDiagonalEntry) {
if (col == row) {
rowHadDiagonalEntry = true;
} else if (col > row && !rowHadDiagonalEntry) {
rowHadDiagonalEntry = true;
if (insertDiagonalEntriesIfMissing) {
this->matrix->addNextValue(row, row, storm::utility::constGetZero<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;
}
/*
* Check if the transition is a self-loop
*/
if (row == col) {
rowHadDiagonalEntry = true;
}
lastRow = row;
this->matrix->addNextValue(row, col, val);
buf = trimWhitespaces(buf);
}
if (!rowHadDiagonalEntry) {
this->matrix->addNextValue(lastRow, lastRow, storm::utility::constGetZero<double>());
if (insertDiagonalEntriesIfMissing) {
this->matrix->addNextValue(lastRow, lastRow, storm::utility::constGetZero<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 (!fixDeadlocks && hadDeadlocks) throw storm::exceptions::WrongFileFormatException() << "Some of the nodes had deadlocks. You can use --fix-deadlocks to insert self-loops on the fly.";

2
test/parser/ParseDtmcTest.cpp
View File

@ -12,7 +12,7 @@
#include "src/utility/IoUtility.h"
TEST(ParseDtmcTest, parseAndOutput) {
storm::parser::DeterministicModelParser* dtmcParser;
storm::parser::DeterministicModelParser* dtmcParser = nullptr;
ASSERT_NO_THROW(dtmcParser = new storm::parser::DeterministicModelParser(
STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/pctl_general_input_01.tra",
STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/pctl_general_input_01.lab"));

52
test/parser/ReadTraFileTest.cpp
View File

@ -22,45 +22,51 @@ TEST(ReadTraFileTest, NonExistingFileTest) {
/* The following test case is based on one of the original STORM test cases
*/
TEST(ReadTraFileTest, ParseFileTest1) {
storm::parser::DeterministicSparseTransitionParser* parser;
storm::parser::DeterministicSparseTransitionParser* parser = nullptr;
ASSERT_NO_THROW(parser = new storm::parser::DeterministicSparseTransitionParser(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/csl_general_input_01.tra"));
std::shared_ptr<storm::storage::SparseMatrix<double>> result = parser->getMatrix();
if (result != NULL) {
double val = 0;
ASSERT_TRUE(result->getValue(1,1,&val));
ASSERT_EQ(val,0.080645161290322580645161290322581);
ASSERT_TRUE(result->getValue(0, 0, &val));
ASSERT_EQ(val, 0.0);
ASSERT_TRUE(result->getValue(1,2,&val));
ASSERT_EQ(val,0.080645161290322580645161290322581);
ASSERT_TRUE(result->getValue(0, 1, &val));
ASSERT_EQ(val, 1.0);
ASSERT_TRUE(result->getValue(1, 1, &val));
ASSERT_EQ(val, 0.080645161290322580645161290322581);
ASSERT_TRUE(result->getValue(1, 2, &val));
ASSERT_EQ(val, 0.080645161290322580645161290322581);
//Transition 1->3 was not set in the file, so it is not to appear in the matrix!
ASSERT_FALSE(result->getValue(1,3,&val));
ASSERT_EQ(val,0);
ASSERT_FALSE(result->getValue(1, 3, &val));
ASSERT_EQ(val, 0);
ASSERT_TRUE(result->getValue(2,1,&val));
ASSERT_EQ(val,0.04032258064516129032258064516129);
ASSERT_TRUE(result->getValue(2, 1, &val));
ASSERT_EQ(val, 0.04032258064516129032258064516129);
ASSERT_TRUE(result->getValue(2,2,&val));
ASSERT_EQ(val,0.04032258064516129032258064516129);
ASSERT_TRUE(result->getValue(2, 2, &val));
ASSERT_EQ(val, 0.04032258064516129032258064516129);
ASSERT_TRUE(result->getValue(2,3,&val));
ASSERT_EQ(val,0.04032258064516129032258064516129);
ASSERT_TRUE(result->getValue(2, 3, &val));
ASSERT_EQ(val, 0.04032258064516129032258064516129);
ASSERT_TRUE(result->getValue(2,4,&val));
ASSERT_EQ(val,0.04032258064516129032258064516129);
ASSERT_TRUE(result->getValue(2, 4, &val));
ASSERT_EQ(val, 0.04032258064516129032258064516129);
ASSERT_TRUE(result->getValue(3,2,&val));
ASSERT_EQ(val,0.0806451612903225806451612903225812);
ASSERT_TRUE(result->getValue(3, 2, &val));
ASSERT_EQ(val, 0.0806451612903225806451612903225812);
ASSERT_FALSE(result->getValue(3,3,&val));
ASSERT_EQ(val,0);
ASSERT_TRUE(result->getValue(3, 3, &val));
ASSERT_EQ(val, 0.0);
ASSERT_TRUE(result->getValue(3,4,&val));
ASSERT_EQ(val,0.080645161290322580645161290322581);
ASSERT_TRUE(result->getValue(3, 4, &val));
ASSERT_EQ(val, 0.080645161290322580645161290322581);
ASSERT_FALSE(result->getValue(4,4,&val));
ASSERT_EQ(val,0);
ASSERT_TRUE(result->getValue(4, 4, &val));
ASSERT_EQ(val, 0.0);
delete parser;
} else {

Write Preview
Loading…
Cancel
Save