From 00b47979482c891fa695b0f00d9c17f256d54598 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 1 Apr 2013 11:42:29 +0200 Subject: [PATCH] Further refactoring. Other classes are now adapted to the changes in the sparse matrix class. --- .../SparseDtmcPrctlModelChecker.h | 11 +++---- src/modelchecker/SparseMdpPrctlModelChecker.h | 31 +++++++------------ src/models/GraphTransitions.h | 6 ++-- src/storage/SparseMatrix.h | 2 +- src/utility/GraphAnalyzer.h | 6 ++-- test/parser/ParseDtmcTest.cpp | 25 --------------- test/parser/ParseMdpTest.cpp | 1 - test/parser/ReadTraFileTest.cpp | 2 -- test/storage/SparseMatrixTest.cpp | 4 --- 9 files changed, 24 insertions(+), 64 deletions(-) delete mode 100644 test/parser/ParseDtmcTest.cpp diff --git a/src/modelchecker/SparseDtmcPrctlModelChecker.h b/src/modelchecker/SparseDtmcPrctlModelChecker.h index f9a76441e..4bcf4708a 100644 --- a/src/modelchecker/SparseDtmcPrctlModelChecker.h +++ b/src/modelchecker/SparseDtmcPrctlModelChecker.h @@ -311,14 +311,14 @@ public: } // Compute the reward vector to add in each step based on the available reward models. - std::vector* totalRewardVector = nullptr; + std::vector totalRewardVector; if (this->getModel().hasTransitionRewards()) { totalRewardVector = this->getModel().getTransitionMatrix()->getPointwiseProductRowSumVector(*this->getModel().getTransitionRewardMatrix()); if (this->getModel().hasStateRewards()) { - gmm::add(*this->getModel().getStateRewardVector(), *totalRewardVector); + gmm::add(*this->getModel().getStateRewardVector(), totalRewardVector); } } else { - totalRewardVector = new std::vector(*this->getModel().getStateRewardVector()); + totalRewardVector = std::vector(*this->getModel().getStateRewardVector()); } // Initialize result to either the state rewards of the model or the null vector. @@ -330,10 +330,9 @@ public: } // Perform the actual matrix-vector multiplication as long as the bound of the formula is met. - this->performMatrixVectorMultiplication(*this->getModel().getTransitionMatrix(), *result, totalRewardVector, formula.getBound()); + this->performMatrixVectorMultiplication(*this->getModel().getTransitionMatrix(), *result, &totalRewardVector, formula.getBound()); - // Delete temporary variables and return result. - delete totalRewardVector; + // Return result. return result; } diff --git a/src/modelchecker/SparseMdpPrctlModelChecker.h b/src/modelchecker/SparseMdpPrctlModelChecker.h index 389ffdaa3..df9d21d8c 100644 --- a/src/modelchecker/SparseMdpPrctlModelChecker.h +++ b/src/modelchecker/SparseMdpPrctlModelChecker.h @@ -238,7 +238,7 @@ public: if (maybeStatesSetBitCount > 0) { // First, we can eliminate the rows and columns from the original transition probability matrix for states // whose probabilities are already known. - storm::storage::SparseMatrix* submatrix = this->getModel().getTransitionMatrix()->getSubmatrix(maybeStates, *this->getModel().getNondeterministicChoiceIndices()); + storm::storage::SparseMatrix submatrix = this->getModel().getTransitionMatrix()->getSubmatrix(maybeStates, *this->getModel().getNondeterministicChoiceIndices()); // Get the "new" nondeterministic choice indices for the submatrix. std::vector subNondeterministicChoiceIndices = this->computeNondeterministicChoiceIndicesForConstraint(maybeStates); @@ -248,17 +248,13 @@ public: // Prepare the right-hand side of the equation system. For entry i this corresponds to // the accumulated probability of going from state i to some 'yes' state. - std::vector b(submatrix->getRowCount()); - this->getModel().getTransitionMatrix()->getConstrainedRowSumVector(maybeStates, *this->getModel().getNondeterministicChoiceIndices(), statesWithProbability1, &b); + std::vector b = this->getModel().getTransitionMatrix()->getConstrainedRowSumVector(maybeStates, *this->getModel().getNondeterministicChoiceIndices(), statesWithProbability1, submatrix.getRowCount()); // Solve the corresponding system of equations. - this->solveEquationSystem(*submatrix, x, b, subNondeterministicChoiceIndices); + this->solveEquationSystem(submatrix, x, b, subNondeterministicChoiceIndices); // Set values of resulting vector according to result. storm::utility::setVectorValues(result, maybeStates, x); - - // Delete temporary matrix. - delete submatrix; } // Set values of resulting vector that are known exactly. @@ -314,14 +310,14 @@ public: } // Compute the reward vector to add in each step based on the available reward models. - std::vector* totalRewardVector = nullptr; + std::vector totalRewardVector; if (this->getModel().hasTransitionRewards()) { totalRewardVector = this->getModel().getTransitionMatrix()->getPointwiseProductRowSumVector(*this->getModel().getTransitionRewardMatrix()); if (this->getModel().hasStateRewards()) { - gmm::add(*this->getModel().getStateRewardVector(), *totalRewardVector); + gmm::add(*this->getModel().getStateRewardVector(), totalRewardVector); } } else { - totalRewardVector = new std::vector(*this->getModel().getStateRewardVector()); + totalRewardVector = std::vector(*this->getModel().getStateRewardVector()); } // Initialize result to either the state rewards of the model or the null vector. @@ -332,10 +328,9 @@ public: result = new std::vector(this->getModel().getNumberOfStates()); } - this->performMatrixVectorMultiplication(*this->getModel().getTransitionMatrix(), *result, totalRewardVector, formula.getBound()); + this->performMatrixVectorMultiplication(*this->getModel().getTransitionMatrix(), *result, &totalRewardVector, formula.getBound()); // Delete temporary variables and return result. - delete totalRewardVector; return result; } @@ -383,7 +378,7 @@ public: if (maybeStatesSetBitCount > 0) { // First, we can eliminate the rows and columns from the original transition probability matrix for states // whose probabilities are already known. - storm::storage::SparseMatrix* submatrix = this->getModel().getTransitionMatrix()->getSubmatrix(maybeStates, *this->getModel().getNondeterministicChoiceIndices()); + storm::storage::SparseMatrix submatrix = this->getModel().getTransitionMatrix()->getSubmatrix(maybeStates, *this->getModel().getNondeterministicChoiceIndices()); // Get the "new" nondeterministic choice indices for the submatrix. std::vector subNondeterministicChoiceIndices = this->computeNondeterministicChoiceIndicesForConstraint(maybeStates); @@ -393,15 +388,14 @@ public: // Prepare the right-hand side of the equation system. For entry i this corresponds to // the accumulated probability of going from state i to some 'yes' state. - std::vector b(submatrix->getRowCount()); + std::vector b(submatrix.getRowCount()); if (this->getModel().hasTransitionRewards()) { // If a transition-based reward model is available, we initialize the right-hand // side to the vector resulting from summing the rows of the pointwise product // of the transition probability matrix and the transition reward matrix. - std::vector* pointwiseProductRowSumVector = this->getModel().getTransitionMatrix()->getPointwiseProductRowSumVector(*this->getModel().getTransitionRewardMatrix()); - storm::utility::selectVectorValues(&b, maybeStates, *this->getModel().getNondeterministicChoiceIndices(), *pointwiseProductRowSumVector); - delete pointwiseProductRowSumVector; + std::vector pointwiseProductRowSumVector = this->getModel().getTransitionMatrix()->getPointwiseProductRowSumVector(*this->getModel().getTransitionRewardMatrix()); + storm::utility::selectVectorValues(&b, maybeStates, *this->getModel().getNondeterministicChoiceIndices(), pointwiseProductRowSumVector); if (this->getModel().hasStateRewards()) { // If a state-based reward model is also available, we need to add this vector @@ -422,11 +416,10 @@ public: } // Solve the corresponding system of equations. - this->solveEquationSystem(*submatrix, x, b, subNondeterministicChoiceIndices); + this->solveEquationSystem(submatrix, x, b, subNondeterministicChoiceIndices); // Set values of resulting vector according to result. storm::utility::setVectorValues(result, maybeStates, x); - delete submatrix; } // Set values of resulting vector that are known exactly. diff --git a/src/models/GraphTransitions.h b/src/models/GraphTransitions.h index 8782324ad..feed1b952 100644 --- a/src/models/GraphTransitions.h +++ b/src/models/GraphTransitions.h @@ -220,7 +220,7 @@ private: // Now we are ready to actually fill in the list of predecessors for // every state. Again, we start by considering all but the last row. for (uint_fast64_t i = 0; i < numberOfStates; ++i) { - for (auto rowIt = transitionMatrix.beginConstColumnIterator(i); rowIt != transitionMatrix.endConstColumnIterator(i); ++rowIt) { + for (auto rowIt = transitionMatrix.constColumnIteratorBegin(i); rowIt != transitionMatrix.constColumnIteratorEnd(i); ++rowIt) { this->successorList[nextIndices[*rowIt]++] = i; } } @@ -230,7 +230,7 @@ private: // First, we need to count how many backward transitions each state has. for (uint_fast64_t i = 0; i < numberOfStates; ++i) { for (uint_fast64_t j = nondeterministicChoiceIndices[i]; j < nondeterministicChoiceIndices[i + 1]; ++j) { - for (auto rowIt = transitionMatrix.beginConstColumnIterator(j); rowIt != transitionMatrix.endConstColumnIterator(j); ++rowIt) { + for (auto rowIt = transitionMatrix.constColumnIteratorBegin(j); rowIt != transitionMatrix.constColumnIteratorEnd(j); ++rowIt) { this->stateIndications[*rowIt + 1]++; } } @@ -254,7 +254,7 @@ private: // every state. Again, we start by considering all but the last row. for (uint_fast64_t i = 0; i < numberOfStates; i++) { for (uint_fast64_t j = nondeterministicChoiceIndices[i]; j < nondeterministicChoiceIndices[i + 1]; ++j) { - for (auto rowIt = transitionMatrix.beginConstColumnIterator(j); rowIt != transitionMatrix.endConstColumnIterator(j); ++rowIt) { + for (auto rowIt = transitionMatrix.constColumnIteratorBegin(j); rowIt != transitionMatrix.constColumnIteratorEnd(j); ++rowIt) { this->successorList[nextIndices[*rowIt]++] = i; } } diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index b54cb7538..5f76ede9b 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -136,7 +136,7 @@ public: * @returns The column of the current non-zero element this iterator points to. */ uint_fast64_t column() const { - return matrix.columnIndications[index]; + return matrix.columnIndications[posIndex]; } /*! diff --git a/src/utility/GraphAnalyzer.h b/src/utility/GraphAnalyzer.h index b432d0b2a..1ec2c6a53 100644 --- a/src/utility/GraphAnalyzer.h +++ b/src/utility/GraphAnalyzer.h @@ -236,7 +236,7 @@ public: // nondeterminstic choices. for (uint_fast64_t row = (*nondeterministicChoiceIndices)[*it]; row < (*nondeterministicChoiceIndices)[*it + 1]; ++row) { bool allSuccessorsInCurrentStates = true; - for (auto colIt = transitionMatrix->beginConstColumnIterator(row); colIt != transitionMatrix->endConstColumnIterator(row); ++colIt) { + for (auto colIt = transitionMatrix->constColumnIteratorBegin(row); colIt != transitionMatrix->constColumnIteratorEnd(row); ++colIt) { if (!currentStates->get(*colIt)) { allSuccessorsInCurrentStates = false; break; @@ -322,7 +322,7 @@ public: bool addToStatesWithProbability0 = true; for (auto rowIt = nondeterministicChoiceIndices->begin() + *it; rowIt != nondeterministicChoiceIndices->begin() + *it + 1; ++rowIt) { bool hasAtLeastOneSuccessorWithProbabilityGreater0 = false; - for (auto colIt = transitionMatrix->beginConstColumnIterator(*rowIt); colIt != transitionMatrix->endConstColumnIterator(*rowIt); ++colIt) { + for (auto colIt = transitionMatrix->constColumnIteratorBegin(*rowIt); colIt != transitionMatrix->constColumnIteratorEnd(*rowIt); ++colIt) { if (statesWithProbability0->get(*colIt)) { hasAtLeastOneSuccessorWithProbabilityGreater0 = true; break; @@ -383,7 +383,7 @@ public: // nondeterminstic choices. bool allSuccessorsInCurrentStatesForAllChoices = true; for (uint_fast64_t row = (*nondeterministicChoiceIndices)[*it]; row < (*nondeterministicChoiceIndices)[*it + 1]; ++row) { - for (auto colIt = transitionMatrix->beginConstColumnIterator(row); colIt != transitionMatrix->endConstColumnIterator(row); ++colIt) { + for (auto colIt = transitionMatrix->constColumnIteratorBegin(row); colIt != transitionMatrix->constColumnIteratorEnd(row); ++colIt) { if (!currentStates->get(*colIt)) { allSuccessorsInCurrentStatesForAllChoices = false; goto afterCheckLoop; diff --git a/test/parser/ParseDtmcTest.cpp b/test/parser/ParseDtmcTest.cpp deleted file mode 100644 index d99c16f74..000000000 --- a/test/parser/ParseDtmcTest.cpp +++ /dev/null @@ -1,25 +0,0 @@ -/* - * ParseDtmcTest.cpp - * - * Created on: 03.12.2012 - * Author: Thomas Heinemann - */ - - -#include "gtest/gtest.h" -#include "storm-config.h" -#include "src/parser/DeterministicModelParser.h" -#include "src/utility/IoUtility.h" - -TEST(ParseDtmcTest, parseAndOutput) { - 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")); - - ASSERT_NO_THROW(storm::utility::dtmcToDot(*(dtmcParser->getDtmc()), STORM_CPP_TESTS_BASE_PATH "/parser/output.dot")); - - delete dtmcParser; -} - - diff --git a/test/parser/ParseMdpTest.cpp b/test/parser/ParseMdpTest.cpp index 02302dc2a..b19335fdd 100644 --- a/test/parser/ParseMdpTest.cpp +++ b/test/parser/ParseMdpTest.cpp @@ -9,7 +9,6 @@ #include "gtest/gtest.h" #include "storm-config.h" #include "src/parser/NondeterministicModelParser.h" -#include "src/utility/IoUtility.h" TEST(ParseMdpTest, parseAndOutput) { storm::parser::NondeterministicModelParser* mdpParser = nullptr; diff --git a/test/parser/ReadTraFileTest.cpp b/test/parser/ReadTraFileTest.cpp index 6a697536d..807ce27fd 100644 --- a/test/parser/ReadTraFileTest.cpp +++ b/test/parser/ReadTraFileTest.cpp @@ -12,8 +12,6 @@ #include "src/exceptions/FileIoException.h" #include "src/exceptions/WrongFileFormatException.h" -#include "src/utility/IoUtility.h" - TEST(ReadTraFileTest, NonExistingFileTest) { //No matter what happens, please don't create a file with the name "nonExistingFile.not"! :-) ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser(STORM_CPP_TESTS_BASE_PATH "/nonExistingFile.not"), storm::exceptions::FileIoException); diff --git a/test/storage/SparseMatrixTest.cpp b/test/storage/SparseMatrixTest.cpp index 96a1cea43..4ce2a7520 100644 --- a/test/storage/SparseMatrixTest.cpp +++ b/test/storage/SparseMatrixTest.cpp @@ -272,10 +272,6 @@ TEST(SparseMatrixTest, ConversionFromSparseEigen_RowMajor_SparseMatrixTest) { ASSERT_NO_THROW(ssm = storm::adapters::StormAdapter::toStormSparseMatrix(esm)); ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::MatrixStatus::ReadReady); - - const std::vector rowP = ssm->getRowIndications(); - const std::vector colP = ssm->getColumnIndications(); - const std::vector valP = ssm->getStorage(); int target = -1; for (auto &coeff: tripletList) {