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

Further refactoring. Other classes are now adapted to the changes in the sparse matrix class.

tempestpy_adaptions
dehnert 12 years ago
parent
9ae177c9b5
commit
00b4797948
9 changed files with 24 additions and 64 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. 11
      src/modelchecker/SparseDtmcPrctlModelChecker.h
  2. 31
      src/modelchecker/SparseMdpPrctlModelChecker.h
  3. 6
      src/models/GraphTransitions.h
  4. 2
      src/storage/SparseMatrix.h
  5. 6
      src/utility/GraphAnalyzer.h
  6. 25
      test/parser/ParseDtmcTest.cpp
  7. 1
      test/parser/ParseMdpTest.cpp
  8. 2
      test/parser/ReadTraFileTest.cpp
  9. 4
      test/storage/SparseMatrixTest.cpp

11
src/modelchecker/SparseDtmcPrctlModelChecker.h
View File

@ -311,14 +311,14 @@ public:
}
// Compute the reward vector to add in each step based on the available reward models.
std::vector<Type>* totalRewardVector = nullptr;
std::vector<Type> 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<Type>(*this->getModel().getStateRewardVector());
totalRewardVector = std::vector<Type>(*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;
}

31
src/modelchecker/SparseMdpPrctlModelChecker.h
View File

@ -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<Type>* submatrix = this->getModel().getTransitionMatrix()->getSubmatrix(maybeStates, *this->getModel().getNondeterministicChoiceIndices());
storm::storage::SparseMatrix<Type> submatrix = this->getModel().getTransitionMatrix()->getSubmatrix(maybeStates, *this->getModel().getNondeterministicChoiceIndices());
// Get the "new" nondeterministic choice indices for the submatrix.
std::vector<uint_fast64_t> 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<Type> b(submatrix->getRowCount());
this->getModel().getTransitionMatrix()->getConstrainedRowSumVector(maybeStates, *this->getModel().getNondeterministicChoiceIndices(), statesWithProbability1, &b);
std::vector<Type> 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<Type>(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<Type>* totalRewardVector = nullptr;
std::vector<Type> 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<Type>(*this->getModel().getStateRewardVector());
totalRewardVector = std::vector<Type>(*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<Type>(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<Type>* submatrix = this->getModel().getTransitionMatrix()->getSubmatrix(maybeStates, *this->getModel().getNondeterministicChoiceIndices());
storm::storage::SparseMatrix<Type> submatrix = this->getModel().getTransitionMatrix()->getSubmatrix(maybeStates, *this->getModel().getNondeterministicChoiceIndices());
// Get the "new" nondeterministic choice indices for the submatrix.
std::vector<uint_fast64_t> 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<Type> b(submatrix->getRowCount());
std::vector<Type> 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<Type>* pointwiseProductRowSumVector = this->getModel().getTransitionMatrix()->getPointwiseProductRowSumVector(*this->getModel().getTransitionRewardMatrix());
storm::utility::selectVectorValues(&b, maybeStates, *this->getModel().getNondeterministicChoiceIndices(), *pointwiseProductRowSumVector);
delete pointwiseProductRowSumVector;
std::vector<Type> 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<Type>(result, maybeStates, x);
delete submatrix;
}
// Set values of resulting vector that are known exactly.

6
src/models/GraphTransitions.h
View File

@ -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;
}
}

2
src/storage/SparseMatrix.h
View File

@ -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];
}
/*!

6
src/utility/GraphAnalyzer.h
View File

@ -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;

25
test/parser/ParseDtmcTest.cpp
View File

@ -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;
}

1
test/parser/ParseMdpTest.cpp
View File

@ -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;

2
test/parser/ReadTraFileTest.cpp
View File

@ -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);

4
test/storage/SparseMatrixTest.cpp
View File

@ -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<int>::MatrixStatus::ReadReady);
const std::vector<uint_fast64_t> rowP = ssm->getRowIndications();
const std::vector<uint_fast64_t> colP = ssm->getColumnIndications();
const std::vector<int> valP = ssm->getStorage();
int target = -1;
for (auto &coeff: tripletList) {

Write Preview
Loading…
Cancel
Save