diff --git a/resources/cudaForStorm/srcCuda/basicValueIteration.cu b/resources/cudaForStorm/srcCuda/basicValueIteration.cu index b7a879e8b..33ee6218c 100644 --- a/resources/cudaForStorm/srcCuda/basicValueIteration.cu +++ b/resources/cudaForStorm/srcCuda/basicValueIteration.cu @@ -57,7 +57,7 @@ void exploadVector(std::vector> const& inputVect } template -void basicValueIteration_mvReduce(uint_fast64_t const maxIterationCount, ValueType const precision, std::vector const& matrixRowIndices, std::vector> const& columnIndicesAndValues, std::vector& x, std::vector const& b, std::vector const& nondeterministicChoiceIndices) { +void basicValueIteration_mvReduce(uint_fast64_t const maxIterationCount, ValueType const precision, std::vector const& matrixRowIndices, std::vector> const& columnIndicesAndValues, std::vector& x, std::vector const& b, std::vector const& nondeterministicChoiceIndices) { //std::vector matrixColumnIndices; //std::vector matrixValues; //exploadVector(columnIndicesAndValues, matrixColumnIndices, matrixValues); @@ -305,7 +305,7 @@ cleanup: } template -void basicValueIteration_spmv(uint_fast64_t const matrixColCount, std::vector const& matrixRowIndices, std::vector> const& columnIndicesAndValues, std::vector const& x, std::vector& b) { +void basicValueIteration_spmv(uint_fast64_t const matrixColCount, std::vector const& matrixRowIndices, std::vector> const& columnIndicesAndValues, std::vector const& x, std::vector& 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 const& matrixRowIndices, std::vector> const& columnIndicesAndValues, std::vector const& x, std::vector& b) { +void basicValueIteration_spmv_uint64_double(uint_fast64_t const matrixColCount, std::vector const& matrixRowIndices, std::vector> const& columnIndicesAndValues, std::vector const& x, std::vector& b) { basicValueIteration_spmv(matrixColCount, matrixRowIndices, columnIndicesAndValues, x, b); } @@ -705,7 +705,7 @@ void basicValueIteration_equalModuloPrecision_double_NonRelative(std::vector(x, y, maxElement); } -void basicValueIteration_mvReduce_uint64_double_minimize(uint_fast64_t const maxIterationCount, double const precision, bool const relativePrecisionCheck, std::vector const& matrixRowIndices, std::vector> const& columnIndicesAndValues, std::vector& x, std::vector const& b, std::vector const& nondeterministicChoiceIndices) { +void basicValueIteration_mvReduce_uint64_double_minimize(uint_fast64_t const maxIterationCount, double const precision, bool const relativePrecisionCheck, std::vector const& matrixRowIndices, std::vector> const& columnIndicesAndValues, std::vector& x, std::vector const& b, std::vector const& nondeterministicChoiceIndices) { if (relativePrecisionCheck) { basicValueIteration_mvReduce(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 const& matrixRowIndices, std::vector> const& columnIndicesAndValues, std::vector& x, std::vector const& b, std::vector const& nondeterministicChoiceIndices) { +void basicValueIteration_mvReduce_uint64_double_maximize(uint_fast64_t const maxIterationCount, double const precision, bool const relativePrecisionCheck, std::vector const& matrixRowIndices, std::vector> const& columnIndicesAndValues, std::vector& x, std::vector const& b, std::vector const& nondeterministicChoiceIndices) { if (relativePrecisionCheck) { basicValueIteration_mvReduce(maxIterationCount, precision, matrixRowIndices, columnIndicesAndValues, x, b, nondeterministicChoiceIndices); } else { diff --git a/resources/cudaForStorm/srcCuda/basicValueIteration.h b/resources/cudaForStorm/srcCuda/basicValueIteration.h index f23cbec28..1f1f88060 100644 --- a/resources/cudaForStorm/srcCuda/basicValueIteration.h +++ b/resources/cudaForStorm/srcCuda/basicValueIteration.h @@ -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 + 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&& 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 const& getColumnValuePair() const; + + private: + // The actual matrix entry. + std::pair 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 const& matrixRowIndices, std::vector> const& columnIndicesAndValues, std::vector& x, std::vector const& b, std::vector const& nondeterministicChoiceIndices); -cudaForStorm_EXPORT void basicValueIteration_mvReduce_uint64_double_maximize(uint_fast64_t const maxIterationCount, double const precision, bool const relativePrecisionCheck, std::vector const& matrixRowIndices, std::vector> const& columnIndicesAndValues, std::vector& x, std::vector const& b, std::vector const& nondeterministicChoiceIndices); -cudaForStorm_EXPORT void basicValueIteration_spmv_uint64_double(uint_fast64_t const matrixColCount, std::vector const& matrixRowIndices, std::vector> const& columnIndicesAndValues, std::vector const& x, std::vector& b); +cudaForStorm_EXPORT void basicValueIteration_mvReduce_uint64_double_minimize(uint_fast64_t const maxIterationCount, double const precision, bool const relativePrecisionCheck, std::vector const& matrixRowIndices, std::vector> const& columnIndicesAndValues, std::vector& x, std::vector const& b, std::vector const& nondeterministicChoiceIndices); +cudaForStorm_EXPORT void basicValueIteration_mvReduce_uint64_double_maximize(uint_fast64_t const maxIterationCount, double const precision, bool const relativePrecisionCheck, std::vector const& matrixRowIndices, std::vector> const& columnIndicesAndValues, std::vector& x, std::vector const& b, std::vector const& nondeterministicChoiceIndices); +cudaForStorm_EXPORT void basicValueIteration_spmv_uint64_double(uint_fast64_t const matrixColCount, std::vector const& matrixRowIndices, std::vector> const& columnIndicesAndValues, std::vector const& x, std::vector& b); cudaForStorm_EXPORT void basicValueIteration_addVectorsInplace_double(std::vector& a, std::vector const& b); cudaForStorm_EXPORT void basicValueIteration_reduceGroupedVector_uint64_double_minimize(std::vector const& groupedVector, std::vector const& grouping, std::vector& targetVector); cudaForStorm_EXPORT void basicValueIteration_reduceGroupedVector_uint64_double_maximize(std::vector const& groupedVector, std::vector const& grouping, std::vector& targetVector); diff --git a/src/models/PseudoModel.cpp b/src/models/PseudoModel.cpp index 37749a873..7f26e4f36 100644 --- a/src/models/PseudoModel.cpp +++ b/src/models/PseudoModel.cpp @@ -80,7 +80,7 @@ namespace storm { boost::container::flat_set 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) { diff --git a/src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp b/src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp index 84507912e..dce426ec2 100644 --- a/src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp +++ b/src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp @@ -94,7 +94,7 @@ namespace storm { std::vector 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::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; diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index cf19ef98e..c300e6858 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -931,7 +931,7 @@ namespace storm { * Returns a reference to the internal columnMapping vector */ template - std::vector> const& SparseMatrix::__internal_getColumnsAndValues() { + std::vector> const& SparseMatrix::__internal_getColumnsAndValues() { return this->columnsAndValues; } diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index 277ed069f..a06fbeb60 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -732,7 +732,7 @@ namespace storm { /*! * Returns a reference to the internal columnMapping vector */ - std::vector> const& __internal_getColumnsAndValues(); + std::vector> const& __internal_getColumnsAndValues(); private: /*! * Creates a submatrix of the current matrix by keeping only row groups and columns in the given row group diff --git a/src/utility/graph.h b/src/utility/graph.h index 32f311304..5fac4d29a 100644 --- a/src/utility/graph.h +++ b/src/utility/graph.h @@ -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; } diff --git a/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp index 811b9532d..e125b09a2 100644 --- a/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp @@ -10,13 +10,8 @@ #include "storm-config.h" TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) { - storm::settings::Settings* s = storm::settings::Settings::getInstance(); - storm::parser::AutoParser 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 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> mdp = parser.getModel>(); + storm::settings::Settings* s = storm::settings::Settings::getInstance(); + std::shared_ptr> 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>(); 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 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> stateRewardMdp = stateRewardParser.getModel>(); + std::shared_ptr> 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::modelchecker::prctl::TopologicalValueIterationMdpPrctlModelChecker 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 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> stateAndTransitionRewardMdp = stateAndTransitionRewardParser.getModel>(); + std::shared_ptr> 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::modelchecker::prctl::TopologicalValueIterationMdpPrctlModelChecker stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp); @@ -180,11 +165,7 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) { TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, AsynchronousLeader) { storm::settings::Settings* s = storm::settings::Settings::getInstance(); - storm::parser::AutoParser 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> mdp = parser.getModel>(); + std::shared_ptr> 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>(); ASSERT_EQ(mdp->getNumberOfStates(), 3172ull); ASSERT_EQ(mdp->getNumberOfTransitions(), 7144ull); diff --git a/test/functional/storage/StronglyConnectedComponentDecompositionTest.cpp b/test/functional/storage/StronglyConnectedComponentDecompositionTest.cpp index bc3585fc2..6f3d7876f 100644 --- a/test/functional/storage/StronglyConnectedComponentDecompositionTest.cpp +++ b/test/functional/storage/StronglyConnectedComponentDecompositionTest.cpp @@ -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 parser(STORM_CPP_BASE_PATH "/examples/dtmc/scc/scc.tra", STORM_CPP_BASE_PATH "/examples/dtmc/scc/scc.lab", "", ""); - std::shared_ptr> dtmc = parser.getModel>(); + std::shared_ptr> 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::storage::StronglyConnectedComponentDecomposition sccDecomposition; ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(*dtmc, true, false));