From 0922921b24a0331f4170a475780e32c1caec334f Mon Sep 17 00:00:00 2001 From: PBerger Date: Mon, 17 Mar 2014 05:44:15 +0100 Subject: [PATCH] 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: 47d5c2825caafacb361a6d20f73a8db1567f6eba --- resources/cudaForStorm/CMakeLists.txt | 22 +++- .../cudaForStorm/srcCuda/allCudaKernels.h | 3 +- .../srcCuda/basicValueIteration.cu | 4 +- resources/cudaForStorm/srcCuda/cudaForStorm.h | 2 + resources/cudaForStorm/srcCuda/version.cu | 28 +++++ resources/cudaForStorm/srcCuda/version.h | 16 +++ .../cudaForStorm/storm-cudaplugin-config.h.in | 8 +- ...onNondeterministicLinearEquationSolver.cpp | 109 ++++-------------- ...tionNondeterministicLinearEquationSolver.h | 2 +- src/storm.cpp | 19 ++- ...ValueIterationMdpPrctlModelCheckerTest.cpp | 44 ++++++- 11 files changed, 157 insertions(+), 100 deletions(-) create mode 100644 resources/cudaForStorm/srcCuda/version.cu create mode 100644 resources/cudaForStorm/srcCuda/version.h diff --git a/resources/cudaForStorm/CMakeLists.txt b/resources/cudaForStorm/CMakeLists.txt index 6b0496d51..7bc37a097 100644 --- a/resources/cudaForStorm/CMakeLists.txt +++ b/resources/cudaForStorm/CMakeLists.txt @@ -130,7 +130,27 @@ elseif(STORM_CUDA_RUN_RESULT_TYPEALIGNMENT EQUAL 0) else() message(FATAL_ERROR "StoRM (CudaPlugin) - Result of Type Alignment Check: FAILED (Code ${STORM_CUDA_RUN_RESULT_TYPEALIGNMENT})") 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_file ( "${PROJECT_SOURCE_DIR}/storm-cudaplugin-config.h.in" diff --git a/resources/cudaForStorm/srcCuda/allCudaKernels.h b/resources/cudaForStorm/srcCuda/allCudaKernels.h index 182f1b770..50bf92191 100644 --- a/resources/cudaForStorm/srcCuda/allCudaKernels.h +++ b/resources/cudaForStorm/srcCuda/allCudaKernels.h @@ -2,4 +2,5 @@ #include "bandWidth.h" #include "basicAdd.h" #include "kernelSwitchTest.h" -#include "basicValueIteration.h" \ No newline at end of file +#include "basicValueIteration.h" +#include "version.h" \ No newline at end of file diff --git a/resources/cudaForStorm/srcCuda/basicValueIteration.cu b/resources/cudaForStorm/srcCuda/basicValueIteration.cu index ff93d29b6..231c6c4be 100644 --- a/resources/cudaForStorm/srcCuda/basicValueIteration.cu +++ b/resources/cudaForStorm/srcCuda/basicValueIteration.cu @@ -138,7 +138,7 @@ void basicValueIteration_mvReduce(uint_fast64_t const maxIterationCount, ValueTy } CUDA_CHECK_ALL_ERRORS(); - cudaMallocResult = cudaMalloc(reinterpret_cast(&device_nondeterministicChoiceIndices), sizeof(IndexType) * (matrixRowCount + 1)); + cudaMallocResult = cudaMalloc(reinterpret_cast(&device_nondeterministicChoiceIndices), sizeof(IndexType) * (matrixColCount + 1)); if (cudaMallocResult != cudaSuccess) { std::cout << "Could not allocate memory for Nondeterministic Choice Indices, Error Code " << cudaMallocResult << "." << std::endl; goto cleanup; @@ -203,7 +203,7 @@ void basicValueIteration_mvReduce(uint_fast64_t const maxIterationCount, ValueTy } 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) { std::cout << "Could not copy data for Vector b, Error Code " << cudaCopyResult << std::endl; goto cleanup; diff --git a/resources/cudaForStorm/srcCuda/cudaForStorm.h b/resources/cudaForStorm/srcCuda/cudaForStorm.h index fdc484eaa..2ea39c2d0 100644 --- a/resources/cudaForStorm/srcCuda/cudaForStorm.h +++ b/resources/cudaForStorm/srcCuda/cudaForStorm.h @@ -11,6 +11,8 @@ // Utility Functions #include "srcCuda/utility.h" +// Version Information +#include "srcCuda/version.h" diff --git a/resources/cudaForStorm/srcCuda/version.cu b/resources/cudaForStorm/srcCuda/version.cu new file mode 100644 index 000000000..3850c895c --- /dev/null +++ b/resources/cudaForStorm/srcCuda/version.cu @@ -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); +} \ No newline at end of file diff --git a/resources/cudaForStorm/srcCuda/version.h b/resources/cudaForStorm/srcCuda/version.h new file mode 100644 index 000000000..de3f4f16c --- /dev/null +++ b/resources/cudaForStorm/srcCuda/version.h @@ -0,0 +1,16 @@ +#ifndef STORM_CUDAFORSTORM_VERSION_H_ +#define STORM_CUDAFORSTORM_VERSION_H_ + +// Library exports +#include "cudaForStorm_Export.h" + +#include + +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_ \ No newline at end of file diff --git a/resources/cudaForStorm/storm-cudaplugin-config.h.in b/resources/cudaForStorm/storm-cudaplugin-config.h.in index d59532a6c..1cfc9119e 100644 --- a/resources/cudaForStorm/storm-cudaplugin-config.h.in +++ b/resources/cudaForStorm/storm-cudaplugin-config.h.in @@ -8,6 +8,12 @@ #ifndef 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_ diff --git a/src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp b/src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp index 6807a77fd..cdc468936 100644 --- a/src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp +++ b/src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp @@ -1,6 +1,7 @@ #include "src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.h" #include +#include #include "src/settings/Settings.h" #include "src/utility/vector.h" @@ -15,7 +16,9 @@ extern log4cplus::Logger logger; #include "storm-config.h" -#include "cudaForStorm.h" +#ifdef STORM_HAVE_CUDAFORSTORM +# include "cudaForStorm.h" +#endif namespace storm { namespace solver { @@ -44,12 +47,9 @@ namespace storm { template void TopologicalValueIterationNondeterministicLinearEquationSolver::solveEquationSystem(bool minimize, storm::storage::SparseMatrix const& A, std::vector& x, std::vector const& b, std::vector* multiplyResult, std::vector* newX) const { - // Now, we need to determine the SCCs of the MDP and a topological sort. - //std::vector> stronglyConnectedComponents = storm::utility::graph::performSccDecomposition(this->getModel(), stronglyConnectedComponents, stronglyConnectedComponentsDependencyGraph); - //storm::storage::SparseMatrix stronglyConnectedComponentsDependencyGraph = this->getModel().extractSccDependencyGraph(stronglyConnectedComponents); + // Now, we need to determine the SCCs of the MDP and perform a topological sort. std::vector const& nondeterministicChoiceIndices = A.getRowGroupIndices(); storm::models::NonDeterministicMatrixBasedPseudoModel pseudoModel(A, nondeterministicChoiceIndices); - //storm::storage::StronglyConnectedComponentDecomposition sccDecomposition(*static_cast*>(&pseudoModel), false, false); storm::storage::StronglyConnectedComponentDecomposition sccDecomposition(pseudoModel, false, false); if (sccDecomposition.size() == 0) { @@ -61,20 +61,10 @@ namespace storm { std::vector topologicalSort = storm::utility::graph::getTopologicalSort(stronglyConnectedComponentsDependencyGraph); // Calculate the optimal distribution of sccs - std::vector>> optimalSccs = this->getOptimalGroupingFromTopologicalSccDecomposition(sccDecomposition, topologicalSort, A); - - // Set up the environment for the power method. -// bool multiplyResultMemoryProvided = true; -// if (multiplyResult == nullptr) { -// multiplyResult = new std::vector(A.getRowCount()); -// multiplyResultMemoryProvided = false; -// } + std::vector> optimalSccs = this->getOptimalGroupingFromTopologicalSccDecomposition(sccDecomposition, topologicalSort, A); + LOG4CPLUS_INFO(logger, "Optimized SCC Decomposition, originally " << topologicalSort.size() << " SCCs, optimized to " << optimalSccs.size() << " SCCs."); + std::vector* currentX = nullptr; - //bool xMemoryProvided = true; - //if (newX == nullptr) { - // newX = new std::vector(x.size()); - // xMemoryProvided = false; - //} std::vector* swap = nullptr; uint_fast64_t currentMaxLocalIterations = 0; uint_fast64_t localIterations = 0; @@ -87,7 +77,7 @@ namespace storm { for (auto sccIndexIt = optimalSccs.cbegin(); sccIndexIt != optimalSccs.cend() && converged; ++sccIndexIt) { bool const useGpu = sccIndexIt->first; - std::vector const& scc = sccIndexIt->second; + storm::storage::StateBlock const& scc = sccIndexIt->second; // Generate a submatrix 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, "The CUDA Runtime Version is " << getRuntimeCudaVersion()); - std::vector copyX(*currentX); 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 { - 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; - - // DEBUG - localIterations = 0; - converged = false; - while (!converged && localIterations < this->maximalNumberOfIterations) { - // Compute x' = A*x + b. - sccSubmatrix.multiplyWithVector(*currentX, sccMultiplyResult); - storm::utility::vector::addVectorsInPlace(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(sccMultiplyResult, *swap, sccSubNondeterministicChoiceIndices); - } - else { - storm::utility::vector::reduceVectorMax(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(*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; +#else + LOG4CPLUS_ERROR(logger, "The useGpu Flag of a SCC was set, but this version of StoRM does not support CUDA acceleration. Internal Error!"); + throw storm::exceptions::InvalidStateException() << "The useGpu Flag of a SCC was set, but this version of StoRM does not support CUDA acceleration. Internal Error!"; #endif } else { localIterations = 0; @@ -256,14 +199,6 @@ namespace storm { currentMaxLocalIterations = localIterations; } } - - //if (!xMemoryProvided) { - // delete newX; - //} - -// if (!multiplyResultMemoryProvided) { -// delete multiplyResult; -// } // Check if the solver converged and issue a warning otherwise. if (converged) { @@ -275,9 +210,9 @@ namespace storm { } template - std::vector>> + std::vector> TopologicalValueIterationNondeterministicLinearEquationSolver::getOptimalGroupingFromTopologicalSccDecomposition(storm::storage::StronglyConnectedComponentDecomposition const& sccDecomposition, std::vector const& topologicalSort, storm::storage::SparseMatrix const& matrix) const { - std::vector>> result; + std::vector> result; #ifdef STORM_HAVE_CUDAFORSTORM // 95% to have a bit of padding size_t const cudaFreeMemory = static_cast(getFreeCudaMemory() * 0.95); @@ -290,13 +225,13 @@ namespace storm { uint_fast64_t rowCount = 0; uint_fast64_t entryCount = 0; - std::vector rowGroups; + storm::storage::StateBlock rowGroups; rowGroups.reserve(scc.size()); for (auto sccIt = scc.cbegin(); sccIt != scc.cend(); ++sccIt) { rowCount += matrix.getRowGroupSize(*sccIt); entryCount += matrix.getRowGroupEntryCount(*sccIt); - rowGroups.push_back(*sccIt); + rowGroups.insert(*sccIt); } size_t sccSize = basicValueIteration_mvReduce_uint64_double_calculateMemorySize(static_cast(rowCount), scc.size(), static_cast(entryCount)); @@ -308,7 +243,7 @@ namespace storm { result.push_back(std::make_pair(true, rowGroups)); } else { - result[lastResultIndex].second.insert(result[lastResultIndex].second.end(), rowGroups.begin(), rowGroups.end()); + result[lastResultIndex].second.insert(rowGroups.begin(), rowGroups.end()); } currentSize += sccSize; } @@ -329,12 +264,12 @@ namespace storm { #else for (auto sccIndexIt = topologicalSort.cbegin(); sccIndexIt != topologicalSort.cend(); ++sccIndexIt) { storm::storage::StateBlock const& scc = sccDecomposition[*sccIndexIt]; - std::vector rowGroups; + storm::storage::StateBlock rowGroups; rowGroups.reserve(scc.size()); for (auto sccIt = scc.cbegin(); sccIt != scc.cend(); ++sccIt) { - rowGroups.push_back(*sccIt); - result.push_back(std::make_pair(false, rowGroups)); + rowGroups.insert(*sccIt); } + result.push_back(std::make_pair(false, rowGroups)); } #endif return result; diff --git a/src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.h b/src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.h index 84aba15fe..40d9df354 100644 --- a/src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.h +++ b/src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.h @@ -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. */ - std::vector>> getOptimalGroupingFromTopologicalSccDecomposition(storm::storage::StronglyConnectedComponentDecomposition const& sccDecomposition, std::vector const& topologicalSort, storm::storage::SparseMatrix const& matrix) const; + std::vector> getOptimalGroupingFromTopologicalSccDecomposition(storm::storage::StronglyConnectedComponentDecomposition const& sccDecomposition, std::vector const& topologicalSort, storm::storage::SparseMatrix const& matrix) const; }; } // namespace solver } // namespace storm diff --git a/src/storm.cpp b/src/storm.cpp index 636606049..cd1ec951c 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -75,6 +75,9 @@ #ifdef STORM_HAVE_Z3 # include "z3.h" #endif +#ifdef STORM_HAVE_CUDAFORSTORM +# include "cudaForStorm.h" +#endif #include #include @@ -173,8 +176,20 @@ void printHeader(const int argc, const char* argv[]) { if (STORM_CPP_VERSION_DIRTY == 1) { 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 std::cout << "Linked with Intel Threading Building Blocks v" << TBB_VERSION_MAJOR << "." << TBB_VERSION_MINOR << " (Interface version " << TBB_INTERFACE_VERSION << ")." << std::endl; #endif diff --git a/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp index f39d17022..811b9532d 100644 --- a/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp @@ -7,6 +7,8 @@ #include "src/modelchecker/prctl/TopologicalValueIterationMdpPrctlModelChecker.h" #include "src/parser/AutoParser.h" +#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"); @@ -86,8 +88,12 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) { storm::property::prctl::RewardNoBoundOperator* rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, true); 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()); +#endif delete rewardFormula; apFormula = new storm::property::prctl::Ap("done"); @@ -95,8 +101,12 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) { rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, false); 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()); +#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", ""); @@ -112,8 +122,12 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) { rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, true); 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()); +#endif delete rewardFormula; apFormula = new storm::property::prctl::Ap("done"); @@ -122,7 +136,11 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) { 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()); +#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"); @@ -139,7 +157,11 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) { 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()); +#endif delete rewardFormula; apFormula = new storm::property::prctl::Ap("done"); @@ -148,7 +170,11 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) { 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()); +#endif delete rewardFormula; } @@ -209,17 +235,25 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, AsynchronousLeader) { storm::property::prctl::ReachabilityReward* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); storm::property::prctl::RewardNoBoundOperator* rewardFormula = new storm::property::prctl::RewardNoBoundOperator(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()); +#else + ASSERT_LT(std::abs(result[0] - 4.285701547), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); +#endif delete rewardFormula; apFormula = new storm::property::prctl::Ap("elected"); reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); rewardFormula = new storm::property::prctl::RewardNoBoundOperator(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()); +#else + ASSERT_LT(std::abs(result[0] - 4.285703591), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); +#endif delete rewardFormula; }