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

Updated cudaForStorm/CMakeLists.txt to make use of the new GIT based version schema. 

Added version functions to the Cuda Plugin.
Edited storm.cpp to show version infos for the CUDA Plugin.
Fixed a critical error in basicValueIteration.cu which causes random SEGFAULTs... :P
Streamlined the TopologicalValueIterationNondeterministicLinearEquationSolver.cpp. The SCC group optimizer now returns flat_sets instead of a vector as the sets are ordered, which is required for the Solver to work.

This is now a stable version of StoRM containing a fully wor


Former-commit-id: 47d5c2825c
main
PBerger 11 years ago
parent
05814f5d73
commit
0922921b24
11 changed files with 157 additions and 100 deletions
Unified View
  1. 20
      resources/cudaForStorm/CMakeLists.txt
  2. 1
      resources/cudaForStorm/srcCuda/allCudaKernels.h
  3. 4
      resources/cudaForStorm/srcCuda/basicValueIteration.cu
  4. 2
      resources/cudaForStorm/srcCuda/cudaForStorm.h
  5. 28
      resources/cudaForStorm/srcCuda/version.cu
  6. 16
      resources/cudaForStorm/srcCuda/version.h
  7. 8
      resources/cudaForStorm/storm-cudaplugin-config.h.in
  8. 109
      src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp
  9. 2
      src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.h
  10. 17
      src/storm.cpp
  11. 38
      test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp

20
resources/cudaForStorm/CMakeLists.txt
View File

