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

Made changes to comply with new SparseMatrix Interface (YUCK). 

Fixed tests, all that stuff.


Former-commit-id: c78de5f8ce
tempestpy_adaptions
PBerger 11 years ago
parent
eca20ce085
commit
d2f4c85711
9 changed files with 98 additions and 43 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. 10
      resources/cudaForStorm/srcCuda/basicValueIteration.cu
  2. 80
      resources/cudaForStorm/srcCuda/basicValueIteration.h
  3. 2
      src/models/PseudoModel.cpp
  4. 6
      src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp
  5. 2
      src/storage/SparseMatrix.cpp
  6. 2
      src/storage/SparseMatrix.h
  7. 6
      src/utility/graph.h
  8. 29
      test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp
  9. 4
      test/functional/storage/StronglyConnectedComponentDecompositionTest.cpp

10
resources/cudaForStorm/srcCuda/basicValueIteration.cu
View File

@ -57,7 +57,7 @@ void exploadVector(std::vector<std::pair<IndexType, ValueType>> const& inputVect
}
template <bool Minimize, bool Relative, typename IndexType, typename ValueType>
void basicValueIteration_mvReduce(uint_fast64_t const maxIterationCount, ValueType const precision, std::vector<IndexType> const& matrixRowIndices, std::vector<std::pair<IndexType, ValueType>> const& columnIndicesAndValues, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<IndexType> const& nondeterministicChoiceIndices) {
void basicValueIteration_mvReduce(uint_fast64_t const maxIterationCount, ValueType const precision, std::vector<IndexType> const& matrixRowIndices, std::vector<storm::storage::MatrixEntry<ValueType>> const& columnIndicesAndValues, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<IndexType> const& nondeterministicChoiceIndices) {
//std::vector<IndexType> matrixColumnIndices;
//std::vector<ValueType> matrixValues;
//exploadVector<IndexType, ValueType>(columnIndicesAndValues, matrixColumnIndices, matrixValues);
@ -305,7 +305,7 @@ cleanup:
}
template <typename IndexType, typename ValueType>
void basicValueIteration_spmv(uint_fast64_t const matrixColCount, std::vector<IndexType> const& matrixRowIndices, std::vector<std::pair<IndexType, ValueType>> const& columnIndicesAndValues, std::vector<ValueType> const& x, std::vector<ValueType>& b) {
void basicValueIteration_spmv(uint_fast64_t const matrixColCount, std::vector<IndexType> const& matrixRowIndices, std::vector<storm::storage::MatrixEntry<ValueType>> const& columnIndicesAndValues, std::vector<ValueType> const& x, std::vector<ValueType>& b) {
IndexType* device_matrixRowIndices = nullptr;
IndexType* device_matrixColIndicesAndValues = nullptr;
ValueType* device_x = nullptr;
@ -681,7 +681,7 @@ cleanup:
*
*/
void basicValueIteration_spmv_uint64_double(uint_fast64_t const matrixColCount, std::vector<uint_fast64_t> const& matrixRowIndices, std::vector<std::pair<uint_fast64_t, double>> const& columnIndicesAndValues, std::vector<double> const& x, std::vector<double>& b) {
void basicValueIteration_spmv_uint64_double(uint_fast64_t const matrixColCount, std::vector<uint_fast64_t> const& matrixRowIndices, std::vector<storm::storage::MatrixEntry<double>> const& columnIndicesAndValues, std::vector<double> const& x, std::vector<double>& b) {
basicValueIteration_spmv(matrixColCount, matrixRowIndices, columnIndicesAndValues, x, b);
}
@ -705,7 +705,7 @@ void basicValueIteration_equalModuloPrecision_double_NonRelative(std::vector<dou
basicValueIteration_equalModuloPrecision<double, false>(x, y, maxElement);
}
void basicValueIteration_mvReduce_uint64_double_minimize(uint_fast64_t const maxIterationCount, double const precision, bool const relativePrecisionCheck, std::vector<uint_fast64_t> const& matrixRowIndices, std::vector<std::pair<uint_fast64_t, double>> const& columnIndicesAndValues, std::vector<double>& x, std::vector<double> const& b, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices) {
void basicValueIteration_mvReduce_uint64_double_minimize(uint_fast64_t const maxIterationCount, double const precision, bool const relativePrecisionCheck, std::vector<uint_fast64_t> const& matrixRowIndices, std::vector<storm::storage::MatrixEntry<double>> const& columnIndicesAndValues, std::vector<double>& x, std::vector<double> const& b, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices) {
if (relativePrecisionCheck) {
basicValueIteration_mvReduce<true, true, uint_fast64_t, double>(maxIterationCount, precision, matrixRowIndices, columnIndicesAndValues, x, b, nondeterministicChoiceIndices);
} else {
@ -713,7 +713,7 @@ void basicValueIteration_mvReduce_uint64_double_minimize(uint_fast64_t const max
}
}
void basicValueIteration_mvReduce_uint64_double_maximize(uint_fast64_t const maxIterationCount, double const precision, bool const relativePrecisionCheck, std::vector<uint_fast64_t> const& matrixRowIndices, std::vector<std::pair<uint_fast64_t, double>> const& columnIndicesAndValues, std::vector<double>& x, std::vector<double> const& b, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices) {
void basicValueIteration_mvReduce_uint64_double_maximize(uint_fast64_t const maxIterationCount, double const precision, bool const relativePrecisionCheck, std::vector<uint_fast64_t> const& matrixRowIndices, std::vector<storm::storage::MatrixEntry<double>> const& columnIndicesAndValues, std::vector<double>& x, std::vector<double> const& b, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices) {
if (relativePrecisionCheck) {
basicValueIteration_mvReduce<false, true, uint_fast64_t, double>(maxIterationCount, precision, matrixRowIndices, columnIndicesAndValues, x, b, nondeterministicChoiceIndices);
} else {

80
resources/cudaForStorm/srcCuda/basicValueIteration.h
View File

@ -8,10 +8,84 @@
// Library exports
#include "cudaForStorm_Export.h"
/* Helper declaration to cope with new internal format */
#ifndef STORM_STORAGE_SPARSEMATRIX_H_
namespace storm {
namespace storage {
template<typename T>
class MatrixEntry {
public:
/*!
* Constructs a matrix entry with the given column and value.
*
* @param column The column of the matrix entry.
* @param value The value of the matrix entry.
*/
MatrixEntry(uint_fast64_t column, T value);
/*!
* Move-constructs the matrix entry fro the given column-value pair.
*
* @param pair The column-value pair from which to move-construct the matrix entry.
*/
MatrixEntry(std::pair<uint_fast64_t, T>&& pair);
//MatrixEntry() = default;
//MatrixEntry(MatrixEntry const& other) = default;
//MatrixEntry& operator=(MatrixEntry const& other) = default;
#ifndef WINDOWS
//MatrixEntry(MatrixEntry&& other) = default;
//MatrixEntry& operator=(MatrixEntry&& other) = default;
#endif
/*!
* Retrieves the column of the matrix entry.
*
* @return The column of the matrix entry.
*/
uint_fast64_t const& getColumn() const;
/*!
* Retrieves the column of the matrix entry.
*
* @return The column of the matrix entry.
*/
uint_fast64_t& getColumn();
/*!
* Retrieves the value of the matrix entry.
*
* @return The value of the matrix entry.
*/
T const& getValue() const;
/*!
* Retrieves the value of the matrix entry.
*
* @return The value of the matrix entry.
*/
T& getValue();
/*!
* Retrieves a pair of column and value that characterizes this entry.
*
* @return A column-value pair that characterizes this entry.
*/
std::pair<uint_fast64_t, T> const& getColumnValuePair() const;
private:
// The actual matrix entry.
std::pair<uint_fast64_t, T> entry;
};
}
}
#endif
cudaForStorm_EXPORT size_t basicValueIteration_mvReduce_uint64_double_calculateMemorySize(size_t const rowCount, size_t const rowGroupCount, size_t const nnzCount);
cudaForStorm_EXPORT void basicValueIteration_mvReduce_uint64_double_minimize(uint_fast64_t const maxIterationCount, double const precision, bool const relativePrecisionCheck, std::vector<uint_fast64_t> const& matrixRowIndices, std::vector<std::pair<uint_fast64_t, double>> const& columnIndicesAndValues, std::vector<double>& x, std::vector<double> const& b, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices);
cudaForStorm_EXPORT void basicValueIteration_mvReduce_uint64_double_maximize(uint_fast64_t const maxIterationCount, double const precision, bool const relativePrecisionCheck, std::vector<uint_fast64_t> const& matrixRowIndices, std::vector<std::pair<uint_fast64_t, double>> const& columnIndicesAndValues, std::vector<double>& x, std::vector<double> const& b, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices);
cudaForStorm_EXPORT void basicValueIteration_spmv_uint64_double(uint_fast64_t const matrixColCount, std::vector<uint_fast64_t> const& matrixRowIndices, std::vector<std::pair<uint_fast64_t, double>> const& columnIndicesAndValues, std::vector<double> const& x, std::vector<double>& b);
cudaForStorm_EXPORT void basicValueIteration_mvReduce_uint64_double_minimize(uint_fast64_t const maxIterationCount, double const precision, bool const relativePrecisionCheck, std::vector<uint_fast64_t> const& matrixRowIndices, std::vector<storm::storage::MatrixEntry<double>> const& columnIndicesAndValues, std::vector<double>& x, std::vector<double> const& b, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices);
cudaForStorm_EXPORT void basicValueIteration_mvReduce_uint64_double_maximize(uint_fast64_t const maxIterationCount, double const precision, bool const relativePrecisionCheck, std::vector<uint_fast64_t> const& matrixRowIndices, std::vector<storm::storage::MatrixEntry<double>> const& columnIndicesAndValues, std::vector<double>& x, std::vector<double> const& b, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices);
cudaForStorm_EXPORT void basicValueIteration_spmv_uint64_double(uint_fast64_t const matrixColCount, std::vector<uint_fast64_t> const& matrixRowIndices, std::vector<storm::storage::MatrixEntry<double>> const& columnIndicesAndValues, std::vector<double> const& x, std::vector<double>& b);
cudaForStorm_EXPORT void basicValueIteration_addVectorsInplace_double(std::vector<double>& a, std::vector<double> const& b);
cudaForStorm_EXPORT void basicValueIteration_reduceGroupedVector_uint64_double_minimize(std::vector<double> const& groupedVector, std::vector<uint_fast64_t> const& grouping, std::vector<double>& targetVector);
cudaForStorm_EXPORT void basicValueIteration_reduceGroupedVector_uint64_double_maximize(std::vector<double> const& groupedVector, std::vector<uint_fast64_t> const& grouping, std::vector<double>& targetVector);

2
src/models/PseudoModel.cpp
View File

@ -80,7 +80,7 @@ namespace storm {
boost::container::flat_set<uint_fast64_t> allTargetBlocks;
for (auto state : block) {
for (auto const& transitionEntry : this->getRows(state)) {
uint_fast64_t targetBlock = stateToBlockMap[transitionEntry.first];
uint_fast64_t targetBlock = stateToBlockMap[transitionEntry.getColumn()];
// We only need to consider transitions that are actually leaving the SCC.
if (targetBlock != currentBlockIndex) {

6
src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp
View File

@ -94,7 +94,7 @@ namespace storm {
std::vector<uint_fast64_t> sccSubNondeterministicChoiceIndices(sccSubmatrix.getColumnCount() + 1);
sccSubNondeterministicChoiceIndices.at(0) = 0;
// Preprocess all dependant states
// Preprocess all dependent states
// Remove outgoing transitions and create the ChoiceIndices
uint_fast64_t innerIndex = 0;
uint_fast64_t outerIndex = 0;
@ -105,10 +105,10 @@ namespace storm {
for (auto rowGroupIt = nondeterministicChoiceIndices[state]; rowGroupIt != nondeterministicChoiceIndices[state + 1]; ++rowGroupIt) {
typename storm::storage::SparseMatrix<ValueType>::const_rows row = A.getRow(rowGroupIt);
for (auto rowIt = row.begin(); rowIt != row.end(); ++rowIt) {
if (!subMatrixIndices.get(rowIt->first)) {
if (!subMatrixIndices.get(rowIt->getColumn())) {
// This is an outgoing transition of a state in the SCC to a state not included in the SCC
// Subtracting Pr(tau) * x_other from b fixes that
sccSubB.at(innerIndex) = sccSubB.at(innerIndex) + (rowIt->second * x.at(rowIt->first));
sccSubB.at(innerIndex) = sccSubB.at(innerIndex) + (rowIt->getValue() * x.at(rowIt->getColumn()));
}
}
++innerIndex;

2
src/storage/SparseMatrix.cpp
View File

@ -931,7 +931,7 @@ namespace storm {
* Returns a reference to the internal columnMapping vector
*/
template<typename T>
std::vector<std::pair<uint_fast64_t, T>> const& SparseMatrix<T>::__internal_getColumnsAndValues() {
std::vector<MatrixEntry<T>> const& SparseMatrix<T>::__internal_getColumnsAndValues() {
return this->columnsAndValues;
}

2
src/storage/SparseMatrix.h
View File

@ -732,7 +732,7 @@ namespace storm {
/*!
* Returns a reference to the internal columnMapping vector
*/
std::vector<std::pair<uint_fast64_t, T>> const& __internal_getColumnsAndValues();
std::vector<MatrixEntry<T>> const& __internal_getColumnsAndValues();
private:
/*!
* Creates a submatrix of the current matrix by keeping only row groups and columns in the given row group

6
src/utility/graph.h
View File

@ -598,12 +598,12 @@ namespace storm {
recursionStepBackward:
for (; successorIterator != matrix.end(currentState); ++successorIterator) {
if (!visitedStates.get(successorIterator->first)) {
if (!visitedStates.get(successorIterator->getColumn())) {
// Put unvisited successor on top of our recursion stack and remember that.
recursionStack.push_back(successorIterator->first);
recursionStack.push_back(successorIterator->getColumn());
// Also, put initial value for iterator on corresponding recursion stack.
iteratorRecursionStack.push_back(matrix.begin(successorIterator->first));
iteratorRecursionStack.push_back(matrix.begin(successorIterator->getColumn()));
goto recursionStepForward;
}

29
test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp
View File

@ -10,13 +10,8 @@
#include "storm-config.h"
TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) {
storm::settings::Settings* s = storm::settings::Settings::getInstance();
storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.trans.rew");
//storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/mdp/scc/scc.tra", STORM_CPP_BASE_PATH "/examples/mdp/scc/scc.lab", "");
ASSERT_EQ(parser.getType(), storm::models::MDP);
std::shared_ptr<storm::models::Mdp<double>> mdp = parser.getModel<storm::models::Mdp<double>>();
storm::settings::Settings* s = storm::settings::Settings::getInstance();
std::shared_ptr<storm::models::Mdp<double>> mdp = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.trans.rew")->as<storm::models::Mdp<double>>();
ASSERT_EQ(mdp->getNumberOfStates(), 169ull);
ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull);
@ -108,12 +103,7 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) {
ASSERT_LT(std::abs(result[0] - 7.33333151), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
#endif
delete rewardFormula;
storm::parser::AutoParser<double> stateRewardParser(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.state.rew", "");
ASSERT_EQ(stateRewardParser.getType(), storm::models::MDP);
std::shared_ptr<storm::models::Mdp<double>> stateRewardMdp = stateRewardParser.getModel<storm::models::Mdp<double>>();
std::shared_ptr<storm::models::Mdp<double>> stateRewardMdp = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.state.rew", "")->as<storm::models::Mdp<double>>();
storm::modelchecker::prctl::TopologicalValueIterationMdpPrctlModelChecker<double> stateRewardModelChecker(*stateRewardMdp);
@ -142,12 +132,7 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) {
ASSERT_LT(std::abs(result[0] - 7.33333151), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
#endif
delete rewardFormula;
storm::parser::AutoParser<double> stateAndTransitionRewardParser(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.state.rew", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.trans.rew");
ASSERT_EQ(stateAndTransitionRewardParser.getType(), storm::models::MDP);
std::shared_ptr<storm::models::Mdp<double>> stateAndTransitionRewardMdp = stateAndTransitionRewardParser.getModel<storm::models::Mdp<double>>();
std::shared_ptr<storm::models::Mdp<double>> stateAndTransitionRewardMdp = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.state.rew", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.trans.rew")->as<storm::models::Mdp<double>>();
storm::modelchecker::prctl::TopologicalValueIterationMdpPrctlModelChecker<double> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp);
@ -180,11 +165,7 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) {
TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, AsynchronousLeader) {
storm::settings::Settings* s = storm::settings::Settings::getInstance();
storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.trans.rew");
ASSERT_EQ(parser.getType(), storm::models::MDP);
std::shared_ptr<storm::models::Mdp<double>> mdp = parser.getModel<storm::models::Mdp<double>>();
std::shared_ptr<storm::models::Mdp<double>> mdp = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.trans.rew")->as<storm::models::Mdp<double>>();
ASSERT_EQ(mdp->getNumberOfStates(), 3172ull);
ASSERT_EQ(mdp->getNumberOfTransitions(), 7144ull);

4
test/functional/storage/StronglyConnectedComponentDecompositionTest.cpp
View File

@ -1,6 +1,7 @@
#include "gtest/gtest.h"
#include "storm-config.h"
#include "src/parser/AutoParser.h"
#include "src/models/Dtmc.h"
#include "src/storage/StronglyConnectedComponentDecomposition.h"
#include "src/models/MarkovAutomaton.h"
@ -49,8 +50,7 @@ TEST(StronglyConnectedComponentDecomposition, FullSystem2) {
}
TEST(StronglyConnectedComponentDecomposition, MatrixBasedSystem) {
storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/dtmc/scc/scc.tra", STORM_CPP_BASE_PATH "/examples/dtmc/scc/scc.lab", "", "");
std::shared_ptr<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>();
std::shared_ptr<storm::models::Dtmc<double>> dtmc = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/scc/scc.tra", STORM_CPP_BASE_PATH "/examples/dtmc/scc/scc.lab", "", "")->as<storm::models::Dtmc<double>>();
storm::storage::StronglyConnectedComponentDecomposition<double> sccDecomposition;
ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*dtmc, true, false));

Write Preview
Loading…
Cancel
Save