You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

74 lines
3.5 KiB

  1. #ifndef CUDA_KERNELS_GRAPH_H
  2. #define CUDA_KERNELS_GRAPH_H
  3. #include <set>
  4. #include <limits>
  5. #include "src/storage/sparse/StateType.h"
  6. #include "src/models/AbstractDeterministicModel.h"
  7. #include "src/models/AbstractNondeterministicModel.h"
  8. #include "src/utility/constants.h"
  9. #include "src/exceptions/InvalidArgumentException.h"
  10. namespace stormcuda {
  11. namespace graph {
  12. void helloWorld();
  13. template <typename T>
  14. storm::storage::BitVector performProbGreater0(storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) {
  15. helloWorld();
  16. // Prepare the resulting bit vector.
  17. uint_fast64_t numberOfStates = phiStates.size();
  18. storm::storage::BitVector statesWithProbabilityGreater0(numberOfStates);
  19. // Add all psi states as the already satisfy the condition.
  20. statesWithProbabilityGreater0 |= psiStates;
  21. // Initialize the stack used for the DFS with the states.
  22. std::vector<uint_fast64_t> stack(psiStates.begin(), psiStates.end());
  23. // Initialize the stack for the step bound, if the number of steps is bounded.
  24. std::vector<uint_fast64_t> stepStack;
  25. std::vector<uint_fast64_t> remainingSteps;
  26. if (useStepBound) {
  27. stepStack.reserve(numberOfStates);
  28. stepStack.insert(stepStack.begin(), psiStates.getNumberOfSetBits(), maximalSteps);
  29. remainingSteps.resize(numberOfStates);
  30. for (auto state : psiStates) {
  31. remainingSteps[state] = maximalSteps;
  32. }
  33. }
  34. // Perform the actual DFS.
  35. uint_fast64_t currentState, currentStepBound;
  36. while (!stack.empty()) {
  37. currentState = stack.back();
  38. stack.pop_back();
  39. if (useStepBound) {
  40. currentStepBound = stepStack.back();
  41. stepStack.pop_back();
  42. }
  43. for (typename storm::storage::SparseMatrix<T>::const_iterator entryIt = backwardTransitions.begin(currentState), entryIte = backwardTransitions.end(currentState); entryIt != entryIte; ++entryIt) {
  44. if (phiStates[entryIt->getColumn()] && (!statesWithProbabilityGreater0.get(entryIt->getColumn()) || (useStepBound && remainingSteps[entryIt->getColumn()] < currentStepBound - 1))) {
  45. // If we don't have a bound on the number of steps to take, just add the state to the stack.
  46. if (!useStepBound) {
  47. statesWithProbabilityGreater0.set(entryIt->getColumn(), true);
  48. stack.push_back(entryIt->getColumn());
  49. } else if (currentStepBound > 0) {
  50. // If there is at least one more step to go, we need to push the state and the new number of steps.
  51. remainingSteps[entryIt->getColumn()] = currentStepBound - 1;
  52. statesWithProbabilityGreater0.set(entryIt->getColumn(), true);
  53. stack.push_back(entryIt->getColumn());
  54. stepStack.push_back(currentStepBound - 1);
  55. }
  56. }
  57. }
  58. }
  59. // Return result.
  60. return statesWithProbabilityGreater0;
  61. }
  62. }
  63. }
  64. #endif /* CUDA_KERNELS_GRAPH_H */