@ -131,6 +131,26 @@ else()
message(FATAL_ERROR "StoRM (CudaPlugin) - Result of Type Alignment Check: FAILED (Code ${STORM_CUDA_RUN_RESULT_TYPEALIGNMENT})") message(FATAL_ERROR "StoRM (CudaPlugin) - Result of Type Alignment Check: FAILED (Code ${STORM_CUDA_RUN_RESULT_TYPEALIGNMENT})")
endif() endif()
#
# Make a version file containing the current version from git.
#
include(GetGitRevisionDescription)
git_describe_checkout(STORM_GIT_VERSION_STRING)
# Parse the git Tag into variables
string(REGEX REPLACE "^([0-9]+)\\..*" "\\1" STORM_CUDAPLUGIN_VERSION_MAJOR "${STORM_GIT_VERSION_STRING}")
string(REGEX REPLACE "^[0-9]+\\.([0-9]+).*" "\\1" STORM_CUDAPLUGIN_VERSION_MINOR "${STORM_GIT_VERSION_STRING}")
string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.([0-9]+).*" "\\1" STORM_CUDAPLUGIN_VERSION_PATCH "${STORM_GIT_VERSION_STRING}")
string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.[0-9]+\\-([0-9]+)\\-.*" "\\1" STORM_CUDAPLUGIN_VERSION_COMMITS_AHEAD "${STORM_GIT_VERSION_STRING}")
string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.[0-9]+\\-[0-9]+\\-([a-z0-9]+).*" "\\1" STORM_CUDAPLUGIN_VERSION_HASH "${STORM_GIT_VERSION_STRING}")
string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.[0-9]+\\-[0-9]+\\-[a-z0-9]+\\-(.*)" "\\1" STORM_CUDAPLUGIN_VERSION_APPENDIX "${STORM_GIT_VERSION_STRING}")
if ("${STORM_CUDAPLUGIN_VERSION_APPENDIX}" MATCHES "^.*dirty.*$")
set(STORM_CUDAPLUGIN_VERSION_DIRTY 1)
else()
set(STORM_CUDAPLUGIN_VERSION_DIRTY 0)
endif()
message(STATUS "StoRM (CudaPlugin) - Version information: ${STORM_CUDAPLUGIN_VERSION_MAJOR}.${STORM_CUDAPLUGIN_VERSION_MINOR}.${STORM_CUDAPLUGIN_VERSION_PATCH} (${STORM_CUDAPLUGIN_VERSION_COMMITS_AHEAD} commits ahead of Tag) build from ${STORM_CUDAPLUGIN_VERSION_HASH} (Dirty: ${STORM_CUDAPLUGIN_VERSION_DIRTY})")
# Configure a header file to pass some of the CMake settings to the source code # Configure a header file to pass some of the CMake settings to the source code
configure_file ( configure_file (
"${PROJECT_SOURCE_DIR}/storm-cudaplugin-config.h.in" "${PROJECT_SOURCE_DIR}/storm-cudaplugin-config.h.in"

1
resources/cudaForStorm/srcCuda/allCudaKernels.h
View File

@ -3,3 +3,4 @@
#include "basicAdd.h" #include "basicAdd.h"
#include "kernelSwitchTest.h" #include "kernelSwitchTest.h"
#include "basicValueIteration.h" #include "basicValueIteration.h"
#include "version.h"

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

@ -138,7 +138,7 @@ void basicValueIteration_mvReduce(uint_fast64_t const maxIterationCount, ValueTy
} }
CUDA_CHECK_ALL_ERRORS(); CUDA_CHECK_ALL_ERRORS();
cudaMallocResult = cudaMalloc(reinterpret_cast<void**>(&device_nondeterministicChoiceIndices), sizeof(IndexType) * (matrixRowCount + 1)); cudaMallocResult = cudaMalloc(reinterpret_cast<void**>(&device_nondeterministicChoiceIndices), sizeof(IndexType) * (matrixColCount + 1));
if (cudaMallocResult != cudaSuccess) { if (cudaMallocResult != cudaSuccess) {
std::cout << "Could not allocate memory for Nondeterministic Choice Indices, Error Code " << cudaMallocResult << "." << std::endl; std::cout << "Could not allocate memory for Nondeterministic Choice Indices, Error Code " << cudaMallocResult << "." << std::endl;
goto cleanup; goto cleanup;
@ -203,7 +203,7 @@ void basicValueIteration_mvReduce(uint_fast64_t const maxIterationCount, ValueTy
} }
CUDA_CHECK_ALL_ERRORS(); CUDA_CHECK_ALL_ERRORS();
cudaCopyResult = cudaMemcpy(device_nondeterministicChoiceIndices, nondeterministicChoiceIndices.data(), sizeof(IndexType) * (matrixRowCount + 1), cudaMemcpyHostToDevice); cudaCopyResult = cudaMemcpy(device_nondeterministicChoiceIndices, nondeterministicChoiceIndices.data(), sizeof(IndexType) * (matrixColCount + 1), cudaMemcpyHostToDevice);
if (cudaCopyResult != cudaSuccess) { if (cudaCopyResult != cudaSuccess) {
std::cout << "Could not copy data for Vector b, Error Code " << cudaCopyResult << std::endl; std::cout << "Could not copy data for Vector b, Error Code " << cudaCopyResult << std::endl;
goto cleanup; goto cleanup;

2
resources/cudaForStorm/srcCuda/cudaForStorm.h
View File

@ -11,6 +11,8 @@
// Utility Functions // Utility Functions
#include "srcCuda/utility.h" #include "srcCuda/utility.h"
// Version Information
#include "srcCuda/version.h"

28
resources/cudaForStorm/srcCuda/version.cu
View File

@ -0,0 +1,28 @@
#include "version.h"
#include "storm-cudaplugin-config.h"
size_t getStormCudaPluginVersionMajor() {
return STORM_CUDAPLUGIN_VERSION_MAJOR;
}
size_t getStormCudaPluginVersionMinor() {
return STORM_CUDAPLUGIN_VERSION_MINOR;
}
size_t getStormCudaPluginVersionPatch() {
return STORM_CUDAPLUGIN_VERSION_PATCH;
}
size_t getStormCudaPluginVersionCommitsAhead() {
return STORM_CUDAPLUGIN_VERSION_COMMITS_AHEAD;
}
const char* getStormCudaPluginVersionHash() {
static const std::string versionHash = STORM_CUDAPLUGIN_VERSION_HASH;
return versionHash.c_str();
}
bool getStormCudaPluginVersionIsDirty() {
return ((STORM_CUDAPLUGIN_VERSION_DIRTY) != 0);
}

16
resources/cudaForStorm/srcCuda/version.h
View File

@ -0,0 +1,16 @@
#ifndef STORM_CUDAFORSTORM_VERSION_H_
#define STORM_CUDAFORSTORM_VERSION_H_
// Library exports
#include "cudaForStorm_Export.h"
#include <string>
cudaForStorm_EXPORT size_t getStormCudaPluginVersionMajor();
cudaForStorm_EXPORT size_t getStormCudaPluginVersionMinor();
cudaForStorm_EXPORT size_t getStormCudaPluginVersionPatch();
cudaForStorm_EXPORT size_t getStormCudaPluginVersionCommitsAhead();
cudaForStorm_EXPORT const char* getStormCudaPluginVersionHash();
cudaForStorm_EXPORT bool getStormCudaPluginVersionIsDirty();
#endif // STORM_CUDAFORSTORM_VERSION_H_

8
resources/cudaForStorm/storm-cudaplugin-config.h.in
View File

@ -8,6 +8,12 @@
#ifndef STORM_CUDAPLUGIN_GENERATED_STORMCONFIG_H_ #ifndef STORM_CUDAPLUGIN_GENERATED_STORMCONFIG_H_
#define STORM_CUDAPLUGIN_GENERATED_STORMCONFIG_H_ #define STORM_CUDAPLUGIN_GENERATED_STORMCONFIG_H_
// Version Information
#define STORM_CUDAPLUGIN_VERSION_MAJOR @STORM_CUDAPLUGIN_VERSION_MAJOR@ // The major version of StoRM
#define STORM_CUDAPLUGIN_VERSION_MINOR @STORM_CUDAPLUGIN_VERSION_MINOR@ // The minor version of StoRM
#define STORM_CUDAPLUGIN_VERSION_PATCH @STORM_CUDAPLUGIN_VERSION_PATCH@ // The patch version of StoRM
#define STORM_CUDAPLUGIN_VERSION_COMMITS_AHEAD @STORM_CUDAPLUGIN_VERSION_COMMITS_AHEAD@ // How many commits passed since the tag was last set
#define STORM_CUDAPLUGIN_VERSION_HASH "@STORM_CUDAPLUGIN_VERSION_HASH@" // The short hash of the git commit this build is bases on
#define STORM_CUDAPLUGIN_VERSION_DIRTY @STORM_CUDAPLUGIN_VERSION_DIRTY@ // 0 iff there no files were modified in the checkout, 1 else
#endif // STORM_CUDAPLUGIN_GENERATED_STORMCONFIG_H_ #endif // STORM_CUDAPLUGIN_GENERATED_STORMCONFIG_H_

109
src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp
View File

@ -1,6 +1,7 @@
#include "src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.h" #include "src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.h"
#include <utility> #include <utility>
#include <set>
#include "src/settings/Settings.h" #include "src/settings/Settings.h"
#include "src/utility/vector.h" #include "src/utility/vector.h"
@ -15,7 +16,9 @@
extern log4cplus::Logger logger; extern log4cplus::Logger logger;
#include "storm-config.h" #include "storm-config.h"
#include "cudaForStorm.h" #ifdef STORM_HAVE_CUDAFORSTORM
# include "cudaForStorm.h"
#endif
namespace storm { namespace storm {
namespace solver { namespace solver {
@ -44,12 +47,9 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
void TopologicalValueIterationNondeterministicLinearEquationSolver<ValueType>::solveEquationSystem(bool minimize, storm::storage::SparseMatrix<ValueType> const& A, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult, std::vector<ValueType>* newX) const { void TopologicalValueIterationNondeterministicLinearEquationSolver<ValueType>::solveEquationSystem(bool minimize, storm::storage::SparseMatrix<ValueType> const& A, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult, std::vector<ValueType>* newX) const {
// Now, we need to determine the SCCs of the MDP and a topological sort. // Now, we need to determine the SCCs of the MDP and perform a topological sort.
//std::vector<std::vector<uint_fast64_t>> stronglyConnectedComponents = storm::utility::graph::performSccDecomposition(this->getModel(), stronglyConnectedComponents, stronglyConnectedComponentsDependencyGraph);
//storm::storage::SparseMatrix<T> stronglyConnectedComponentsDependencyGraph = this->getModel().extractSccDependencyGraph(stronglyConnectedComponents);
std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = A.getRowGroupIndices(); std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = A.getRowGroupIndices();
storm::models::NonDeterministicMatrixBasedPseudoModel<ValueType> pseudoModel(A, nondeterministicChoiceIndices); storm::models::NonDeterministicMatrixBasedPseudoModel<ValueType> pseudoModel(A, nondeterministicChoiceIndices);
//storm::storage::StronglyConnectedComponentDecomposition<ValueType> sccDecomposition(*static_cast<storm::models::AbstractPseudoModel<ValueType>*>(&pseudoModel), false, false);
storm::storage::StronglyConnectedComponentDecomposition<ValueType> sccDecomposition(pseudoModel, false, false); storm::storage::StronglyConnectedComponentDecomposition<ValueType> sccDecomposition(pseudoModel, false, false);
if (sccDecomposition.size() == 0) { if (sccDecomposition.size() == 0) {
@ -61,20 +61,10 @@ namespace storm {
std::vector<uint_fast64_t> topologicalSort = storm::utility::graph::getTopologicalSort(stronglyConnectedComponentsDependencyGraph); std::vector<uint_fast64_t> topologicalSort = storm::utility::graph::getTopologicalSort(stronglyConnectedComponentsDependencyGraph);
// Calculate the optimal distribution of sccs // Calculate the optimal distribution of sccs
std::vector<std::pair<bool, std::vector<uint_fast64_t>>> optimalSccs = this->getOptimalGroupingFromTopologicalSccDecomposition(sccDecomposition, topologicalSort, A); std::vector<std::pair<bool, storm::storage::StateBlock>> optimalSccs = this->getOptimalGroupingFromTopologicalSccDecomposition(sccDecomposition, topologicalSort, A);
LOG4CPLUS_INFO(logger, "Optimized SCC Decomposition, originally " << topologicalSort.size() << " SCCs, optimized to " << optimalSccs.size() << " SCCs.");
// Set up the environment for the power method.
// bool multiplyResultMemoryProvided = true;
// if (multiplyResult == nullptr) {
// multiplyResult = new std::vector<ValueType>(A.getRowCount());
// multiplyResultMemoryProvided = false;
// }
std::vector<ValueType>* currentX = nullptr; std::vector<ValueType>* currentX = nullptr;
//bool xMemoryProvided = true;
//if (newX == nullptr) {
// newX = new std::vector<ValueType>(x.size());
// xMemoryProvided = false;
//}
std::vector<ValueType>* swap = nullptr; std::vector<ValueType>* swap = nullptr;
uint_fast64_t currentMaxLocalIterations = 0; uint_fast64_t currentMaxLocalIterations = 0;
uint_fast64_t localIterations = 0; uint_fast64_t localIterations = 0;
@ -87,7 +77,7 @@ namespace storm {
for (auto sccIndexIt = optimalSccs.cbegin(); sccIndexIt != optimalSccs.cend() && converged; ++sccIndexIt) { for (auto sccIndexIt = optimalSccs.cbegin(); sccIndexIt != optimalSccs.cend() && converged; ++sccIndexIt) {
bool const useGpu = sccIndexIt->first; bool const useGpu = sccIndexIt->first;
std::vector <uint_fast64_t> const& scc = sccIndexIt->second; storm::storage::StateBlock const& scc = sccIndexIt->second;
// Generate a submatrix // Generate a submatrix
storm::storage::BitVector subMatrixIndices(A.getColumnCount(), scc.cbegin(), scc.cend()); storm::storage::BitVector subMatrixIndices(A.getColumnCount(), scc.cbegin(), scc.cend());
@ -140,63 +130,16 @@ namespace storm {
LOG4CPLUS_INFO(logger, "We will allocate " << (sizeof(uint_fast64_t)* sccSubmatrix.rowIndications.size() + sizeof(uint_fast64_t)* sccSubmatrix.columnsAndValues.size() * 2 + sizeof(double)* sccSubX.size() + sizeof(double)* sccSubX.size() + sizeof(double)* sccSubB.size() + sizeof(double)* sccSubB.size() + sizeof(uint_fast64_t)* sccSubNondeterministicChoiceIndices.size()) << " Bytes."); LOG4CPLUS_INFO(logger, "We will allocate " << (sizeof(uint_fast64_t)* sccSubmatrix.rowIndications.size() + sizeof(uint_fast64_t)* sccSubmatrix.columnsAndValues.size() * 2 + sizeof(double)* sccSubX.size() + sizeof(double)* sccSubX.size() + sizeof(double)* sccSubB.size() + sizeof(double)* sccSubB.size() + sizeof(uint_fast64_t)* sccSubNondeterministicChoiceIndices.size()) << " Bytes.");
LOG4CPLUS_INFO(logger, "The CUDA Runtime Version is " << getRuntimeCudaVersion()); LOG4CPLUS_INFO(logger, "The CUDA Runtime Version is " << getRuntimeCudaVersion());
std::vector<ValueType> copyX(*currentX);
if (minimize) { if (minimize) {
basicValueIteration_mvReduce_uint64_double_minimize(this->maximalNumberOfIterations, this->precision, this->relative, sccSubmatrix.rowIndications, sccSubmatrix.columnsAndValues, copyX, sccSubB, sccSubNondeterministicChoiceIndices); basicValueIteration_mvReduce_uint64_double_minimize(this->maximalNumberOfIterations, this->precision, this->relative, sccSubmatrix.rowIndications, sccSubmatrix.columnsAndValues, *currentX, sccSubB, sccSubNondeterministicChoiceIndices);
} }
else { else {
basicValueIteration_mvReduce_uint64_double_maximize(this->maximalNumberOfIterations, this->precision, this->relative, sccSubmatrix.rowIndications, sccSubmatrix.columnsAndValues, copyX, sccSubB, sccSubNondeterministicChoiceIndices); basicValueIteration_mvReduce_uint64_double_maximize(this->maximalNumberOfIterations, this->precision, this->relative, sccSubmatrix.rowIndications, sccSubmatrix.columnsAndValues, *currentX, sccSubB, sccSubNondeterministicChoiceIndices);
} }
converged = true; converged = true;
#else
// DEBUG LOG4CPLUS_ERROR(logger, "The useGpu Flag of a SCC was set, but this version of StoRM does not support CUDA acceleration. Internal Error!");
localIterations = 0; throw storm::exceptions::InvalidStateException() << "The useGpu Flag of a SCC was set, but this version of StoRM does not support CUDA acceleration. Internal Error!";
converged = false;
while (!converged && localIterations < this->maximalNumberOfIterations) {
// Compute x' = A*x + b.
sccSubmatrix.multiplyWithVector(*currentX, sccMultiplyResult);
storm::utility::vector::addVectorsInPlace<ValueType>(sccMultiplyResult, sccSubB);
//A.multiplyWithVector(scc, nondeterministicChoiceIndices, *currentX, multiplyResult);
//storm::utility::addVectors(scc, nondeterministicChoiceIndices, multiplyResult, b);
/*
Versus:
A.multiplyWithVector(*currentX, *multiplyResult);
storm::utility::vector::addVectorsInPlace(*multiplyResult, b);
*/
// Reduce the vector x' by applying min/max for all non-deterministic choices.
if (minimize) {
storm::utility::vector::reduceVectorMin<ValueType>(sccMultiplyResult, *swap, sccSubNondeterministicChoiceIndices);
}
else {
storm::utility::vector::reduceVectorMax<ValueType>(sccMultiplyResult, *swap, sccSubNondeterministicChoiceIndices);
}
// Determine whether the method converged.
// TODO: It seems that the equalModuloPrecision call that compares all values should have a higher
// running time. In fact, it is faster. This has to be investigated.
// converged = storm::utility::equalModuloPrecision(*currentX, *newX, scc, precision, relative);
converged = storm::utility::vector::equalModuloPrecision<ValueType>(*currentX, *swap, this->precision, this->relative);
// Update environment variables.
std::swap(currentX, swap);
++localIterations;
++globalIterations;
}
LOG4CPLUS_INFO(logger, "Executed " << localIterations << " of max. " << maximalNumberOfIterations << " Iterations.");
uint_fast64_t diffCount = 0;
for (size_t i = 0; i < currentX->size(); ++i) {
if (currentX->at(i) != copyX.at(i)) {
LOG4CPLUS_WARN(logger, "CUDA solution differs on index " << i << " diff. " << std::abs(currentX->at(i) - copyX.at(i)) << ", CPU: " << currentX->at(i) << ", CUDA: " << copyX.at(i));
std::cout << "CUDA solution differs on index " << i << " diff. " << std::abs(currentX->at(i) - copyX.at(i)) << ", CPU: " << currentX->at(i) << ", CUDA: " << copyX.at(i) << std::endl;
++diffCount;
}
}
std::cout << "CUDA solution differed in " << diffCount << " of " << currentX->size() << " values." << std::endl;
#endif #endif
} else { } else {
localIterations = 0; localIterations = 0;
@ -257,14 +200,6 @@ namespace storm {
} }
} }
//if (!xMemoryProvided) {
// delete newX;
//}
// if (!multiplyResultMemoryProvided) {
// delete multiplyResult;
// }
// Check if the solver converged and issue a warning otherwise. // Check if the solver converged and issue a warning otherwise.
if (converged) { if (converged) {
LOG4CPLUS_INFO(logger, "Iterative solver converged after " << currentMaxLocalIterations << " iterations."); LOG4CPLUS_INFO(logger, "Iterative solver converged after " << currentMaxLocalIterations << " iterations.");
@ -275,9 +210,9 @@ namespace storm {
} }
template<typename ValueType> template<typename ValueType>
std::vector<std::pair<bool, std::vector<uint_fast64_t>>> std::vector<std::pair<bool, storm::storage::StateBlock>>
TopologicalValueIterationNondeterministicLinearEquationSolver<ValueType>::getOptimalGroupingFromTopologicalSccDecomposition(storm::storage::StronglyConnectedComponentDecomposition<ValueType> const& sccDecomposition, std::vector<uint_fast64_t> const& topologicalSort, storm::storage::SparseMatrix<ValueType> const& matrix) const { TopologicalValueIterationNondeterministicLinearEquationSolver<ValueType>::getOptimalGroupingFromTopologicalSccDecomposition(storm::storage::StronglyConnectedComponentDecomposition<ValueType> const& sccDecomposition, std::vector<uint_fast64_t> const& topologicalSort, storm::storage::SparseMatrix<ValueType> const& matrix) const {
std::vector<std::pair<bool, std::vector<uint_fast64_t>>> result; std::vector<std::pair<bool, storm::storage::StateBlock>> result;
#ifdef STORM_HAVE_CUDAFORSTORM #ifdef STORM_HAVE_CUDAFORSTORM
// 95% to have a bit of padding // 95% to have a bit of padding
size_t const cudaFreeMemory = static_cast<size_t>(getFreeCudaMemory() * 0.95); size_t const cudaFreeMemory = static_cast<size_t>(getFreeCudaMemory() * 0.95);
@ -290,13 +225,13 @@ namespace storm {
uint_fast64_t rowCount = 0; uint_fast64_t rowCount = 0;
uint_fast64_t entryCount = 0; uint_fast64_t entryCount = 0;
std::vector<uint_fast64_t> rowGroups; storm::storage::StateBlock rowGroups;
rowGroups.reserve(scc.size()); rowGroups.reserve(scc.size());
for (auto sccIt = scc.cbegin(); sccIt != scc.cend(); ++sccIt) { for (auto sccIt = scc.cbegin(); sccIt != scc.cend(); ++sccIt) {
rowCount += matrix.getRowGroupSize(*sccIt); rowCount += matrix.getRowGroupSize(*sccIt);
entryCount += matrix.getRowGroupEntryCount(*sccIt); entryCount += matrix.getRowGroupEntryCount(*sccIt);
rowGroups.push_back(*sccIt); rowGroups.insert(*sccIt);
} }
size_t sccSize = basicValueIteration_mvReduce_uint64_double_calculateMemorySize(static_cast<size_t>(rowCount), scc.size(), static_cast<size_t>(entryCount)); size_t sccSize = basicValueIteration_mvReduce_uint64_double_calculateMemorySize(static_cast<size_t>(rowCount), scc.size(), static_cast<size_t>(entryCount));
@ -308,7 +243,7 @@ namespace storm {
result.push_back(std::make_pair(true, rowGroups)); result.push_back(std::make_pair(true, rowGroups));
} }
else { else {
result[lastResultIndex].second.insert(result[lastResultIndex].second.end(), rowGroups.begin(), rowGroups.end()); result[lastResultIndex].second.insert(rowGroups.begin(), rowGroups.end());
} }
currentSize += sccSize; currentSize += sccSize;
} }
@ -329,12 +264,12 @@ namespace storm {
#else #else
for (auto sccIndexIt = topologicalSort.cbegin(); sccIndexIt != topologicalSort.cend(); ++sccIndexIt) { for (auto sccIndexIt = topologicalSort.cbegin(); sccIndexIt != topologicalSort.cend(); ++sccIndexIt) {
storm::storage::StateBlock const& scc = sccDecomposition[*sccIndexIt]; storm::storage::StateBlock const& scc = sccDecomposition[*sccIndexIt];
std::vector<uint_fast64_t> rowGroups; storm::storage::StateBlock rowGroups;
rowGroups.reserve(scc.size()); rowGroups.reserve(scc.size());
for (auto sccIt = scc.cbegin(); sccIt != scc.cend(); ++sccIt) { for (auto sccIt = scc.cbegin(); sccIt != scc.cend(); ++sccIt) {
rowGroups.push_back(*sccIt); rowGroups.insert(*sccIt);
result.push_back(std::make_pair(false, rowGroups));
} }
result.push_back(std::make_pair(false, rowGroups));
} }
#endif #endif
return result; return result;

2
src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.h
View File

@ -40,7 +40,7 @@ namespace storm {
/*! /*!
* Given a topological sort of a SCC Decomposition, this will calculate the optimal grouping of SCCs with respect to the size of the GPU memory. * Given a topological sort of a SCC Decomposition, this will calculate the optimal grouping of SCCs with respect to the size of the GPU memory.
*/ */
std::vector<std::pair<bool, std::vector<uint_fast64_t>>> getOptimalGroupingFromTopologicalSccDecomposition(storm::storage::StronglyConnectedComponentDecomposition<ValueType> const& sccDecomposition, std::vector<uint_fast64_t> const& topologicalSort, storm::storage::SparseMatrix<ValueType> const& matrix) const; std::vector<std::pair<bool, storm::storage::StateBlock>> getOptimalGroupingFromTopologicalSccDecomposition(storm::storage::StronglyConnectedComponentDecomposition<ValueType> const& sccDecomposition, std::vector<uint_fast64_t> const& topologicalSort, storm::storage::SparseMatrix<ValueType> const& matrix) const;
}; };
} // namespace solver } // namespace solver
} // namespace storm } // namespace storm

17
src/storm.cpp
View File

@ -75,6 +75,9 @@
#ifdef STORM_HAVE_Z3 #ifdef STORM_HAVE_Z3
# include "z3.h" # include "z3.h"
#endif #endif
#ifdef STORM_HAVE_CUDAFORSTORM
# include "cudaForStorm.h"
#endif
#include <iostream> #include <iostream>
#include <iomanip> #include <iomanip>
@ -173,8 +176,20 @@ void printHeader(const int argc, const char* argv[]) {
if (STORM_CPP_VERSION_DIRTY == 1) { if (STORM_CPP_VERSION_DIRTY == 1) {
std::cout << " (DIRTY)"; std::cout << " (DIRTY)";
} }
std::cout << std::endl; std::cout << "." << std::endl;
#ifdef STORM_HAVE_CUDAFORSTORM
std::cout << "Compiled with Runtime Support for the StoRM CUDA Plugin." << std::endl;
std::cout << "Detected the StoRM CUDA Plugin in Version " << getStormCudaPluginVersionMajor() << "." << getStormCudaPluginVersionMinor() << "." << getStormCudaPluginVersionPatch();
if (getStormCudaPluginVersionCommitsAhead() != 0) {
std::cout << " (+" << getStormCudaPluginVersionCommitsAhead() << " commits)";
}
std::cout << " build from revision " << getStormCudaPluginVersionHash();
if (getStormCudaPluginVersionIsDirty()) {
std::cout << " (DIRTY)";
}
std::cout << "." << std::endl;
#endif
#ifdef STORM_HAVE_INTELTBB #ifdef STORM_HAVE_INTELTBB
std::cout << "Linked with Intel Threading Building Blocks v" << TBB_VERSION_MAJOR << "." << TBB_VERSION_MINOR << " (Interface version " << TBB_INTERFACE_VERSION << ")." << std::endl; std::cout << "Linked with Intel Threading Building Blocks v" << TBB_VERSION_MAJOR << "." << TBB_VERSION_MINOR << " (Interface version " << TBB_INTERFACE_VERSION << ")." << std::endl;
#endif #endif

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

@ -7,6 +7,8 @@
#include "src/modelchecker/prctl/TopologicalValueIterationMdpPrctlModelChecker.h" #include "src/modelchecker/prctl/TopologicalValueIterationMdpPrctlModelChecker.h"
#include "src/parser/AutoParser.h" #include "src/parser/AutoParser.h"
#include "storm-config.h"
TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) { TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) {
storm::settings::Settings* s = storm::settings::Settings::getInstance(); 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/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");
@ -87,7 +89,11 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) {
result = mc.checkNoBoundOperator(*rewardFormula); result = mc.checkNoBoundOperator(*rewardFormula);
#ifdef STORM_HAVE_CUDAFORSTORM
ASSERT_LT(std::abs(result[0] - 7.333329499), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
#else
ASSERT_LT(std::abs(result[0] - 7.33332904), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); ASSERT_LT(std::abs(result[0] - 7.33332904), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
#endif
delete rewardFormula; delete rewardFormula;
apFormula = new storm::property::prctl::Ap<double>("done"); apFormula = new storm::property::prctl::Ap<double>("done");
@ -96,7 +102,11 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) {
result = mc.checkNoBoundOperator(*rewardFormula);; result = mc.checkNoBoundOperator(*rewardFormula);;
#ifdef STORM_HAVE_CUDAFORSTORM
ASSERT_LT(std::abs(result[0] - 7.333329499), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
#else
ASSERT_LT(std::abs(result[0] - 7.33333151), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); ASSERT_LT(std::abs(result[0] - 7.33333151), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
#endif
delete rewardFormula; 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", ""); 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", "");
@ -113,7 +123,11 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) {
result = stateRewardModelChecker.checkNoBoundOperator(*rewardFormula); result = stateRewardModelChecker.checkNoBoundOperator(*rewardFormula);
#ifdef STORM_HAVE_CUDAFORSTORM
ASSERT_LT(std::abs(result[0] - 7.333329499), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
#else
ASSERT_LT(std::abs(result[0] - 7.33332904), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); ASSERT_LT(std::abs(result[0] - 7.33332904), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
#endif
delete rewardFormula; delete rewardFormula;
apFormula = new storm::property::prctl::Ap<double>("done"); apFormula = new storm::property::prctl::Ap<double>("done");
@ -122,7 +136,11 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) {
result = stateRewardModelChecker.checkNoBoundOperator(*rewardFormula); result = stateRewardModelChecker.checkNoBoundOperator(*rewardFormula);
#ifdef STORM_HAVE_CUDAFORSTORM
ASSERT_LT(std::abs(result[0] - 7.333329499), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
#else
ASSERT_LT(std::abs(result[0] - 7.33333151), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); ASSERT_LT(std::abs(result[0] - 7.33333151), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
#endif
delete rewardFormula; 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"); 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");
@ -139,7 +157,11 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) {
result = stateAndTransitionRewardModelChecker.checkNoBoundOperator(*rewardFormula); result = stateAndTransitionRewardModelChecker.checkNoBoundOperator(*rewardFormula);
#ifdef STORM_HAVE_CUDAFORSTORM
ASSERT_LT(std::abs(result[0] - 14.666658998), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
#else
ASSERT_LT(std::abs(result[0] - 14.6666581), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); ASSERT_LT(std::abs(result[0] - 14.6666581), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
#endif
delete rewardFormula; delete rewardFormula;
apFormula = new storm::property::prctl::Ap<double>("done"); apFormula = new storm::property::prctl::Ap<double>("done");
@ -148,7 +170,11 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) {
result = stateAndTransitionRewardModelChecker.checkNoBoundOperator(*rewardFormula); result = stateAndTransitionRewardModelChecker.checkNoBoundOperator(*rewardFormula);
#ifdef STORM_HAVE_CUDAFORSTORM
ASSERT_LT(std::abs(result[0] - 14.666658998), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
#else
ASSERT_LT(std::abs(result[0] - 14.666663), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); ASSERT_LT(std::abs(result[0] - 14.666663), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
#endif
delete rewardFormula; delete rewardFormula;
} }
@ -209,17 +235,25 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, AsynchronousLeader) {
storm::property::prctl::ReachabilityReward<double>* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula); storm::property::prctl::ReachabilityReward<double>* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
storm::property::prctl::RewardNoBoundOperator<double>* rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, true); storm::property::prctl::RewardNoBoundOperator<double>* rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, true);
result = mc.checkNoBoundOperator(*rewardFormula);; result = mc.checkNoBoundOperator(*rewardFormula);
#ifdef STORM_HAVE_CUDAFORSTORM
ASSERT_LT(std::abs(result[0] - 4.285689611), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); ASSERT_LT(std::abs(result[0] - 4.285689611), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
#else
ASSERT_LT(std::abs(result[0] - 4.285701547), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
#endif
delete rewardFormula; delete rewardFormula;
apFormula = new storm::property::prctl::Ap<double>("elected"); apFormula = new storm::property::prctl::Ap<double>("elected");
reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula); reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, false); rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, false);
result = mc.checkNoBoundOperator(*rewardFormula);; result = mc.checkNoBoundOperator(*rewardFormula);
#ifdef STORM_HAVE_CUDAFORSTORM
ASSERT_LT(std::abs(result[0] - 4.285689611), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); ASSERT_LT(std::abs(result[0] - 4.285689611), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
#else
ASSERT_LT(std::abs(result[0] - 4.285703591), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
#endif
delete rewardFormula; delete rewardFormula;
} }
Write Preview
|||||||
100:0
Loading…
Cancel
Save