From d266d9effe20af0d9c4d4ec6a0eec4901a716470 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 1 Apr 2013 15:36:48 +0200 Subject: [PATCH] Fixed another bug in sparse matrix. Fixed bug in test. --- src/storage/SparseMatrix.h | 8 ++++---- src/storm.cpp | 2 +- src/utility/GraphAnalyzer.h | 2 +- test/parser/ReadLabFileTest.cpp | 29 ++++++++++++++++------------- 4 files changed, 22 insertions(+), 19 deletions(-) diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index c24dcb36b..6dfeabf2a 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -275,7 +275,7 @@ public: // error otherwise. if ((row > rowCount) || (col > colCount)) { triggerErrorState(); - LOG4CPLUS_ERROR(logger, "Trying to add a value at illegal position (" << row << ", " << col << ")."); + LOG4CPLUS_ERROR(logger, "Trying to add a value at illegal position (" << row << ", " << col << ") in matrix of size (" << rowCount << ", " << colCount << ")."); throw storm::exceptions::OutOfRangeException("Trying to add a value at illegal position."); } @@ -717,7 +717,7 @@ public: uint_fast64_t* bitsSetBeforeIndex = new uint_fast64_t[colCount]; uint_fast64_t lastIndex = 0; uint_fast64_t currentNumberOfSetBits = 0; - for (auto index : rowGroupIndices) { + for (auto index : rowGroupConstraint) { while (lastIndex <= index) { bitsSetBeforeIndex[lastIndex++] = currentNumberOfSetBits; } @@ -726,7 +726,7 @@ public: // Copy over selected entries. uint_fast64_t rowCount = 0; - for (auto index : rowGroupIndices) { + for (auto index : rowGroupConstraint) { for (uint_fast64_t i = rowGroupIndices[index]; i < rowGroupIndices[index + 1]; ++i) { for (uint_fast64_t j = rowIndications[i]; j < rowIndications[i + 1]; ++j) { if (rowGroupConstraint.get(columnIndications[j])) { @@ -976,7 +976,7 @@ public: * @returns An iterator that points to the first element after the matrix. */ ConstIndexIterator constColumnIteratorEnd(uint_fast64_t row) const { - return &(this->columnIndications[0]) + this->rowIndications[row]; + return &(this->columnIndications[0]) + this->rowIndications[row + 1]; } /*! diff --git a/src/storm.cpp b/src/storm.cpp index dfedb0954..bb089fb5c 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -449,7 +449,7 @@ void testChecking() { std::shared_ptr> mdp = parser.getModel>(); mdp->printModelInformationToStream(std::cout); - // testCheckingDice(*mdp); + testCheckingDice(*mdp); // testCheckingAsynchLeader(*mdp); // testCheckingConsensus(*mdp); } else { diff --git a/src/utility/GraphAnalyzer.h b/src/utility/GraphAnalyzer.h index 1ec2c6a53..025c2fe4a 100644 --- a/src/utility/GraphAnalyzer.h +++ b/src/utility/GraphAnalyzer.h @@ -72,7 +72,7 @@ public: // Get the backwards transition relation from the model to ease the search. storm::models::GraphTransitions backwardTransitions(*model.getTransitionMatrix(), false); - + // Add all psi states as the already satisfy the condition. *statesWithProbabilityGreater0 |= psiStates; diff --git a/test/parser/ReadLabFileTest.cpp b/test/parser/ReadLabFileTest.cpp index 9b1d72241..d8ff86344 100644 --- a/test/parser/ReadLabFileTest.cpp +++ b/test/parser/ReadLabFileTest.cpp @@ -38,39 +38,42 @@ TEST(ReadLabFileTest, ParseTest) { ASSERT_TRUE(labeling->containsAtomicProposition(smth)); //Testing whether all and only the correct nodes are labeled with "phi" + ASSERT_TRUE(labeling->stateHasAtomicProposition(phi,0)); ASSERT_TRUE(labeling->stateHasAtomicProposition(phi,1)); ASSERT_TRUE(labeling->stateHasAtomicProposition(phi,2)); - ASSERT_TRUE(labeling->stateHasAtomicProposition(phi,3)); - ASSERT_TRUE(labeling->stateHasAtomicProposition(phi,5)); - ASSERT_TRUE(labeling->stateHasAtomicProposition(phi,7)); - ASSERT_TRUE(labeling->stateHasAtomicProposition(phi,9)); - ASSERT_TRUE(labeling->stateHasAtomicProposition(phi,10)); - ASSERT_TRUE(labeling->stateHasAtomicProposition(phi,11)); + ASSERT_FALSE(labeling->stateHasAtomicProposition(phi,3)); ASSERT_FALSE(labeling->stateHasAtomicProposition(phi,4)); + ASSERT_FALSE(labeling->stateHasAtomicProposition(phi,5)); ASSERT_FALSE(labeling->stateHasAtomicProposition(phi,6)); + ASSERT_FALSE(labeling->stateHasAtomicProposition(phi,7)); + ASSERT_FALSE(labeling->stateHasAtomicProposition(phi,8)); + ASSERT_FALSE(labeling->stateHasAtomicProposition(phi,9)); + ASSERT_FALSE(labeling->stateHasAtomicProposition(phi,10)); + ASSERT_FALSE(labeling->stateHasAtomicProposition(phi,11)); //Testing whether all and only the correct nodes are labeled with "psi" - ASSERT_TRUE(labeling->stateHasAtomicProposition(psi,6)); - ASSERT_TRUE(labeling->stateHasAtomicProposition(psi,7)); - ASSERT_TRUE(labeling->stateHasAtomicProposition(psi,8)); - + ASSERT_FALSE(labeling->stateHasAtomicProposition(psi,0)); ASSERT_FALSE(labeling->stateHasAtomicProposition(psi,1)); ASSERT_FALSE(labeling->stateHasAtomicProposition(psi,2)); ASSERT_FALSE(labeling->stateHasAtomicProposition(psi,3)); ASSERT_FALSE(labeling->stateHasAtomicProposition(psi,4)); ASSERT_FALSE(labeling->stateHasAtomicProposition(psi,5)); + ASSERT_FALSE(labeling->stateHasAtomicProposition(psi,6)); + ASSERT_FALSE(labeling->stateHasAtomicProposition(psi,7)); + ASSERT_FALSE(labeling->stateHasAtomicProposition(psi,8)); ASSERT_FALSE(labeling->stateHasAtomicProposition(psi,9)); ASSERT_FALSE(labeling->stateHasAtomicProposition(psi,10)); ASSERT_FALSE(labeling->stateHasAtomicProposition(psi,11)); //Testing whether all and only the correct nodes are labeled with "smth" - ASSERT_TRUE(labeling->stateHasAtomicProposition(smth,4)); - ASSERT_TRUE(labeling->stateHasAtomicProposition(smth,5)); + ASSERT_TRUE(labeling->stateHasAtomicProposition(smth,2)); + ASSERT_FALSE(labeling->stateHasAtomicProposition(smth,0)); ASSERT_FALSE(labeling->stateHasAtomicProposition(smth,1)); - ASSERT_FALSE(labeling->stateHasAtomicProposition(smth,2)); ASSERT_FALSE(labeling->stateHasAtomicProposition(smth,3)); + ASSERT_FALSE(labeling->stateHasAtomicProposition(smth,4)); + ASSERT_FALSE(labeling->stateHasAtomicProposition(smth,5)); ASSERT_FALSE(labeling->stateHasAtomicProposition(smth,6)); ASSERT_FALSE(labeling->stateHasAtomicProposition(smth,7)); ASSERT_FALSE(labeling->stateHasAtomicProposition(smth,8));