From 35a154f67fa899e42c8e8e40ab86529f104825a9 Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@rwth-aachen.de>
Date: Wed, 26 Aug 2015 21:20:00 +0200
Subject: [PATCH] Splitted graph in h and cpp`
Former-commit-id: e22ab7f8eb519d5fc7844cf330529122f4738bd6
---
.../csl/helper/HybridCtmcCslHelper.cpp | 1 +
.../helper/SparseMarkovAutomatonCslHelper.cpp | 3 +
.../prctl/HybridDtmcPrctlModelChecker.cpp | 1 +
.../prctl/SparseMdpPrctlModelChecker.cpp | 3 +
.../prctl/SymbolicMdpPrctlModelChecker.cpp | 2 +
.../prctl/helper/HybridDtmcPrctlHelper.cpp | 1 +
.../prctl/helper/HybridMdpPrctlHelper.cpp | 1 +
.../prctl/helper/SparseMdpPrctlHelper.cpp | 3 +
.../prctl/helper/SymbolicDtmcPrctlHelper.cpp | 1 +
.../prctl/helper/SymbolicMdpPrctlHelper.cpp | 3 +
src/utility/graph.cpp | 1025 +++++++++++++++++
src/utility/graph.h | 794 +------------
12 files changed, 1104 insertions(+), 734 deletions(-)
create mode 100644 src/utility/graph.cpp
diff --git a/src/modelchecker/csl/helper/HybridCtmcCslHelper.cpp b/src/modelchecker/csl/helper/HybridCtmcCslHelper.cpp
index 273788e20..510c0cba9 100644
--- a/src/modelchecker/csl/helper/HybridCtmcCslHelper.cpp
+++ b/src/modelchecker/csl/helper/HybridCtmcCslHelper.cpp
@@ -10,6 +10,7 @@
#include "src/utility/macros.h"
#include "src/utility/graph.h"
+#include "src/utility/constants.h"
#include "src/models/symbolic/StandardRewardModel.h"
diff --git a/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
index 3dc58ba6a..c8138d908 100644
--- a/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
+++ b/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
@@ -12,6 +12,9 @@
#include "src/utility/vector.h"
#include "src/utility/graph.h"
+#include "src/storage/expressions/Variable.h"
+#include "src/storage/expressions/Expression.h"
+
#include "src/utility/numerical.h"
#include "src/solver/MinMaxLinearEquationSolver.h"
diff --git a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp
index 44fc0fef9..c2d67f7ba 100644
--- a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp
+++ b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp
@@ -19,6 +19,7 @@
#include "src/exceptions/InvalidStateException.h"
#include "src/exceptions/InvalidPropertyException.h"
+#include "src/exceptions/InvalidArgumentException.h"
namespace storm {
namespace modelchecker {
diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
index aa4c620d6..3c1c3bc4d 100644
--- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
+++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
@@ -21,6 +21,9 @@
#include "src/storage/MaximalEndComponentDecomposition.h"
+
+#include "src/exceptions/InvalidArgumentException.h"
+
namespace storm {
namespace modelchecker {
template<typename SparseMdpModelType>
diff --git a/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp
index 69a54d4ba..a8304af48 100644
--- a/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp
+++ b/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp
@@ -15,6 +15,8 @@
#include "src/exceptions/InvalidStateException.h"
#include "src/exceptions/InvalidPropertyException.h"
+#include "src/exceptions/InvalidArgumentException.h"
+
namespace storm {
namespace modelchecker {
template<storm::dd::DdType DdType, typename ValueType>
diff --git a/src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp b/src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp
index f3e9eeaf9..08719db30 100644
--- a/src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp
+++ b/src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp
@@ -9,6 +9,7 @@
#include "src/storage/dd/CuddOdd.h"
#include "src/utility/graph.h"
+#include "src/utility/constants.h"
#include "src/models/symbolic/StandardRewardModel.h"
diff --git a/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp b/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp
index 697ce9f0c..22cf9c314 100644
--- a/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp
+++ b/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp
@@ -6,6 +6,7 @@
#include "src/storage/dd/CuddOdd.h"
#include "src/utility/graph.h"
+#include "src/utility/constants.h"
#include "src/models/symbolic/StandardRewardModel.h"
diff --git a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
index 33db26a60..f771ceea3 100644
--- a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
+++ b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
@@ -6,6 +6,9 @@
#include "src/utility/vector.h"
#include "src/utility/graph.h"
+#include "src/storage/expressions/Variable.h"
+#include "src/storage/expressions/Expression.h"
+
#include "src/solver/MinMaxLinearEquationSolver.h"
#include "src/solver/LpSolver.h"
diff --git a/src/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp b/src/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp
index 986b8cd35..9992285b9 100644
--- a/src/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp
+++ b/src/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp
@@ -11,6 +11,7 @@
#include "src/models/symbolic/StandardRewardModel.h"
#include "src/utility/graph.h"
+#include "src/utility/constants.h"
#include "src/exceptions/InvalidPropertyException.h"
diff --git a/src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp b/src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp
index a0086e465..02d350fcb 100644
--- a/src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp
+++ b/src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp
@@ -8,6 +8,8 @@
#include "src/storage/dd/CuddOdd.h"
#include "src/utility/graph.h"
+#include "src/utility/constants.h"
+
#include "src/models/symbolic/StandardRewardModel.h"
@@ -15,6 +17,7 @@
#include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h"
#include "src/exceptions/InvalidPropertyException.h"
+#include "src/exceptions/InvalidArgumentException.h"
namespace storm {
namespace modelchecker {
diff --git a/src/utility/graph.cpp b/src/utility/graph.cpp
new file mode 100644
index 000000000..f48e6f5e2
--- /dev/null
+++ b/src/utility/graph.cpp
@@ -0,0 +1,1025 @@
+#include "graph.h"
+#include "utility/OsDetection.h"
+#include "storm-config.h"
+
+#include "src/adapters/CarlAdapter.h"
+
+#include "src/storage/sparse/StateType.h"
+#include "src/models/symbolic/DeterministicModel.h"
+#include "src/models/symbolic/NondeterministicModel.h"
+#include "src/models/sparse/DeterministicModel.h"
+#include "src/models/sparse/NondeterministicModel.h"
+#include "src/utility/constants.h"
+#include "src/exceptions/InvalidArgumentException.h"
+#include "src/storage/dd/CuddBdd.h"
+#include "src/storage/dd/CuddAdd.h"
+#include "src/storage/dd/CuddDdManager.h"
+
+#include "log4cplus/logger.h"
+#include "log4cplus/loggingmacros.h"
+
+extern log4cplus::Logger logger;
+
+namespace storm {
+ namespace utility {
+ namespace graph {
+
+ template<typename T>
+ storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix<T> const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates) {
+ storm::storage::BitVector reachableStates(initialStates);
+
+ // Initialize the stack used for the DFS with the states.
+ std::vector<uint_fast64_t> stack(initialStates.begin(), initialStates.end());
+
+ // Perform the actual DFS.
+ uint_fast64_t currentState = 0;
+ while (!stack.empty()) {
+ currentState = stack.back();
+ stack.pop_back();
+
+ for (auto const& successor : transitionMatrix.getRowGroup(currentState)) {
+ // Only explore the state if the transition was actually there and the successor has not yet
+ // been visited.
+ if (successor.getValue() != storm::utility::zero<T>() && !reachableStates.get(successor.getColumn())) {
+ // If the successor is one of the target states, we need to include it, but must not explore
+ // it further.
+ if (targetStates.get(successor.getColumn())) {
+ reachableStates.set(successor.getColumn());
+ } else if (constraintStates.get(successor.getColumn())) {
+ // However, if the state is in the constrained set of states, we need to follow it.
+ reachableStates.set(successor.getColumn());
+ stack.push_back(successor.getColumn());
+ }
+ }
+ }
+ }
+
+ return reachableStates;
+ }
+
+ template<typename T>
+ std::vector<std::size_t> getDistances(storm::storage::SparseMatrix<T> const& transitionMatrix, storm::storage::BitVector const& initialStates) {
+ std::vector<std::size_t> distances(transitionMatrix.getRowGroupCount());
+
+ std::vector<std::pair<storm::storage::sparse::state_type, std::size_t>> stateQueue;
+ stateQueue.reserve(transitionMatrix.getRowGroupCount());
+ storm::storage::BitVector statesInQueue(transitionMatrix.getRowGroupCount());
+
+ storm::storage::sparse::state_type currentPosition = 0;
+ for (auto const& initialState : initialStates) {
+ stateQueue.emplace_back(initialState, 0);
+ statesInQueue.set(initialState);
+ }
+
+ // Perform a BFS.
+ while (currentPosition < stateQueue.size()) {
+ std::pair<storm::storage::sparse::state_type, std::size_t> const& stateDistancePair = stateQueue[currentPosition];
+ distances[stateDistancePair.first] = stateDistancePair.second;
+
+ for (auto const& successorEntry : transitionMatrix.getRowGroup(stateDistancePair.first)) {
+ if (!statesInQueue.get(successorEntry.getColumn())) {
+ stateQueue.emplace_back(successorEntry.getColumn(), stateDistancePair.second + 1);
+ statesInQueue.set(successorEntry.getColumn());
+ }
+ }
+ ++currentPosition;
+ }
+
+ return distances;
+ }
+
+ template <typename T>
+ storm::storage::BitVector performProbGreater0(storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound, uint_fast64_t maximalSteps) {
+ // Prepare the resulting bit vector.
+ uint_fast64_t numberOfStates = phiStates.size();
+ storm::storage::BitVector statesWithProbabilityGreater0(numberOfStates);
+
+ // Add all psi states as they already satisfy the condition.
+ statesWithProbabilityGreater0 |= psiStates;
+
+ // Initialize the stack used for the DFS with the states.
+ std::vector<uint_fast64_t> stack(psiStates.begin(), psiStates.end());
+
+ // Initialize the stack for the step bound, if the number of steps is bounded.
+ std::vector<uint_fast64_t> stepStack;
+ std::vector<uint_fast64_t> remainingSteps;
+ if (useStepBound) {
+ stepStack.reserve(numberOfStates);
+ stepStack.insert(stepStack.begin(), psiStates.getNumberOfSetBits(), maximalSteps);
+ remainingSteps.resize(numberOfStates);
+ for (auto state : psiStates) {
+ remainingSteps[state] = maximalSteps;
+ }
+ }
+
+ // Perform the actual DFS.
+ uint_fast64_t currentState, currentStepBound;
+ while (!stack.empty()) {
+ currentState = stack.back();
+ stack.pop_back();
+
+ if (useStepBound) {
+ currentStepBound = stepStack.back();
+ stepStack.pop_back();
+ }
+
+ for (typename storm::storage::SparseMatrix<T>::const_iterator entryIt = backwardTransitions.begin(currentState), entryIte = backwardTransitions.end(currentState); entryIt != entryIte; ++entryIt) {
+ if (phiStates[entryIt->getColumn()] && (!statesWithProbabilityGreater0.get(entryIt->getColumn()) || (useStepBound && remainingSteps[entryIt->getColumn()] < currentStepBound - 1))) {
+ // If we don't have a bound on the number of steps to take, just add the state to the stack.
+ if (!useStepBound) {
+ statesWithProbabilityGreater0.set(entryIt->getColumn(), true);
+ stack.push_back(entryIt->getColumn());
+ } else if (currentStepBound > 0) {
+ // If there is at least one more step to go, we need to push the state and the new number of steps.
+ remainingSteps[entryIt->getColumn()] = currentStepBound - 1;
+ statesWithProbabilityGreater0.set(entryIt->getColumn(), true);
+ stack.push_back(entryIt->getColumn());
+ stepStack.push_back(currentStepBound - 1);
+ }
+ }
+ }
+ }
+
+ // Return result.
+ return statesWithProbabilityGreater0;
+ }
+
+ template <typename T>
+ storm::storage::BitVector performProb1(storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector const& statesWithProbabilityGreater0) {
+ storm::storage::BitVector statesWithProbability1 = performProbGreater0(backwardTransitions, ~psiStates, ~statesWithProbabilityGreater0);
+ statesWithProbability1.complement();
+ return statesWithProbability1;
+ }
+
+ template <typename T>
+ storm::storage::BitVector performProb1(storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
+ storm::storage::BitVector statesWithProbabilityGreater0 = performProbGreater0(backwardTransitions, phiStates, psiStates);
+ storm::storage::BitVector statesWithProbability1 = performProbGreater0(backwardTransitions, ~psiStates, ~(statesWithProbabilityGreater0));
+ statesWithProbability1.complement();
+ return statesWithProbability1;
+ }
+
+ template <typename T>
+ std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01(storm::models::sparse::DeterministicModel<T> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
+ std::pair<storm::storage::BitVector, storm::storage::BitVector> result;
+ storm::storage::SparseMatrix<T> backwardTransitions = model.getBackwardTransitions();
+ result.first = performProbGreater0(backwardTransitions, phiStates, psiStates);
+ result.second = performProb1(backwardTransitions, phiStates, psiStates, result.first);
+ result.first.complement();
+ return result;
+ }
+
+ template <typename T>
+ std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01(storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
+ std::pair<storm::storage::BitVector, storm::storage::BitVector> result;
+ result.first = performProbGreater0(backwardTransitions, phiStates, psiStates);
+ result.second = performProb1(backwardTransitions, phiStates, psiStates, result.first);
+ result.first.complement();
+ return result;
+ }
+
+ template <storm::dd::DdType Type>
+ storm::dd::Bdd<Type> performProbGreater0(storm::models::symbolic::Model<Type> const& model, storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates, boost::optional<uint_fast64_t> const& stepBound) {
+ // Initialize environment for backward search.
+ storm::dd::DdManager<Type> const& manager = model.getManager();
+ storm::dd::Bdd<Type> lastIterationStates = manager.getBddZero();
+ storm::dd::Bdd<Type> statesWithProbabilityGreater0 = psiStates;
+
+ uint_fast64_t iterations = 0;
+ while (lastIterationStates != statesWithProbabilityGreater0) {
+ if (stepBound && iterations >= stepBound.get()) {
+ break;
+ }
+
+ lastIterationStates = statesWithProbabilityGreater0;
+ statesWithProbabilityGreater0 = statesWithProbabilityGreater0.swapVariables(model.getRowColumnMetaVariablePairs());
+ statesWithProbabilityGreater0 &= transitionMatrix;
+ statesWithProbabilityGreater0 = statesWithProbabilityGreater0.existsAbstract(model.getColumnVariables());
+ statesWithProbabilityGreater0 &= phiStates;
+ statesWithProbabilityGreater0 |= lastIterationStates;
+ ++iterations;
+ }
+
+ return statesWithProbabilityGreater0;
+ }
+
+ template <storm::dd::DdType Type>
+ storm::dd::Bdd<Type> performProb1(storm::models::symbolic::Model<Type> const& model, storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates, storm::dd::Bdd<Type> const& statesWithProbabilityGreater0) {
+ storm::dd::Bdd<Type> statesWithProbability1 = performProbGreater0(model, transitionMatrix, !psiStates && model.getReachableStates(), !statesWithProbabilityGreater0 && model.getReachableStates());
+ statesWithProbability1 = !statesWithProbability1 && model.getReachableStates();
+ return statesWithProbability1;
+ }
+
+ template <storm::dd::DdType Type>
+ storm::dd::Bdd<Type> performProb1(storm::models::symbolic::Model<Type> const& model, storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates) {
+ storm::dd::Bdd<Type> statesWithProbabilityGreater0 = performProbGreater0(model, transitionMatrix, phiStates, psiStates);
+ return performProb1(model, transitionMatrix, phiStates, psiStates, statesWithProbabilityGreater0);
+ }
+
+ template <storm::dd::DdType Type>
+ std::pair<storm::dd::Bdd<Type>, storm::dd::Bdd<Type>> performProb01(storm::models::symbolic::DeterministicModel<Type> const& model, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates) {
+ std::pair<storm::dd::Bdd<Type>, storm::dd::Bdd<Type>> result;
+ storm::dd::Bdd<Type> transitionMatrix = model.getTransitionMatrix().notZero();
+ result.first = performProbGreater0(model, transitionMatrix, phiStates, psiStates);
+ result.second = !performProbGreater0(model, transitionMatrix, !psiStates && model.getReachableStates(), !result.first && model.getReachableStates()) && model.getReachableStates();
+ result.first = !result.first && model.getReachableStates();
+ return result;
+ }
+
+ template <storm::dd::DdType Type>
+ std::pair<storm::dd::Bdd<Type>, storm::dd::Bdd<Type>> performProb01(storm::models::symbolic::Model<Type> const& model, storm::dd::Add<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates) {
+ std::pair<storm::dd::Bdd<Type>, storm::dd::Bdd<Type>> result;
+ storm::dd::Bdd<Type> transitionMatrixBdd = transitionMatrix.notZero();
+ result.first = performProbGreater0(model, transitionMatrixBdd, phiStates, psiStates);
+ result.second = !performProbGreater0(model, transitionMatrixBdd, !psiStates && model.getReachableStates(), !result.first && model.getReachableStates()) && model.getReachableStates();
+ result.first = !result.first && model.getReachableStates();
+ return result;
+ }
+
+ template <typename T>
+ storm::storage::BitVector performProbGreater0E(storm::storage::SparseMatrix<T> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound, uint_fast64_t maximalSteps) {
+ size_t numberOfStates = phiStates.size();
+
+ // Prepare resulting bit vector.
+ storm::storage::BitVector statesWithProbabilityGreater0(numberOfStates);
+
+ // Add all psi states as the already satisfy the condition.
+ statesWithProbabilityGreater0 |= psiStates;
+
+ // Initialize the stack used for the DFS with the states
+ std::vector<uint_fast64_t> stack(psiStates.begin(), psiStates.end());
+
+ // Initialize the stack for the step bound, if the number of steps is bounded.
+ std::vector<uint_fast64_t> stepStack;
+ std::vector<uint_fast64_t> remainingSteps;
+ if (useStepBound) {
+ stepStack.reserve(numberOfStates);
+ stepStack.insert(stepStack.begin(), psiStates.getNumberOfSetBits(), maximalSteps);
+ remainingSteps.resize(numberOfStates);
+ for (auto state : psiStates) {
+ remainingSteps[state] = maximalSteps;
+ }
+ }
+
+ // Perform the actual DFS.
+ uint_fast64_t currentState, currentStepBound;
+ while (!stack.empty()) {
+ currentState = stack.back();
+ stack.pop_back();
+
+ if (useStepBound) {
+ currentStepBound = stepStack.back();
+ stepStack.pop_back();
+ }
+
+ for (typename storm::storage::SparseMatrix<T>::const_iterator entryIt = backwardTransitions.begin(currentState), entryIte = backwardTransitions.end(currentState); entryIt != entryIte; ++entryIt) {
+ if (phiStates.get(entryIt->getColumn()) && (!statesWithProbabilityGreater0.get(entryIt->getColumn()) || (useStepBound && remainingSteps[entryIt->getColumn()] < currentStepBound - 1))) {
+ // If we don't have a bound on the number of steps to take, just add the state to the stack.
+ if (!useStepBound) {
+ statesWithProbabilityGreater0.set(entryIt->getColumn(), true);
+ stack.push_back(entryIt->getColumn());
+ } else if (currentStepBound > 0) {
+ // If there is at least one more step to go, we need to push the state and the new number of steps.
+ remainingSteps[entryIt->getColumn()] = currentStepBound - 1;
+ statesWithProbabilityGreater0.set(entryIt->getColumn(), true);
+ stack.push_back(entryIt->getColumn());
+ stepStack.push_back(currentStepBound - 1);
+ }
+ }
+ }
+ }
+
+ return statesWithProbabilityGreater0;
+ }
+
+ template <typename T>
+ storm::storage::BitVector performProb0A(storm::storage::SparseMatrix<T> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
+ storm::storage::BitVector statesWithProbability0 = performProbGreater0E(transitionMatrix, nondeterministicChoiceIndices, backwardTransitions, phiStates, psiStates);
+ statesWithProbability0.complement();
+ return statesWithProbability0;
+ }
+
+ template <typename T>
+ storm::storage::BitVector performProb0A(storm::models::sparse::NondeterministicModel<T> const& model, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
+ return performProb0A(model.getTransitionMatrix(), model.getNondeterministicChoiceIndices(), backwardTransitions, phiStates, psiStates);
+ }
+
+ template <typename T>
+ storm::storage::BitVector performProb1E(storm::storage::SparseMatrix<T> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
+ size_t numberOfStates = phiStates.size();
+
+ // Initialize the environment for the iterative algorithm.
+ storm::storage::BitVector currentStates(numberOfStates, true);
+ std::vector<uint_fast64_t> stack;
+ stack.reserve(numberOfStates);
+
+ // Perform the loop as long as the set of states gets larger.
+ bool done = false;
+ uint_fast64_t currentState;
+ while (!done) {
+ stack.clear();
+ storm::storage::BitVector nextStates(psiStates);
+ stack.insert(stack.end(), psiStates.begin(), psiStates.end());
+
+ while (!stack.empty()) {
+ currentState = stack.back();
+ stack.pop_back();
+
+ for (typename storm::storage::SparseMatrix<T>::const_iterator predecessorEntryIt = backwardTransitions.begin(currentState), predecessorEntryIte = backwardTransitions.end(currentState); predecessorEntryIt != predecessorEntryIte; ++predecessorEntryIt) {
+ if (phiStates.get(predecessorEntryIt->getColumn()) && !nextStates.get(predecessorEntryIt->getColumn())) {
+ // Check whether the predecessor has only successors in the current state set for one of the
+ // nondeterminstic choices.
+ for (uint_fast64_t row = nondeterministicChoiceIndices[predecessorEntryIt->getColumn()]; row < nondeterministicChoiceIndices[predecessorEntryIt->getColumn() + 1]; ++row) {
+ bool allSuccessorsInCurrentStates = true;
+ for (typename storm::storage::SparseMatrix<T>::const_iterator successorEntryIt = transitionMatrix.begin(row), successorEntryIte = transitionMatrix.end(row); successorEntryIt != successorEntryIte; ++successorEntryIt) {
+ if (!currentStates.get(successorEntryIt->getColumn())) {
+ allSuccessorsInCurrentStates = false;
+ break;
+ }
+ }
+
+ // If all successors for a given nondeterministic choice are in the current state set, we
+ // add it to the set of states for the next iteration and perform a backward search from
+ // that state.
+ if (allSuccessorsInCurrentStates) {
+ nextStates.set(predecessorEntryIt->getColumn(), true);
+ stack.push_back(predecessorEntryIt->getColumn());
+ break;
+ }
+ }
+ }
+ }
+ }
+
+ // Check whether we need to perform an additional iteration.
+ if (currentStates == nextStates) {
+ done = true;
+ } else {
+ currentStates = std::move(nextStates);
+ }
+ }
+
+ return currentStates;
+ }
+
+ template <typename T>
+ storm::storage::BitVector performProb1E(storm::models::sparse::NondeterministicModel<T> const& model, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
+ return performProb1E(model.getTransitionMatrix(), model.getNondeterministicChoiceIndices(), backwardTransitions, phiStates, psiStates);
+ }
+
+ template <typename T>
+ std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Max(storm::storage::SparseMatrix<T> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
+ std::pair<storm::storage::BitVector, storm::storage::BitVector> result;
+
+ result.first = performProb0A(transitionMatrix, nondeterministicChoiceIndices, backwardTransitions, phiStates, psiStates);
+ result.second = performProb1E(transitionMatrix, nondeterministicChoiceIndices, backwardTransitions, phiStates, psiStates);
+ return result;
+ }
+
+ template <typename T>
+ std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Max(storm::models::sparse::NondeterministicModel<T> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
+ return performProb01Max(model.getTransitionMatrix(), model.getTransitionMatrix().getRowGroupIndices(), model.getBackwardTransitions(), phiStates, psiStates);
+ }
+
+ template <typename T>
+ storm::storage::BitVector performProbGreater0A(storm::storage::SparseMatrix<T> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound, uint_fast64_t maximalSteps) {
+ size_t numberOfStates = phiStates.size();
+
+ // Prepare resulting bit vector.
+ storm::storage::BitVector statesWithProbabilityGreater0(numberOfStates);
+
+ // Add all psi states as the already satisfy the condition.
+ statesWithProbabilityGreater0 |= psiStates;
+
+ // Initialize the stack used for the DFS with the states
+ std::vector<uint_fast64_t> stack(psiStates.begin(), psiStates.end());
+
+ // Initialize the stack for the step bound, if the number of steps is bounded.
+ std::vector<uint_fast64_t> stepStack;
+ std::vector<uint_fast64_t> remainingSteps;
+ if (useStepBound) {
+ stepStack.reserve(numberOfStates);
+ stepStack.insert(stepStack.begin(), psiStates.getNumberOfSetBits(), maximalSteps);
+ remainingSteps.resize(numberOfStates);
+ for (auto state : psiStates) {
+ remainingSteps[state] = maximalSteps;
+ }
+ }
+
+ // Perform the actual DFS.
+ uint_fast64_t currentState, currentStepBound;
+ while(!stack.empty()) {
+ currentState = stack.back();
+ stack.pop_back();
+
+ if (useStepBound) {
+ currentStepBound = stepStack.back();
+ stepStack.pop_back();
+ }
+
+ for(typename storm::storage::SparseMatrix<T>::const_iterator predecessorEntryIt = backwardTransitions.begin(currentState), predecessorEntryIte = backwardTransitions.end(currentState); predecessorEntryIt != predecessorEntryIte; ++predecessorEntryIt) {
+ if (phiStates.get(predecessorEntryIt->getColumn()) && (!statesWithProbabilityGreater0.get(predecessorEntryIt->getColumn()) || (useStepBound && remainingSteps[predecessorEntryIt->getColumn()] < currentStepBound - 1))) {
+ // Check whether the predecessor has at least one successor in the current state set for every
+ // nondeterministic choice.
+ bool addToStatesWithProbabilityGreater0 = true;
+ for (uint_fast64_t row = nondeterministicChoiceIndices[predecessorEntryIt->getColumn()]; row < nondeterministicChoiceIndices[predecessorEntryIt->getColumn() + 1]; ++row) {
+ bool hasAtLeastOneSuccessorWithProbabilityGreater0 = false;
+ for (typename storm::storage::SparseMatrix<T>::const_iterator successorEntryIt = transitionMatrix.begin(row), successorEntryIte = transitionMatrix.end(row); successorEntryIt != successorEntryIte; ++successorEntryIt) {
+ if (statesWithProbabilityGreater0.get(successorEntryIt->getColumn())) {
+ hasAtLeastOneSuccessorWithProbabilityGreater0 = true;
+ break;
+ }
+ }
+
+ if (!hasAtLeastOneSuccessorWithProbabilityGreater0) {
+ addToStatesWithProbabilityGreater0 = false;
+ break;
+ }
+ }
+
+ // If we need to add the state, then actually add it and perform further search from the state.
+ if (addToStatesWithProbabilityGreater0) {
+ // If we don't have a bound on the number of steps to take, just add the state to the stack.
+ if (!useStepBound) {
+ statesWithProbabilityGreater0.set(predecessorEntryIt->getColumn(), true);
+ stack.push_back(predecessorEntryIt->getColumn());
+ } else if (currentStepBound > 0) {
+ // If there is at least one more step to go, we need to push the state and the new number of steps.
+ remainingSteps[predecessorEntryIt->getColumn()] = currentStepBound - 1;
+ statesWithProbabilityGreater0.set(predecessorEntryIt->getColumn(), true);
+ stack.push_back(predecessorEntryIt->getColumn());
+ stepStack.push_back(currentStepBound - 1);
+ }
+ }
+ }
+ }
+ }
+
+ return statesWithProbabilityGreater0;
+ }
+
+ template <typename T>
+ storm::storage::BitVector performProb0E(storm::models::sparse::NondeterministicModel<T> const& model, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
+ storm::storage::BitVector statesWithProbability0 = performProbGreater0A(model.getTransitionMatrix(), model.getNondeterministicChoiceIndices(), backwardTransitions, phiStates, psiStates);
+ statesWithProbability0.complement();
+ return statesWithProbability0;
+ }
+
+ template <typename T>
+ storm::storage::BitVector performProb0E(storm::storage::SparseMatrix<T> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
+ storm::storage::BitVector statesWithProbability0 = performProbGreater0A(transitionMatrix, nondeterministicChoiceIndices, backwardTransitions, phiStates, psiStates);
+ statesWithProbability0.complement();
+ return statesWithProbability0;
+ }
+
+ template <typename T>
+ storm::storage::BitVector performProb1A( storm::storage::SparseMatrix<T> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
+ size_t numberOfStates = phiStates.size();
+
+ // Initialize the environment for the iterative algorithm.
+ storm::storage::BitVector currentStates(numberOfStates, true);
+ std::vector<uint_fast64_t> stack;
+ stack.reserve(numberOfStates);
+
+ // Perform the loop as long as the set of states gets smaller.
+ bool done = false;
+ uint_fast64_t currentState;
+ while (!done) {
+ stack.clear();
+ storm::storage::BitVector nextStates(psiStates);
+ stack.insert(stack.end(), psiStates.begin(), psiStates.end());
+
+ while (!stack.empty()) {
+ currentState = stack.back();
+ stack.pop_back();
+
+ for(typename storm::storage::SparseMatrix<T>::const_iterator predecessorEntryIt = backwardTransitions.begin(currentState), predecessorEntryIte = backwardTransitions.end(currentState); predecessorEntryIt != predecessorEntryIte; ++predecessorEntryIt) {
+ if (phiStates.get(predecessorEntryIt->getColumn()) && !nextStates.get(predecessorEntryIt->getColumn())) {
+ // Check whether the predecessor has only successors in the current state set for all of the
+ // nondeterminstic choices and that for each choice there exists a successor that is already
+ // in the next states.
+ bool addToStatesWithProbability1 = true;
+ for (uint_fast64_t row = nondeterministicChoiceIndices[predecessorEntryIt->getColumn()]; row < nondeterministicChoiceIndices[predecessorEntryIt->getColumn() + 1]; ++row) {
+ bool hasAtLeastOneSuccessorWithProbability1 = false;
+ for (typename storm::storage::SparseMatrix<T>::const_iterator successorEntryIt = transitionMatrix.begin(row), successorEntryIte = transitionMatrix.end(row); successorEntryIt != successorEntryIte; ++successorEntryIt) {
+ if (!currentStates.get(successorEntryIt->getColumn())) {
+ addToStatesWithProbability1 = false;
+ goto afterCheckLoop;
+ }
+ if (nextStates.get(successorEntryIt->getColumn())) {
+ hasAtLeastOneSuccessorWithProbability1 = true;
+ }
+ }
+
+ if (!hasAtLeastOneSuccessorWithProbability1) {
+ addToStatesWithProbability1 = false;
+ break;
+ }
+ }
+
+ afterCheckLoop:
+ // If all successors for all nondeterministic choices are in the current state set, we
+ // add it to the set of states for the next iteration and perform a backward search from
+ // that state.
+ if (addToStatesWithProbability1) {
+ nextStates.set(predecessorEntryIt->getColumn(), true);
+ stack.push_back(predecessorEntryIt->getColumn());
+ }
+ }
+ }
+ }
+
+ // Check whether we need to perform an additional iteration.
+ if (currentStates == nextStates) {
+ done = true;
+ } else {
+ currentStates = std::move(nextStates);
+ }
+ }
+ return currentStates;
+ }
+
+ template <typename T>
+ std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Min(storm::storage::SparseMatrix<T> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
+ std::pair<storm::storage::BitVector, storm::storage::BitVector> result;
+ result.first = performProb0E(transitionMatrix, nondeterministicChoiceIndices, backwardTransitions, phiStates, psiStates);
+ result.second = performProb1A(transitionMatrix, nondeterministicChoiceIndices, backwardTransitions, phiStates, psiStates);
+ return result;
+ }
+
+ template <typename T>
+ std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Min(storm::models::sparse::NondeterministicModel<T> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
+ return performProb01Min(model.getTransitionMatrix(), model.getTransitionMatrix().getRowGroupIndices(), model.getBackwardTransitions(), phiStates, psiStates);
+ }
+
+ template <storm::dd::DdType Type>
+ storm::dd::Bdd<Type> performProbGreater0E(storm::models::symbolic::NondeterministicModel<Type> const& model, storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates) {
+ // Initialize environment for backward search.
+ storm::dd::DdManager<Type> const& manager = model.getManager();
+ storm::dd::Bdd<Type> lastIterationStates = manager.getBddZero();
+ storm::dd::Bdd<Type> statesWithProbabilityGreater0E = psiStates;
+
+ uint_fast64_t iterations = 0;
+ storm::dd::Bdd<Type> abstractedTransitionMatrix = transitionMatrix.existsAbstract(model.getNondeterminismVariables());
+ while (lastIterationStates != statesWithProbabilityGreater0E) {
+ lastIterationStates = statesWithProbabilityGreater0E;
+ statesWithProbabilityGreater0E = statesWithProbabilityGreater0E.swapVariables(model.getRowColumnMetaVariablePairs());
+ statesWithProbabilityGreater0E = statesWithProbabilityGreater0E.andExists(abstractedTransitionMatrix, model.getColumnVariables());
+ statesWithProbabilityGreater0E &= phiStates;
+ statesWithProbabilityGreater0E |= lastIterationStates;
+ ++iterations;
+ }
+
+ return statesWithProbabilityGreater0E;
+ }
+
+ template <storm::dd::DdType Type>
+ storm::dd::Bdd<Type> performProb0A(storm::models::symbolic::NondeterministicModel<Type> const& model, storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates) {
+ return !performProbGreater0E(model, transitionMatrix, phiStates, psiStates) && model.getReachableStates();
+ }
+
+ template <storm::dd::DdType Type>
+ storm::dd::Bdd<Type> performProbGreater0A(storm::models::symbolic::NondeterministicModel<Type> const& model, storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates) {
+ // Initialize environment for backward search.
+ storm::dd::DdManager<Type> const& manager = model.getManager();
+ storm::dd::Bdd<Type> lastIterationStates = manager.getBddZero();
+ storm::dd::Bdd<Type> statesWithProbabilityGreater0A = psiStates;
+
+ uint_fast64_t iterations = 0;
+ while (lastIterationStates != statesWithProbabilityGreater0A) {
+ lastIterationStates = statesWithProbabilityGreater0A;
+ statesWithProbabilityGreater0A = statesWithProbabilityGreater0A.swapVariables(model.getRowColumnMetaVariablePairs());
+ statesWithProbabilityGreater0A = statesWithProbabilityGreater0A.andExists(transitionMatrix, model.getColumnVariables());
+ statesWithProbabilityGreater0A |= model.getIllegalMask();
+ statesWithProbabilityGreater0A = statesWithProbabilityGreater0A.universalAbstract(model.getNondeterminismVariables());
+ statesWithProbabilityGreater0A &= phiStates;
+ statesWithProbabilityGreater0A |= psiStates;
+ ++iterations;
+ }
+
+ return statesWithProbabilityGreater0A;
+ }
+
+ template <storm::dd::DdType Type>
+ storm::dd::Bdd<Type> performProb0E(storm::models::symbolic::NondeterministicModel<Type> const& model, storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates) {
+ return !performProbGreater0A(model, transitionMatrix, phiStates, psiStates) && model.getReachableStates();
+ }
+
+ template <storm::dd::DdType Type>
+ storm::dd::Bdd<Type> performProb1A(storm::models::symbolic::NondeterministicModel<Type> const& model, storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates, storm::dd::Bdd<Type> const& statesWithProbabilityGreater0A) {
+ // Initialize environment for backward search.
+ storm::dd::DdManager<Type> const& manager = model.getManager();
+ storm::dd::Bdd<Type> lastIterationStates = manager.getBddZero();
+ storm::dd::Bdd<Type> statesWithProbability1A = psiStates || statesWithProbabilityGreater0A;
+
+ uint_fast64_t iterations = 0;
+ while (lastIterationStates != statesWithProbability1A) {
+ lastIterationStates = statesWithProbability1A;
+ statesWithProbability1A = statesWithProbability1A.swapVariables(model.getRowColumnMetaVariablePairs());
+ statesWithProbability1A = transitionMatrix.implies(statesWithProbability1A).universalAbstract(model.getColumnVariables());
+ statesWithProbability1A |= model.getIllegalMask();
+ statesWithProbability1A = statesWithProbability1A.universalAbstract(model.getNondeterminismVariables());
+ statesWithProbability1A &= statesWithProbabilityGreater0A;
+ statesWithProbability1A |= psiStates;
+ ++iterations;
+ }
+
+ return statesWithProbability1A;
+ }
+
+ template <storm::dd::DdType Type>
+ storm::dd::Bdd<Type> performProb1E(storm::models::symbolic::NondeterministicModel<Type> const& model, storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates, storm::dd::Bdd<Type> const& statesWithProbabilityGreater0E) {
+ // Initialize environment for backward search.
+ storm::dd::DdManager<Type> const& manager = model.getManager();
+ storm::dd::Bdd<Type> statesWithProbability1E = statesWithProbabilityGreater0E;
+
+ uint_fast64_t iterations = 0;
+ bool outerLoopDone = false;
+ while (!outerLoopDone) {
+ storm::dd::Bdd<Type> innerStates = manager.getBddZero();
+
+ bool innerLoopDone = false;
+ while (!innerLoopDone) {
+ storm::dd::Bdd<Type> temporary = statesWithProbability1E.swapVariables(model.getRowColumnMetaVariablePairs());
+ temporary = transitionMatrix.implies(temporary).universalAbstract(model.getColumnVariables());
+
+ storm::dd::Bdd<Type> temporary2 = innerStates.swapVariables(model.getRowColumnMetaVariablePairs());
+ temporary2 = transitionMatrix.andExists(temporary2, model.getColumnVariables());
+
+ temporary = temporary.andExists(temporary2, model.getNondeterminismVariables());
+ temporary &= phiStates;
+ temporary |= psiStates;
+
+ if (innerStates == temporary) {
+ innerLoopDone = true;
+ } else {
+ innerStates = temporary;
+ }
+ }
+
+ if (statesWithProbability1E == innerStates) {
+ outerLoopDone = true;
+ } else {
+ statesWithProbability1E = innerStates;
+ }
+ ++iterations;
+ }
+
+ return statesWithProbability1E;
+ }
+
+ template <storm::dd::DdType Type>
+ std::pair<storm::dd::Bdd<Type>, storm::dd::Bdd<Type>> performProb01Max(storm::models::symbolic::NondeterministicModel<Type> const& model, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates) {
+ std::pair<storm::dd::Bdd<Type>, storm::dd::Bdd<Type>> result;
+ storm::dd::Bdd<Type> transitionMatrix = model.getTransitionMatrix().notZero();
+ result.first = performProb0A(model, transitionMatrix, phiStates, psiStates);
+ result.second = performProb1E(model, transitionMatrix, phiStates, psiStates, !result.first && model.getReachableStates());
+ return result;
+ }
+
+ template <storm::dd::DdType Type>
+ std::pair<storm::dd::Bdd<Type>, storm::dd::Bdd<Type>> performProb01Min(storm::models::symbolic::NondeterministicModel<Type> const& model, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates) {
+ std::pair<storm::dd::Bdd<Type>, storm::dd::Bdd<Type>> result;
+ storm::dd::Bdd<Type> transitionMatrix = model.getTransitionMatrix().notZero();
+ result.first = performProb0E(model, transitionMatrix, phiStates, psiStates);
+ result.second = performProb1A(model, transitionMatrix, phiStates, psiStates, !result.first && model.getReachableStates());
+ return result;
+ }
+
+ template <typename T>
+ std::vector<uint_fast64_t> getTopologicalSort(storm::storage::SparseMatrix<T> const& matrix) {
+ if (matrix.getRowCount() != matrix.getColumnCount()) {
+ LOG4CPLUS_ERROR(logger, "Provided matrix is required to be square.");
+ throw storm::exceptions::InvalidArgumentException() << "Provided matrix is required to be square.";
+ }
+
+ uint_fast64_t numberOfStates = matrix.getRowCount();
+
+ // Prepare the result. This relies on the matrix being square.
+ std::vector<uint_fast64_t> topologicalSort;
+ topologicalSort.reserve(numberOfStates);
+
+ // Prepare the stacks needed for recursion.
+ std::vector<uint_fast64_t> recursionStack;
+ recursionStack.reserve(matrix.getRowCount());
+ std::vector<typename storm::storage::SparseMatrix<T>::const_iterator> iteratorRecursionStack;
+ iteratorRecursionStack.reserve(numberOfStates);
+
+ // Perform a depth-first search over the given transitions and record states in the reverse order they were visited.
+ storm::storage::BitVector visitedStates(numberOfStates);
+ for (uint_fast64_t state = 0; state < numberOfStates; ++state) {
+ if (!visitedStates.get(state)) {
+ recursionStack.push_back(state);
+ iteratorRecursionStack.push_back(matrix.begin(state));
+
+ recursionStepForward:
+ while (!recursionStack.empty()) {
+ uint_fast64_t currentState = recursionStack.back();
+ typename storm::storage::SparseMatrix<T>::const_iterator successorIterator = iteratorRecursionStack.back();
+
+ visitedStates.set(currentState, true);
+
+ recursionStepBackward:
+ for (; successorIterator != matrix.end(currentState); ++successorIterator) {
+ if (!visitedStates.get(successorIterator->getColumn())) {
+ // Put unvisited successor on top of our recursion stack and remember that.
+ recursionStack.push_back(successorIterator->getColumn());
+
+ // Also, put initial value for iterator on corresponding recursion stack.
+ iteratorRecursionStack.push_back(matrix.begin(successorIterator->getColumn()));
+
+ goto recursionStepForward;
+ }
+ }
+
+ topologicalSort.push_back(currentState);
+
+ // If we reach this point, we have completed the recursive descent for the current state.
+ // That is, we need to pop it from the recursion stacks.
+ recursionStack.pop_back();
+ iteratorRecursionStack.pop_back();
+
+ // If there is at least one state under the current one in our recursion stack, we need
+ // to restore the topmost state as the current state and jump to the part after the
+ // original recursive call.
+ if (recursionStack.size() > 0) {
+ currentState = recursionStack.back();
+ successorIterator = iteratorRecursionStack.back();
+
+ goto recursionStepBackward;
+ }
+ }
+ }
+ }
+
+ return topologicalSort;
+ }
+
+
+
+ template <typename T>
+ std::pair<std::vector<T>, std::vector<uint_fast64_t>> performDijkstra(storm::models::sparse::Model<T> const& model,
+ storm::storage::SparseMatrix<T> const& transitions,
+ storm::storage::BitVector const& startingStates,
+ storm::storage::BitVector const* filterStates) {
+
+ LOG4CPLUS_INFO(logger, "Performing Dijkstra search.");
+
+ const uint_fast64_t noPredecessorValue = storm::utility::zero<uint_fast64_t>();
+ std::vector<T> probabilities(model.getNumberOfStates(), storm::utility::zero<T>());
+ std::vector<uint_fast64_t> predecessors(model.getNumberOfStates(), noPredecessorValue);
+
+ // Set the probability to 1 for all starting states.
+ std::set<std::pair<T, uint_fast64_t>, DistanceCompare<T>> probabilityStateSet;
+
+ for (auto state : startingStates) {
+ probabilityStateSet.emplace(storm::utility::one<T>(), state);
+ probabilities[state] = storm::utility::one<T>();
+ }
+
+ // As long as there is one reachable state, we need to consider it.
+ while (!probabilityStateSet.empty()) {
+ // Get the state with the least distance from the set and remove it.
+ std::pair<T, uint_fast64_t> probabilityStatePair = probabilityStateSet.erase(probabilityStateSet.begin());
+
+ // Now check the new distances for all successors of the current state.
+ typename storm::storage::SparseMatrix<T>::Rows row = transitions.getRow(probabilityStatePair.second);
+ for (auto const& transition : row) {
+ // Only follow the transition if it lies within the filtered states.
+ if (filterStates != nullptr && filterStates->get(transition.first)) {
+ // Calculate the distance we achieve when we take the path to the successor via the current state.
+ T newDistance = probabilityStatePair.first;
+ // We found a cheaper way to get to the target state of the transition.
+ if (newDistance > probabilities[transition.first]) {
+ // Remove the old distance.
+ if (probabilities[transition.first] != noPredecessorValue) {
+ probabilityStateSet.erase(std::make_pair(probabilities[transition.first], transition.first));
+ }
+
+ // Set and add the new distance.
+ probabilities[transition.first] = newDistance;
+ predecessors[transition.first] = probabilityStatePair.second;
+ probabilityStateSet.insert(std::make_pair(newDistance, transition.first));
+ }
+ }
+ }
+ }
+
+ // Move the values into the result and return it.
+ std::pair<std::vector<T>, std::vector<uint_fast64_t>> result;
+ result.first = std::move(probabilities);
+ result.second = std::move(predecessors);
+ LOG4CPLUS_INFO(logger, "Done performing Dijkstra search.");
+ return result;
+ }
+
+
+
+
+ template storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix<double> const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates);
+
+ template std::vector<std::size_t> getDistances(storm::storage::SparseMatrix<double> const& transitionMatrix, storm::storage::BitVector const& initialStates);
+
+
+ template storm::storage::BitVector performProbGreater0(storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0);
+
+ template storm::storage::BitVector performProb1(storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector const& statesWithProbabilityGreater0);
+
+
+ template storm::storage::BitVector performProb1(storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
+
+
+ template std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01(storm::models::sparse::DeterministicModel<double> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
+
+
+ template std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01(storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
+
+
+
+ template storm::storage::BitVector performProbGreater0E(storm::storage::SparseMatrix<double> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) ;
+
+ template storm::storage::BitVector performProb0A(storm::storage::SparseMatrix<double> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
+
+ template storm::storage::BitVector performProb0A(storm::models::sparse::NondeterministicModel<double> const& model, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ;
+
+ template storm::storage::BitVector performProb1E(storm::storage::SparseMatrix<double> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
+
+
+ template storm::storage::BitVector performProb1E(storm::models::sparse::NondeterministicModel<double> const& model, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
+
+ template std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Max(storm::storage::SparseMatrix<double> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ;
+
+
+ template std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Max(storm::models::sparse::NondeterministicModel<double> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ;
+
+ template storm::storage::BitVector performProbGreater0A(storm::storage::SparseMatrix<double> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0);
+
+
+ template storm::storage::BitVector performProb0E(storm::models::sparse::NondeterministicModel<double> const& model, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
+ template storm::storage::BitVector performProb0E(storm::storage::SparseMatrix<double> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ;
+
+
+ template storm::storage::BitVector performProb1A( storm::storage::SparseMatrix<double> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
+
+ template std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Min(storm::storage::SparseMatrix<double> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ;
+
+
+ template std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Min(storm::models::sparse::NondeterministicModel<double> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
+
+
+ template std::vector<uint_fast64_t> getTopologicalSort(storm::storage::SparseMatrix<double> const& matrix) ;
+
+
+
+ template storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix<float> const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates);
+
+ template std::vector<std::size_t> getDistances(storm::storage::SparseMatrix<float> const& transitionMatrix, storm::storage::BitVector const& initialStates);
+
+
+ template storm::storage::BitVector performProbGreater0(storm::storage::SparseMatrix<float> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0);
+
+ template storm::storage::BitVector performProb1(storm::storage::SparseMatrix<float> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector const& statesWithProbabilityGreater0);
+
+
+ template storm::storage::BitVector performProb1(storm::storage::SparseMatrix<float> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
+
+
+ template std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01(storm::models::sparse::DeterministicModel<float> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
+
+
+ template std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01(storm::storage::SparseMatrix<float> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
+
+
+
+ template storm::storage::BitVector performProbGreater0E(storm::storage::SparseMatrix<float> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<float> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) ;
+
+ template storm::storage::BitVector performProb0A(storm::storage::SparseMatrix<float> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<float> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
+
+ template storm::storage::BitVector performProb0A(storm::models::sparse::NondeterministicModel<float> const& model, storm::storage::SparseMatrix<float> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ;
+
+ template storm::storage::BitVector performProb1E(storm::storage::SparseMatrix<float> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<float> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
+
+
+ template storm::storage::BitVector performProb1E(storm::models::sparse::NondeterministicModel<float> const& model, storm::storage::SparseMatrix<float> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
+
+ template std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Max(storm::storage::SparseMatrix<float> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<float> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ;
+
+
+ template std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Max(storm::models::sparse::NondeterministicModel<float> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ;
+
+ template storm::storage::BitVector performProbGreater0A(storm::storage::SparseMatrix<float> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<float> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0);
+
+
+ template storm::storage::BitVector performProb0E(storm::models::sparse::NondeterministicModel<float> const& model, storm::storage::SparseMatrix<float> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
+ template storm::storage::BitVector performProb0E(storm::storage::SparseMatrix<float> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<float> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ;
+
+
+ template storm::storage::BitVector performProb1A( storm::storage::SparseMatrix<float> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<float> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
+
+ template std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Min(storm::storage::SparseMatrix<float> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<float> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ;
+
+
+ template std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Min(storm::models::sparse::NondeterministicModel<float> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
+
+
+ template std::vector<uint_fast64_t> getTopologicalSort(storm::storage::SparseMatrix<float> const& matrix) ;
+
+#ifdef STORM_HAVE_CARL
+
+
+ template storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates);
+
+ template std::vector<std::size_t> getDistances(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, storm::storage::BitVector const& initialStates);
+
+
+ template storm::storage::BitVector performProbGreater0(storm::storage::SparseMatrix<storm::RationalFunction> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0);
+
+ template storm::storage::BitVector performProb1(storm::storage::SparseMatrix<storm::RationalFunction> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector const& statesWithProbabilityGreater0);
+
+
+ template storm::storage::BitVector performProb1(storm::storage::SparseMatrix<storm::RationalFunction> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
+
+
+ template std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01(storm::models::sparse::DeterministicModel<storm::RationalFunction> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
+
+
+ template std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01(storm::storage::SparseMatrix<storm::RationalFunction> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
+
+
+
+ template storm::storage::BitVector performProbGreater0E(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<storm::RationalFunction> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) ;
+
+ template storm::storage::BitVector performProb0A(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<storm::RationalFunction> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
+
+ template storm::storage::BitVector performProb0A(storm::models::sparse::NondeterministicModel<storm::RationalFunction> const& model, storm::storage::SparseMatrix<storm::RationalFunction> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ;
+
+ template storm::storage::BitVector performProb1E(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<storm::RationalFunction> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
+
+
+ template storm::storage::BitVector performProb1E(storm::models::sparse::NondeterministicModel<storm::RationalFunction> const& model, storm::storage::SparseMatrix<storm::RationalFunction> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
+
+ template std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Max(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<storm::RationalFunction> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ;
+
+
+ template std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Max(storm::models::sparse::NondeterministicModel<storm::RationalFunction> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ;
+
+ template storm::storage::BitVector performProbGreater0A(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<storm::RationalFunction> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0);
+
+
+ template storm::storage::BitVector performProb0E(storm::models::sparse::NondeterministicModel<storm::RationalFunction> const& model, storm::storage::SparseMatrix<storm::RationalFunction> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
+ template storm::storage::BitVector performProb0E(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<storm::RationalFunction> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ;
+
+
+ template storm::storage::BitVector performProb1A( storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<storm::RationalFunction> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
+
+ template std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Min(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<storm::RationalFunction> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ;
+
+
+ template std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Min(storm::models::sparse::NondeterministicModel<storm::RationalFunction> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
+
+
+ template std::vector<uint_fast64_t> getTopologicalSort(storm::storage::SparseMatrix<storm::RationalFunction> const& matrix) ;
+
+#endif
+
+
+ template storm::dd::Bdd<storm::dd::DdType::CUDD> performProbGreater0(storm::models::symbolic::Model<storm::dd::DdType::CUDD> const& model, storm::dd::Bdd<storm::dd::DdType::CUDD> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::CUDD> const& phiStates, storm::dd::Bdd<storm::dd::DdType::CUDD> const& psiStates, boost::optional<uint_fast64_t> const& stepBound = boost::optional<uint_fast64_t>());
+
+ template storm::dd::Bdd<storm::dd::DdType::CUDD> performProb1(storm::models::symbolic::Model<storm::dd::DdType::CUDD> const& model, storm::dd::Bdd<storm::dd::DdType::CUDD> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::CUDD> const& phiStates, storm::dd::Bdd<storm::dd::DdType::CUDD> const& psiStates, storm::dd::Bdd<storm::dd::DdType::CUDD> const& statesWithProbabilityGreater0);
+
+
+ template storm::dd::Bdd<storm::dd::DdType::CUDD> performProb1(storm::models::symbolic::Model<storm::dd::DdType::CUDD> const& model, storm::dd::Bdd<storm::dd::DdType::CUDD> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::CUDD> const& phiStates, storm::dd::Bdd<storm::dd::DdType::CUDD> const& psiStates) ;
+
+
+ template std::pair<storm::dd::Bdd<storm::dd::DdType::CUDD>, storm::dd::Bdd<storm::dd::DdType::CUDD>> performProb01(storm::models::symbolic::DeterministicModel<storm::dd::DdType::CUDD> const& model, storm::dd::Bdd<storm::dd::DdType::CUDD> const& phiStates, storm::dd::Bdd<storm::dd::DdType::CUDD> const& psiStates);
+
+
+ template std::pair<storm::dd::Bdd<storm::dd::DdType::CUDD>, storm::dd::Bdd<storm::dd::DdType::CUDD>> performProb01(storm::models::symbolic::Model<storm::dd::DdType::CUDD> const& model, storm::dd::Add<storm::dd::DdType::CUDD> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::CUDD> const& phiStates, storm::dd::Bdd<storm::dd::DdType::CUDD> const& psiStates);
+
+
+ template storm::dd::Bdd<storm::dd::DdType::CUDD> performProbGreater0E(storm::models::symbolic::NondeterministicModel<storm::dd::DdType::CUDD> const& model, storm::dd::Bdd<storm::dd::DdType::CUDD> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::CUDD> const& phiStates, storm::dd::Bdd<storm::dd::DdType::CUDD> const& psiStates);
+
+ template storm::dd::Bdd<storm::dd::DdType::CUDD> performProb0A(storm::models::symbolic::NondeterministicModel<storm::dd::DdType::CUDD> const& model, storm::dd::Bdd<storm::dd::DdType::CUDD> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::CUDD> const& phiStates, storm::dd::Bdd<storm::dd::DdType::CUDD> const& psiStates) ;
+
+ template storm::dd::Bdd<storm::dd::DdType::CUDD> performProbGreater0A(storm::models::symbolic::NondeterministicModel<storm::dd::DdType::CUDD> const& model, storm::dd::Bdd<storm::dd::DdType::CUDD> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::CUDD> const& phiStates, storm::dd::Bdd<storm::dd::DdType::CUDD> const& psiStates) ;
+
+ template storm::dd::Bdd<storm::dd::DdType::CUDD> performProb0E(storm::models::symbolic::NondeterministicModel<storm::dd::DdType::CUDD> const& model, storm::dd::Bdd<storm::dd::DdType::CUDD> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::CUDD> const& phiStates, storm::dd::Bdd<storm::dd::DdType::CUDD> const& psiStates) ;
+
+
+ template storm::dd::Bdd<storm::dd::DdType::CUDD> performProb1A(storm::models::symbolic::NondeterministicModel<storm::dd::DdType::CUDD> const& model, storm::dd::Bdd<storm::dd::DdType::CUDD> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::CUDD> const& phiStates, storm::dd::Bdd<storm::dd::DdType::CUDD> const& psiStates, storm::dd::Bdd<storm::dd::DdType::CUDD> const& statesWithProbabilityGreater0A);
+
+
+ template storm::dd::Bdd<storm::dd::DdType::CUDD> performProb1E(storm::models::symbolic::NondeterministicModel<storm::dd::DdType::CUDD> const& model, storm::dd::Bdd<storm::dd::DdType::CUDD> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::CUDD> const& phiStates, storm::dd::Bdd<storm::dd::DdType::CUDD> const& psiStates, storm::dd::Bdd<storm::dd::DdType::CUDD> const& statesWithProbabilityGreater0E) ;
+
+
+ template std::pair<storm::dd::Bdd<storm::dd::DdType::CUDD>, storm::dd::Bdd<storm::dd::DdType::CUDD>> performProb01Max(storm::models::symbolic::NondeterministicModel<storm::dd::DdType::CUDD> const& model, storm::dd::Bdd<storm::dd::DdType::CUDD> const& phiStates, storm::dd::Bdd<storm::dd::DdType::CUDD> const& psiStates) ;
+
+
+ template std::pair<storm::dd::Bdd<storm::dd::DdType::CUDD>, storm::dd::Bdd<storm::dd::DdType::CUDD>> performProb01Min(storm::models::symbolic::NondeterministicModel<storm::dd::DdType::CUDD> const& model, storm::dd::Bdd<storm::dd::DdType::CUDD> const& phiStates, storm::dd::Bdd<storm::dd::DdType::CUDD> const& psiStates) ;
+
+
+
+ } // namespace graph
+ } // namespace utility
+} // namespace storm
+
diff --git a/src/utility/graph.h b/src/utility/graph.h
index 1f424c98d..3ae26d34f 100644
--- a/src/utility/graph.h
+++ b/src/utility/graph.h
@@ -7,19 +7,33 @@
#include "utility/OsDetection.h"
#include "src/storage/sparse/StateType.h"
-#include "src/models/symbolic/DeterministicModel.h"
-#include "src/models/symbolic/NondeterministicModel.h"
-#include "src/models/sparse/DeterministicModel.h"
#include "src/models/sparse/NondeterministicModel.h"
-#include "src/utility/constants.h"
-#include "src/exceptions/InvalidArgumentException.h"
-
-#include "log4cplus/logger.h"
-#include "log4cplus/loggingmacros.h"
-
-extern log4cplus::Logger logger;
+#include "src/models/sparse/DeterministicModel.h"
+#include "src/storage/dd/DdType.h"
namespace storm {
+ namespace storage {
+ class BitVector;
+ template<typename VT> class SparseMatrix;
+ }
+
+ namespace models {
+
+ namespace symbolic {
+ template<storm::dd::DdType T> class Model;
+ template<storm::dd::DdType T> class DeterministicModel;
+ template<storm::dd::DdType T> class NondeterministicModel;
+ }
+
+ }
+
+ namespace dd {
+ template<storm::dd::DdType T> class Bdd;
+ template<storm::dd::DdType T> class Add;
+
+ }
+
+
namespace utility {
namespace graph {
@@ -34,38 +48,7 @@ namespace storm {
* @param targetStates The target states that may not be passed.
*/
template<typename T>
- storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix<T> const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates) {
- storm::storage::BitVector reachableStates(initialStates);
-
- // Initialize the stack used for the DFS with the states.
- std::vector<uint_fast64_t> stack(initialStates.begin(), initialStates.end());
-
- // Perform the actual DFS.
- uint_fast64_t currentState = 0;
- while (!stack.empty()) {
- currentState = stack.back();
- stack.pop_back();
-
- for (auto const& successor : transitionMatrix.getRowGroup(currentState)) {
- // Only explore the state if the transition was actually there and the successor has not yet
- // been visited.
- if (successor.getValue() != storm::utility::zero<T>() && !reachableStates.get(successor.getColumn())) {
- // If the successor is one of the target states, we need to include it, but must not explore
- // it further.
- if (targetStates.get(successor.getColumn())) {
- reachableStates.set(successor.getColumn());
- } else if (constraintStates.get(successor.getColumn())) {
- // However, if the state is in the constrained set of states, we need to follow it.
- reachableStates.set(successor.getColumn());
- stack.push_back(successor.getColumn());
- }
- }
- }
- }
-
- return reachableStates;
- }
-
+ storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix<T> const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates);
/*!
* Performs a breadth-first search through the underlying graph structure to compute the distance from all
* states to the starting states of the search.
@@ -75,35 +58,7 @@ namespace storm {
* @return The distances of each state to the initial states of the sarch.
*/
template<typename T>
- std::vector<std::size_t> getDistances(storm::storage::SparseMatrix<T> const& transitionMatrix, storm::storage::BitVector const& initialStates) {
- std::vector<std::size_t> distances(transitionMatrix.getRowGroupCount());
-
- std::vector<std::pair<storm::storage::sparse::state_type, std::size_t>> stateQueue;
- stateQueue.reserve(transitionMatrix.getRowGroupCount());
- storm::storage::BitVector statesInQueue(transitionMatrix.getRowGroupCount());
-
- storm::storage::sparse::state_type currentPosition = 0;
- for (auto const& initialState : initialStates) {
- stateQueue.emplace_back(initialState, 0);
- statesInQueue.set(initialState);
- }
-
- // Perform a BFS.
- while (currentPosition < stateQueue.size()) {
- std::pair<storm::storage::sparse::state_type, std::size_t> const& stateDistancePair = stateQueue[currentPosition];
- distances[stateDistancePair.first] = stateDistancePair.second;
-
- for (auto const& successorEntry : transitionMatrix.getRowGroup(stateDistancePair.first)) {
- if (!statesInQueue.get(successorEntry.getColumn())) {
- stateQueue.emplace_back(successorEntry.getColumn(), stateDistancePair.second + 1);
- statesInQueue.set(successorEntry.getColumn());
- }
- }
- ++currentPosition;
- }
-
- return distances;
- }
+ std::vector<std::size_t> getDistances(storm::storage::SparseMatrix<T> const& transitionMatrix, storm::storage::BitVector const& initialStates);
/*!
* Performs a backward depth-first search trough the underlying graph structure
@@ -118,61 +73,7 @@ namespace storm {
* @return A bit vector with all indices of states that have a probability greater than 0.
*/
template <typename T>
- 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) {
- // Prepare the resulting bit vector.
- uint_fast64_t numberOfStates = phiStates.size();
- storm::storage::BitVector statesWithProbabilityGreater0(numberOfStates);
-
- // Add all psi states as they already satisfy the condition.
- statesWithProbabilityGreater0 |= psiStates;
-
- // Initialize the stack used for the DFS with the states.
- std::vector<uint_fast64_t> stack(psiStates.begin(), psiStates.end());
-
- // Initialize the stack for the step bound, if the number of steps is bounded.
- std::vector<uint_fast64_t> stepStack;
- std::vector<uint_fast64_t> remainingSteps;
- if (useStepBound) {
- stepStack.reserve(numberOfStates);
- stepStack.insert(stepStack.begin(), psiStates.getNumberOfSetBits(), maximalSteps);
- remainingSteps.resize(numberOfStates);
- for (auto state : psiStates) {
- remainingSteps[state] = maximalSteps;
- }
- }
-
- // Perform the actual DFS.
- uint_fast64_t currentState, currentStepBound;
- while (!stack.empty()) {
- currentState = stack.back();
- stack.pop_back();
-
- if (useStepBound) {
- currentStepBound = stepStack.back();
- stepStack.pop_back();
- }
-
- for (typename storm::storage::SparseMatrix<T>::const_iterator entryIt = backwardTransitions.begin(currentState), entryIte = backwardTransitions.end(currentState); entryIt != entryIte; ++entryIt) {
- if (phiStates[entryIt->getColumn()] && (!statesWithProbabilityGreater0.get(entryIt->getColumn()) || (useStepBound && remainingSteps[entryIt->getColumn()] < currentStepBound - 1))) {
- // If we don't have a bound on the number of steps to take, just add the state to the stack.
- if (!useStepBound) {
- statesWithProbabilityGreater0.set(entryIt->getColumn(), true);
- stack.push_back(entryIt->getColumn());
- } else if (currentStepBound > 0) {
- // If there is at least one more step to go, we need to push the state and the new number of steps.
- remainingSteps[entryIt->getColumn()] = currentStepBound - 1;
- statesWithProbabilityGreater0.set(entryIt->getColumn(), true);
- stack.push_back(entryIt->getColumn());
- stepStack.push_back(currentStepBound - 1);
- }
- }
- }
- }
-
- // Return result.
- return statesWithProbabilityGreater0;
- }
-
+ 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);
/*!
* Computes the set of states of the given model for which all paths lead to
* the given set of target states and only visit states from the filter set
@@ -188,11 +89,7 @@ namespace storm {
* @return A bit vector with all indices of states that have a probability greater than 1.
*/
template <typename T>
- storm::storage::BitVector performProb1(storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector const& statesWithProbabilityGreater0) {
- storm::storage::BitVector statesWithProbability1 = performProbGreater0(backwardTransitions, ~psiStates, ~statesWithProbabilityGreater0);
- statesWithProbability1.complement();
- return statesWithProbability1;
- }
+ storm::storage::BitVector performProb1(storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector const& statesWithProbabilityGreater0);
/*!
* Computes the set of states of the given model for which all paths lead to
@@ -207,12 +104,7 @@ namespace storm {
* @return A bit vector with all indices of states that have a probability greater than 1.
*/
template <typename T>
- storm::storage::BitVector performProb1(storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
- storm::storage::BitVector statesWithProbabilityGreater0 = performProbGreater0(backwardTransitions, phiStates, psiStates);
- storm::storage::BitVector statesWithProbability1 = performProbGreater0(backwardTransitions, ~psiStates, ~(statesWithProbabilityGreater0));
- statesWithProbability1.complement();
- return statesWithProbability1;
- }
+ storm::storage::BitVector performProb1(storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
/*!
* Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi until psi in a
@@ -225,14 +117,7 @@ namespace storm {
* with probability 0 and the second stores all indices of states with probability 1.
*/
template <typename T>
- static std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01(storm::models::sparse::DeterministicModel<T> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
- std::pair<storm::storage::BitVector, storm::storage::BitVector> result;
- storm::storage::SparseMatrix<T> backwardTransitions = model.getBackwardTransitions();
- result.first = performProbGreater0(backwardTransitions, phiStates, psiStates);
- result.second = performProb1(backwardTransitions, phiStates, psiStates, result.first);
- result.first.complement();
- return result;
- }
+ std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01(storm::models::sparse::DeterministicModel<T> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
/*!
* Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi until psi in a
@@ -245,13 +130,8 @@ namespace storm {
* with probability 0 and the second stores all indices of states with probability 1.
*/
template <typename T>
- static std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01(storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
- std::pair<storm::storage::BitVector, storm::storage::BitVector> result;
- result.first = performProbGreater0(backwardTransitions, phiStates, psiStates);
- result.second = performProb1(backwardTransitions, phiStates, psiStates, result.first);
- result.first.complement();
- return result;
- }
+ std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01(storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
+
/*!
* Computes the set of states that has a positive probability of reaching psi states after only passing
@@ -265,30 +145,7 @@ namespace storm {
* @return All states with positive probability.
*/
template <storm::dd::DdType Type>
- storm::dd::Bdd<Type> performProbGreater0(storm::models::symbolic::Model<Type> const& model, storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates, boost::optional<uint_fast64_t> const& stepBound = boost::optional<uint_fast64_t>()) {
- // Initialize environment for backward search.
- storm::dd::DdManager<Type> const& manager = model.getManager();
- storm::dd::Bdd<Type> lastIterationStates = manager.getBddZero();
- storm::dd::Bdd<Type> statesWithProbabilityGreater0 = psiStates;
-
- uint_fast64_t iterations = 0;
- while (lastIterationStates != statesWithProbabilityGreater0) {
- if (stepBound && iterations >= stepBound.get()) {
- break;
- }
-
- lastIterationStates = statesWithProbabilityGreater0;
- statesWithProbabilityGreater0 = statesWithProbabilityGreater0.swapVariables(model.getRowColumnMetaVariablePairs());
- statesWithProbabilityGreater0 &= transitionMatrix;
- statesWithProbabilityGreater0 = statesWithProbabilityGreater0.existsAbstract(model.getColumnVariables());
- statesWithProbabilityGreater0 &= phiStates;
- statesWithProbabilityGreater0 |= lastIterationStates;
- ++iterations;
- }
-
- return statesWithProbabilityGreater0;
- }
-
+ storm::dd::Bdd<Type> performProbGreater0(storm::models::symbolic::Model<Type> const& model, storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates, boost::optional<uint_fast64_t> const& stepBound = boost::optional<uint_fast64_t>());
/*!
* Computes the set of states that have a probability of one of reaching psi states after only passing
* through phi states before.
@@ -302,11 +159,7 @@ namespace storm {
* @return All states with probability 1.
*/
template <storm::dd::DdType Type>
- storm::dd::Bdd<Type> performProb1(storm::models::symbolic::Model<Type> const& model, storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates, storm::dd::Bdd<Type> const& statesWithProbabilityGreater0) {
- storm::dd::Bdd<Type> statesWithProbability1 = performProbGreater0(model, transitionMatrix, !psiStates && model.getReachableStates(), !statesWithProbabilityGreater0 && model.getReachableStates());
- statesWithProbability1 = !statesWithProbability1 && model.getReachableStates();
- return statesWithProbability1;
- }
+ storm::dd::Bdd<Type> performProb1(storm::models::symbolic::Model<Type> const& model, storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates, storm::dd::Bdd<Type> const& statesWithProbabilityGreater0);
/*!
* Computes the set of states that have a probability of one of reaching psi states after only passing
@@ -319,10 +172,7 @@ namespace storm {
* @return All states with probability 1.
*/
template <storm::dd::DdType Type>
- storm::dd::Bdd<Type> performProb1(storm::models::symbolic::Model<Type> const& model, storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates) {
- storm::dd::Bdd<Type> statesWithProbabilityGreater0 = performProbGreater0(model, transitionMatrix, phiStates, psiStates);
- return performProb1(model, transitionMatrix, phiStates, psiStates, statesWithProbabilityGreater0);
- }
+ storm::dd::Bdd<Type> performProb1(storm::models::symbolic::Model<Type> const& model, storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates) ;
/*!
* Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi until psi in a
@@ -334,14 +184,7 @@ namespace storm {
* @return A pair of BDDs that represent all states with probability 0 and 1, respectively.
*/
template <storm::dd::DdType Type>
- static std::pair<storm::dd::Bdd<Type>, storm::dd::Bdd<Type>> performProb01(storm::models::symbolic::DeterministicModel<Type> const& model, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates) {
- std::pair<storm::dd::Bdd<Type>, storm::dd::Bdd<Type>> result;
- storm::dd::Bdd<Type> transitionMatrix = model.getTransitionMatrix().notZero();
- result.first = performProbGreater0(model, transitionMatrix, phiStates, psiStates);
- result.second = !performProbGreater0(model, transitionMatrix, !psiStates && model.getReachableStates(), !result.first && model.getReachableStates()) && model.getReachableStates();
- result.first = !result.first && model.getReachableStates();
- return result;
- }
+ std::pair<storm::dd::Bdd<Type>, storm::dd::Bdd<Type>> performProb01(storm::models::symbolic::DeterministicModel<Type> const& model, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates);
/*!
* Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi until psi in a
@@ -354,14 +197,7 @@ namespace storm {
* @return A pair of BDDs that represent all states with probability 0 and 1, respectively.
*/
template <storm::dd::DdType Type>
- static std::pair<storm::dd::Bdd<Type>, storm::dd::Bdd<Type>> performProb01(storm::models::symbolic::Model<Type> const& model, storm::dd::Add<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates) {
- std::pair<storm::dd::Bdd<Type>, storm::dd::Bdd<Type>> result;
- storm::dd::Bdd<Type> transitionMatrixBdd = transitionMatrix.notZero();
- result.first = performProbGreater0(model, transitionMatrixBdd, phiStates, psiStates);
- result.second = !performProbGreater0(model, transitionMatrixBdd, !psiStates && model.getReachableStates(), !result.first && model.getReachableStates()) && model.getReachableStates();
- result.first = !result.first && model.getReachableStates();
- return result;
- }
+ std::pair<storm::dd::Bdd<Type>, storm::dd::Bdd<Type>> performProb01(storm::models::symbolic::Model<Type> const& model, storm::dd::Add<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates);
/*!
* Computes the sets of states that have probability greater 0 of satisfying phi until psi under at least
@@ -378,67 +214,10 @@ namespace storm {
* @return A bit vector that represents all states with probability 0.
*/
template <typename T>
- storm::storage::BitVector performProbGreater0E(storm::storage::SparseMatrix<T> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) {
- size_t numberOfStates = phiStates.size();
-
- // Prepare resulting bit vector.
- storm::storage::BitVector statesWithProbabilityGreater0(numberOfStates);
-
- // Add all psi states as the already satisfy the condition.
- statesWithProbabilityGreater0 |= psiStates;
-
- // Initialize the stack used for the DFS with the states
- std::vector<uint_fast64_t> stack(psiStates.begin(), psiStates.end());
-
- // Initialize the stack for the step bound, if the number of steps is bounded.
- std::vector<uint_fast64_t> stepStack;
- std::vector<uint_fast64_t> remainingSteps;
- if (useStepBound) {
- stepStack.reserve(numberOfStates);
- stepStack.insert(stepStack.begin(), psiStates.getNumberOfSetBits(), maximalSteps);
- remainingSteps.resize(numberOfStates);
- for (auto state : psiStates) {
- remainingSteps[state] = maximalSteps;
- }
- }
-
- // Perform the actual DFS.
- uint_fast64_t currentState, currentStepBound;
- while (!stack.empty()) {
- currentState = stack.back();
- stack.pop_back();
-
- if (useStepBound) {
- currentStepBound = stepStack.back();
- stepStack.pop_back();
- }
-
- for (typename storm::storage::SparseMatrix<T>::const_iterator entryIt = backwardTransitions.begin(currentState), entryIte = backwardTransitions.end(currentState); entryIt != entryIte; ++entryIt) {
- if (phiStates.get(entryIt->getColumn()) && (!statesWithProbabilityGreater0.get(entryIt->getColumn()) || (useStepBound && remainingSteps[entryIt->getColumn()] < currentStepBound - 1))) {
- // If we don't have a bound on the number of steps to take, just add the state to the stack.
- if (!useStepBound) {
- statesWithProbabilityGreater0.set(entryIt->getColumn(), true);
- stack.push_back(entryIt->getColumn());
- } else if (currentStepBound > 0) {
- // If there is at least one more step to go, we need to push the state and the new number of steps.
- remainingSteps[entryIt->getColumn()] = currentStepBound - 1;
- statesWithProbabilityGreater0.set(entryIt->getColumn(), true);
- stack.push_back(entryIt->getColumn());
- stepStack.push_back(currentStepBound - 1);
- }
- }
- }
- }
-
- return statesWithProbabilityGreater0;
- }
+ storm::storage::BitVector performProbGreater0E(storm::storage::SparseMatrix<T> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) ;
template <typename T>
- storm::storage::BitVector performProb0A(storm::storage::SparseMatrix<T> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
- storm::storage::BitVector statesWithProbability0 = performProbGreater0E(transitionMatrix, nondeterministicChoiceIndices, backwardTransitions, phiStates, psiStates);
- statesWithProbability0.complement();
- return statesWithProbability0;
- }
+ storm::storage::BitVector performProb0A(storm::storage::SparseMatrix<T> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
/*!
* Computes the sets of states that have probability 0 of satisfying phi until psi under all
@@ -455,10 +234,7 @@ namespace storm {
* @return A bit vector that represents all states with probability 0.
*/
template <typename T>
- storm::storage::BitVector performProb0A(storm::models::sparse::NondeterministicModel<T> const& model, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
- return performProb0A(model.getTransitionMatrix(), model.getNondeterministicChoiceIndices(), backwardTransitions, phiStates, psiStates);
- }
-
+ storm::storage::BitVector performProb0A(storm::models::sparse::NondeterministicModel<T> const& model, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ;
/*!
* Computes the sets of states that have probability 1 of satisfying phi until psi under at least
* one possible resolution of non-determinism in a non-deterministic model. Stated differently,
@@ -472,62 +248,7 @@ namespace storm {
* @return A bit vector that represents all states with probability 1.
*/
template <typename T>
- storm::storage::BitVector performProb1E(storm::storage::SparseMatrix<T> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
- size_t numberOfStates = phiStates.size();
-
- // Initialize the environment for the iterative algorithm.
- storm::storage::BitVector currentStates(numberOfStates, true);
- std::vector<uint_fast64_t> stack;
- stack.reserve(numberOfStates);
-
- // Perform the loop as long as the set of states gets larger.
- bool done = false;
- uint_fast64_t currentState;
- while (!done) {
- stack.clear();
- storm::storage::BitVector nextStates(psiStates);
- stack.insert(stack.end(), psiStates.begin(), psiStates.end());
-
- while (!stack.empty()) {
- currentState = stack.back();
- stack.pop_back();
-
- for (typename storm::storage::SparseMatrix<T>::const_iterator predecessorEntryIt = backwardTransitions.begin(currentState), predecessorEntryIte = backwardTransitions.end(currentState); predecessorEntryIt != predecessorEntryIte; ++predecessorEntryIt) {
- if (phiStates.get(predecessorEntryIt->getColumn()) && !nextStates.get(predecessorEntryIt->getColumn())) {
- // Check whether the predecessor has only successors in the current state set for one of the
- // nondeterminstic choices.
- for (uint_fast64_t row = nondeterministicChoiceIndices[predecessorEntryIt->getColumn()]; row < nondeterministicChoiceIndices[predecessorEntryIt->getColumn() + 1]; ++row) {
- bool allSuccessorsInCurrentStates = true;
- for (typename storm::storage::SparseMatrix<T>::const_iterator successorEntryIt = transitionMatrix.begin(row), successorEntryIte = transitionMatrix.end(row); successorEntryIt != successorEntryIte; ++successorEntryIt) {
- if (!currentStates.get(successorEntryIt->getColumn())) {
- allSuccessorsInCurrentStates = false;
- break;
- }
- }
-
- // If all successors for a given nondeterministic choice are in the current state set, we
- // add it to the set of states for the next iteration and perform a backward search from
- // that state.
- if (allSuccessorsInCurrentStates) {
- nextStates.set(predecessorEntryIt->getColumn(), true);
- stack.push_back(predecessorEntryIt->getColumn());
- break;
- }
- }
- }
- }
- }
-
- // Check whether we need to perform an additional iteration.
- if (currentStates == nextStates) {
- done = true;
- } else {
- currentStates = std::move(nextStates);
- }
- }
-
- return currentStates;
- }
+ storm::storage::BitVector performProb1E(storm::storage::SparseMatrix<T> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
/*!
* Computes the sets of states that have probability 1 of satisfying phi until psi under at least
@@ -542,18 +263,10 @@ namespace storm {
* @return A bit vector that represents all states with probability 1.
*/
template <typename T>
- storm::storage::BitVector performProb1E(storm::models::sparse::NondeterministicModel<T> const& model, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
- return performProb1E(model.getTransitionMatrix(), model.getNondeterministicChoiceIndices(), backwardTransitions, phiStates, psiStates);
- }
+ storm::storage::BitVector performProb1E(storm::models::sparse::NondeterministicModel<T> const& model, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
template <typename T>
- std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Max(storm::storage::SparseMatrix<T> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
- std::pair<storm::storage::BitVector, storm::storage::BitVector> result;
-
- result.first = performProb0A(transitionMatrix, nondeterministicChoiceIndices, backwardTransitions, phiStates, psiStates);
- result.second = performProb1E(transitionMatrix, nondeterministicChoiceIndices, backwardTransitions, phiStates, psiStates);
- return result;
- }
+ std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Max(storm::storage::SparseMatrix<T> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ;
/*!
* Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi
@@ -566,9 +279,7 @@ namespace storm {
* @return A pair of bit vectors that represent all states with probability 0 and 1, respectively.
*/
template <typename T>
- std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Max(storm::models::sparse::NondeterministicModel<T> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
- return performProb01Max(model.getTransitionMatrix(), model.getTransitionMatrix().getRowGroupIndices(), model.getBackwardTransitions(), phiStates, psiStates);
- }
+ std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Max(storm::models::sparse::NondeterministicModel<T> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ;
/*!
* Computes the sets of states that have probability greater 0 of satisfying phi until psi under any
@@ -585,81 +296,7 @@ namespace storm {
* @return A bit vector that represents all states with probability 0.
*/
template <typename T>
- storm::storage::BitVector performProbGreater0A(storm::storage::SparseMatrix<T> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) {
- size_t numberOfStates = phiStates.size();
-
- // Prepare resulting bit vector.
- storm::storage::BitVector statesWithProbabilityGreater0(numberOfStates);
-
- // Add all psi states as the already satisfy the condition.
- statesWithProbabilityGreater0 |= psiStates;
-
- // Initialize the stack used for the DFS with the states
- std::vector<uint_fast64_t> stack(psiStates.begin(), psiStates.end());
-
- // Initialize the stack for the step bound, if the number of steps is bounded.
- std::vector<uint_fast64_t> stepStack;
- std::vector<uint_fast64_t> remainingSteps;
- if (useStepBound) {
- stepStack.reserve(numberOfStates);
- stepStack.insert(stepStack.begin(), psiStates.getNumberOfSetBits(), maximalSteps);
- remainingSteps.resize(numberOfStates);
- for (auto state : psiStates) {
- remainingSteps[state] = maximalSteps;
- }
- }
-
- // Perform the actual DFS.
- uint_fast64_t currentState, currentStepBound;
- while(!stack.empty()) {
- currentState = stack.back();
- stack.pop_back();
-
- if (useStepBound) {
- currentStepBound = stepStack.back();
- stepStack.pop_back();
- }
-
- for(typename storm::storage::SparseMatrix<T>::const_iterator predecessorEntryIt = backwardTransitions.begin(currentState), predecessorEntryIte = backwardTransitions.end(currentState); predecessorEntryIt != predecessorEntryIte; ++predecessorEntryIt) {
- if (phiStates.get(predecessorEntryIt->getColumn()) && (!statesWithProbabilityGreater0.get(predecessorEntryIt->getColumn()) || (useStepBound && remainingSteps[predecessorEntryIt->getColumn()] < currentStepBound - 1))) {
- // Check whether the predecessor has at least one successor in the current state set for every
- // nondeterministic choice.
- bool addToStatesWithProbabilityGreater0 = true;
- for (uint_fast64_t row = nondeterministicChoiceIndices[predecessorEntryIt->getColumn()]; row < nondeterministicChoiceIndices[predecessorEntryIt->getColumn() + 1]; ++row) {
- bool hasAtLeastOneSuccessorWithProbabilityGreater0 = false;
- for (typename storm::storage::SparseMatrix<T>::const_iterator successorEntryIt = transitionMatrix.begin(row), successorEntryIte = transitionMatrix.end(row); successorEntryIt != successorEntryIte; ++successorEntryIt) {
- if (statesWithProbabilityGreater0.get(successorEntryIt->getColumn())) {
- hasAtLeastOneSuccessorWithProbabilityGreater0 = true;
- break;
- }
- }
-
- if (!hasAtLeastOneSuccessorWithProbabilityGreater0) {
- addToStatesWithProbabilityGreater0 = false;
- break;
- }
- }
-
- // If we need to add the state, then actually add it and perform further search from the state.
- if (addToStatesWithProbabilityGreater0) {
- // If we don't have a bound on the number of steps to take, just add the state to the stack.
- if (!useStepBound) {
- statesWithProbabilityGreater0.set(predecessorEntryIt->getColumn(), true);
- stack.push_back(predecessorEntryIt->getColumn());
- } else if (currentStepBound > 0) {
- // If there is at least one more step to go, we need to push the state and the new number of steps.
- remainingSteps[predecessorEntryIt->getColumn()] = currentStepBound - 1;
- statesWithProbabilityGreater0.set(predecessorEntryIt->getColumn(), true);
- stack.push_back(predecessorEntryIt->getColumn());
- stepStack.push_back(currentStepBound - 1);
- }
- }
- }
- }
- }
-
- return statesWithProbabilityGreater0;
- }
+ storm::storage::BitVector performProbGreater0A(storm::storage::SparseMatrix<T> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0);
/*!
* Computes the sets of states that have probability 0 of satisfying phi until psi under at least
@@ -674,18 +311,9 @@ namespace storm {
* @return A bit vector that represents all states with probability 0.
*/
template <typename T>
- storm::storage::BitVector performProb0E(storm::models::sparse::NondeterministicModel<T> const& model, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
- storm::storage::BitVector statesWithProbability0 = performProbGreater0A(model.getTransitionMatrix(), model.getNondeterministicChoiceIndices(), backwardTransitions, phiStates, psiStates);
- statesWithProbability0.complement();
- return statesWithProbability0;
- }
-
+ storm::storage::BitVector performProb0E(storm::models::sparse::NondeterministicModel<T> const& model, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
template <typename T>
- storm::storage::BitVector performProb0E(storm::storage::SparseMatrix<T> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
- storm::storage::BitVector statesWithProbability0 = performProbGreater0A(transitionMatrix, nondeterministicChoiceIndices, backwardTransitions, phiStates, psiStates);
- statesWithProbability0.complement();
- return statesWithProbability0;
- }
+ storm::storage::BitVector performProb0E(storm::storage::SparseMatrix<T> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ;
/*!
* Computes the sets of states that have probability 1 of satisfying phi until psi under all
@@ -700,79 +328,10 @@ namespace storm {
* @return A bit vector that represents all states with probability 0.
*/
template <typename T>
- storm::storage::BitVector performProb1A( storm::storage::SparseMatrix<T> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
- size_t numberOfStates = phiStates.size();
-
- // Initialize the environment for the iterative algorithm.
- storm::storage::BitVector currentStates(numberOfStates, true);
- std::vector<uint_fast64_t> stack;
- stack.reserve(numberOfStates);
-
- // Perform the loop as long as the set of states gets smaller.
- bool done = false;
- uint_fast64_t currentState;
- while (!done) {
- stack.clear();
- storm::storage::BitVector nextStates(psiStates);
- stack.insert(stack.end(), psiStates.begin(), psiStates.end());
-
- while (!stack.empty()) {
- currentState = stack.back();
- stack.pop_back();
-
- for(typename storm::storage::SparseMatrix<T>::const_iterator predecessorEntryIt = backwardTransitions.begin(currentState), predecessorEntryIte = backwardTransitions.end(currentState); predecessorEntryIt != predecessorEntryIte; ++predecessorEntryIt) {
- if (phiStates.get(predecessorEntryIt->getColumn()) && !nextStates.get(predecessorEntryIt->getColumn())) {
- // Check whether the predecessor has only successors in the current state set for all of the
- // nondeterminstic choices and that for each choice there exists a successor that is already
- // in the next states.
- bool addToStatesWithProbability1 = true;
- for (uint_fast64_t row = nondeterministicChoiceIndices[predecessorEntryIt->getColumn()]; row < nondeterministicChoiceIndices[predecessorEntryIt->getColumn() + 1]; ++row) {
- bool hasAtLeastOneSuccessorWithProbability1 = false;
- for (typename storm::storage::SparseMatrix<T>::const_iterator successorEntryIt = transitionMatrix.begin(row), successorEntryIte = transitionMatrix.end(row); successorEntryIt != successorEntryIte; ++successorEntryIt) {
- if (!currentStates.get(successorEntryIt->getColumn())) {
- addToStatesWithProbability1 = false;
- goto afterCheckLoop;
- }
- if (nextStates.get(successorEntryIt->getColumn())) {
- hasAtLeastOneSuccessorWithProbability1 = true;
- }
- }
-
- if (!hasAtLeastOneSuccessorWithProbability1) {
- addToStatesWithProbability1 = false;
- break;
- }
- }
-
- afterCheckLoop:
- // If all successors for all nondeterministic choices are in the current state set, we
- // add it to the set of states for the next iteration and perform a backward search from
- // that state.
- if (addToStatesWithProbability1) {
- nextStates.set(predecessorEntryIt->getColumn(), true);
- stack.push_back(predecessorEntryIt->getColumn());
- }
- }
- }
- }
-
- // Check whether we need to perform an additional iteration.
- if (currentStates == nextStates) {
- done = true;
- } else {
- currentStates = std::move(nextStates);
- }
- }
- return currentStates;
- }
+ storm::storage::BitVector performProb1A( storm::storage::SparseMatrix<T> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
template <typename T>
- std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Min(storm::storage::SparseMatrix<T> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
- std::pair<storm::storage::BitVector, storm::storage::BitVector> result;
- result.first = performProb0E(transitionMatrix, nondeterministicChoiceIndices, backwardTransitions, phiStates, psiStates);
- result.second = performProb1A(transitionMatrix, nondeterministicChoiceIndices, backwardTransitions, phiStates, psiStates);
- return result;
- }
+ std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Min(storm::storage::SparseMatrix<T> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ;
/*!
* Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi
@@ -785,9 +344,7 @@ namespace storm {
* @return A pair of bit vectors that represent all states with probability 0 and 1, respectively.
*/
template <typename T>
- std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Min(storm::models::sparse::NondeterministicModel<T> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
- return performProb01Min(model.getTransitionMatrix(), model.getTransitionMatrix().getRowGroupIndices(), model.getBackwardTransitions(), phiStates, psiStates);
- }
+ std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Min(storm::models::sparse::NondeterministicModel<T> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
/*!
* Computes the set of states for which there exists a scheduler that achieves a probability greater than
@@ -800,26 +357,7 @@ namespace storm {
* @return A BDD representing all such states.
*/
template <storm::dd::DdType Type>
- storm::dd::Bdd<Type> performProbGreater0E(storm::models::symbolic::NondeterministicModel<Type> const& model, storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates) {
- // Initialize environment for backward search.
- storm::dd::DdManager<Type> const& manager = model.getManager();
- storm::dd::Bdd<Type> lastIterationStates = manager.getBddZero();
- storm::dd::Bdd<Type> statesWithProbabilityGreater0E = psiStates;
-
- uint_fast64_t iterations = 0;
- storm::dd::Bdd<Type> abstractedTransitionMatrix = transitionMatrix.existsAbstract(model.getNondeterminismVariables());
- while (lastIterationStates != statesWithProbabilityGreater0E) {
- lastIterationStates = statesWithProbabilityGreater0E;
- statesWithProbabilityGreater0E = statesWithProbabilityGreater0E.swapVariables(model.getRowColumnMetaVariablePairs());
- statesWithProbabilityGreater0E = statesWithProbabilityGreater0E.andExists(abstractedTransitionMatrix, model.getColumnVariables());
- statesWithProbabilityGreater0E &= phiStates;
- statesWithProbabilityGreater0E |= lastIterationStates;
- ++iterations;
- }
-
- return statesWithProbabilityGreater0E;
- }
-
+ storm::dd::Bdd<Type> performProbGreater0E(storm::models::symbolic::NondeterministicModel<Type> const& model, storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates);
/*!
* Computes the set of states for which there does not exist a scheduler that achieves a probability greater
* than zero of satisfying phi until psi.
@@ -831,10 +369,7 @@ namespace storm {
* @return A BDD representing all such states.
*/
template <storm::dd::DdType Type>
- storm::dd::Bdd<Type> performProb0A(storm::models::symbolic::NondeterministicModel<Type> const& model, storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates) {
- return !performProbGreater0E(model, transitionMatrix, phiStates, psiStates) && model.getReachableStates();
- }
-
+ storm::dd::Bdd<Type> performProb0A(storm::models::symbolic::NondeterministicModel<Type> const& model, storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates) ;
/*!
* Computes the set of states for which all schedulers achieve a probability greater than zero of satisfying
* phi until psi.
@@ -846,27 +381,7 @@ namespace storm {
* @return A BDD representing all such states.
*/
template <storm::dd::DdType Type>
- storm::dd::Bdd<Type> performProbGreater0A(storm::models::symbolic::NondeterministicModel<Type> const& model, storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates) {
- // Initialize environment for backward search.
- storm::dd::DdManager<Type> const& manager = model.getManager();
- storm::dd::Bdd<Type> lastIterationStates = manager.getBddZero();
- storm::dd::Bdd<Type> statesWithProbabilityGreater0A = psiStates;
-
- uint_fast64_t iterations = 0;
- while (lastIterationStates != statesWithProbabilityGreater0A) {
- lastIterationStates = statesWithProbabilityGreater0A;
- statesWithProbabilityGreater0A = statesWithProbabilityGreater0A.swapVariables(model.getRowColumnMetaVariablePairs());
- statesWithProbabilityGreater0A = statesWithProbabilityGreater0A.andExists(transitionMatrix, model.getColumnVariables());
- statesWithProbabilityGreater0A |= model.getIllegalMask();
- statesWithProbabilityGreater0A = statesWithProbabilityGreater0A.universalAbstract(model.getNondeterminismVariables());
- statesWithProbabilityGreater0A &= phiStates;
- statesWithProbabilityGreater0A |= psiStates;
- ++iterations;
- }
-
- return statesWithProbabilityGreater0A;
- }
-
+ storm::dd::Bdd<Type> performProbGreater0A(storm::models::symbolic::NondeterministicModel<Type> const& model, storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates) ;
/*!
* Computes the set of states for which there exists a scheduler that achieves probability zero of satisfying
* phi until psi.
@@ -878,9 +393,7 @@ namespace storm {
* @return A BDD representing all such states.
*/
template <storm::dd::DdType Type>
- storm::dd::Bdd<Type> performProb0E(storm::models::symbolic::NondeterministicModel<Type> const& model, storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates) {
- return !performProbGreater0A(model, transitionMatrix, phiStates, psiStates) && model.getReachableStates();
- }
+ storm::dd::Bdd<Type> performProb0E(storm::models::symbolic::NondeterministicModel<Type> const& model, storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates) ;
/*!
* Computes the set of states for which all schedulers achieve probability one of satisfying phi until psi.
@@ -894,26 +407,7 @@ namespace storm {
* @return A BDD representing all such states.
*/
template <storm::dd::DdType Type>
- storm::dd::Bdd<Type> performProb1A(storm::models::symbolic::NondeterministicModel<Type> const& model, storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates, storm::dd::Bdd<Type> const& statesWithProbabilityGreater0A) {
- // Initialize environment for backward search.
- storm::dd::DdManager<Type> const& manager = model.getManager();
- storm::dd::Bdd<Type> lastIterationStates = manager.getBddZero();
- storm::dd::Bdd<Type> statesWithProbability1A = psiStates || statesWithProbabilityGreater0A;
-
- uint_fast64_t iterations = 0;
- while (lastIterationStates != statesWithProbability1A) {
- lastIterationStates = statesWithProbability1A;
- statesWithProbability1A = statesWithProbability1A.swapVariables(model.getRowColumnMetaVariablePairs());
- statesWithProbability1A = transitionMatrix.implies(statesWithProbability1A).universalAbstract(model.getColumnVariables());
- statesWithProbability1A |= model.getIllegalMask();
- statesWithProbability1A = statesWithProbability1A.universalAbstract(model.getNondeterminismVariables());
- statesWithProbability1A &= statesWithProbabilityGreater0A;
- statesWithProbability1A |= psiStates;
- ++iterations;
- }
-
- return statesWithProbability1A;
- }
+ storm::dd::Bdd<Type> performProb1A(storm::models::symbolic::NondeterministicModel<Type> const& model, storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates, storm::dd::Bdd<Type> const& statesWithProbabilityGreater0A);
/*!
* Computes the set of states for which there exists a scheduler that achieves probability one of satisfying
@@ -928,63 +422,13 @@ namespace storm {
* @return A BDD representing all such states.
*/
template <storm::dd::DdType Type>
- storm::dd::Bdd<Type> performProb1E(storm::models::symbolic::NondeterministicModel<Type> const& model, storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates, storm::dd::Bdd<Type> const& statesWithProbabilityGreater0E) {
- // Initialize environment for backward search.
- storm::dd::DdManager<Type> const& manager = model.getManager();
- storm::dd::Bdd<Type> statesWithProbability1E = statesWithProbabilityGreater0E;
-
- uint_fast64_t iterations = 0;
- bool outerLoopDone = false;
- while (!outerLoopDone) {
- storm::dd::Bdd<Type> innerStates = manager.getBddZero();
-
- bool innerLoopDone = false;
- while (!innerLoopDone) {
- storm::dd::Bdd<Type> temporary = statesWithProbability1E.swapVariables(model.getRowColumnMetaVariablePairs());
- temporary = transitionMatrix.implies(temporary).universalAbstract(model.getColumnVariables());
-
- storm::dd::Bdd<Type> temporary2 = innerStates.swapVariables(model.getRowColumnMetaVariablePairs());
- temporary2 = transitionMatrix.andExists(temporary2, model.getColumnVariables());
-
- temporary = temporary.andExists(temporary2, model.getNondeterminismVariables());
- temporary &= phiStates;
- temporary |= psiStates;
-
- if (innerStates == temporary) {
- innerLoopDone = true;
- } else {
- innerStates = temporary;
- }
- }
-
- if (statesWithProbability1E == innerStates) {
- outerLoopDone = true;
- } else {
- statesWithProbability1E = innerStates;
- }
- ++iterations;
- }
-
- return statesWithProbability1E;
- }
+ storm::dd::Bdd<Type> performProb1E(storm::models::symbolic::NondeterministicModel<Type> const& model, storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates, storm::dd::Bdd<Type> const& statesWithProbabilityGreater0E) ;
template <storm::dd::DdType Type>
- std::pair<storm::dd::Bdd<Type>, storm::dd::Bdd<Type>> performProb01Max(storm::models::symbolic::NondeterministicModel<Type> const& model, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates) {
- std::pair<storm::dd::Bdd<Type>, storm::dd::Bdd<Type>> result;
- storm::dd::Bdd<Type> transitionMatrix = model.getTransitionMatrix().notZero();
- result.first = performProb0A(model, transitionMatrix, phiStates, psiStates);
- result.second = performProb1E(model, transitionMatrix, phiStates, psiStates, !result.first && model.getReachableStates());
- return result;
- }
+ std::pair<storm::dd::Bdd<Type>, storm::dd::Bdd<Type>> performProb01Max(storm::models::symbolic::NondeterministicModel<Type> const& model, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates) ;
template <storm::dd::DdType Type>
- std::pair<storm::dd::Bdd<Type>, storm::dd::Bdd<Type>> performProb01Min(storm::models::symbolic::NondeterministicModel<Type> const& model, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates) {
- std::pair<storm::dd::Bdd<Type>, storm::dd::Bdd<Type>> result;
- storm::dd::Bdd<Type> transitionMatrix = model.getTransitionMatrix().notZero();
- result.first = performProb0E(model, transitionMatrix, phiStates, psiStates);
- result.second = performProb1A(model, transitionMatrix, phiStates, psiStates, !result.first && model.getReachableStates());
- return result;
- }
+ std::pair<storm::dd::Bdd<Type>, storm::dd::Bdd<Type>> performProb01Min(storm::models::symbolic::NondeterministicModel<Type> const& model, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates) ;
/*!
* Performs a topological sort of the states of the system according to the given transitions.
@@ -993,73 +437,7 @@ namespace storm {
* @return A vector of indices that is a topological sort of the states.
*/
template <typename T>
- std::vector<uint_fast64_t> getTopologicalSort(storm::storage::SparseMatrix<T> const& matrix) {
- if (matrix.getRowCount() != matrix.getColumnCount()) {
- LOG4CPLUS_ERROR(logger, "Provided matrix is required to be square.");
- throw storm::exceptions::InvalidArgumentException() << "Provided matrix is required to be square.";
- }
-
- uint_fast64_t numberOfStates = matrix.getRowCount();
-
- // Prepare the result. This relies on the matrix being square.
- std::vector<uint_fast64_t> topologicalSort;
- topologicalSort.reserve(numberOfStates);
-
- // Prepare the stacks needed for recursion.
- std::vector<uint_fast64_t> recursionStack;
- recursionStack.reserve(matrix.getRowCount());
- std::vector<typename storm::storage::SparseMatrix<T>::const_iterator> iteratorRecursionStack;
- iteratorRecursionStack.reserve(numberOfStates);
-
- // Perform a depth-first search over the given transitions and record states in the reverse order they were visited.
- storm::storage::BitVector visitedStates(numberOfStates);
- for (uint_fast64_t state = 0; state < numberOfStates; ++state) {
- if (!visitedStates.get(state)) {
- recursionStack.push_back(state);
- iteratorRecursionStack.push_back(matrix.begin(state));
-
- recursionStepForward:
- while (!recursionStack.empty()) {
- uint_fast64_t currentState = recursionStack.back();
- typename storm::storage::SparseMatrix<T>::const_iterator successorIterator = iteratorRecursionStack.back();
-
- visitedStates.set(currentState, true);
-
- recursionStepBackward:
- for (; successorIterator != matrix.end(currentState); ++successorIterator) {
- if (!visitedStates.get(successorIterator->getColumn())) {
- // Put unvisited successor on top of our recursion stack and remember that.
- recursionStack.push_back(successorIterator->getColumn());
-
- // Also, put initial value for iterator on corresponding recursion stack.
- iteratorRecursionStack.push_back(matrix.begin(successorIterator->getColumn()));
-
- goto recursionStepForward;
- }
- }
-
- topologicalSort.push_back(currentState);
-
- // If we reach this point, we have completed the recursive descent for the current state.
- // That is, we need to pop it from the recursion stacks.
- recursionStack.pop_back();
- iteratorRecursionStack.pop_back();
-
- // If there is at least one state under the current one in our recursion stack, we need
- // to restore the topmost state as the current state and jump to the part after the
- // original recursive call.
- if (recursionStack.size() > 0) {
- currentState = recursionStack.back();
- successorIterator = iteratorRecursionStack.back();
-
- goto recursionStepBackward;
- }
- }
- }
- }
-
- return topologicalSort;
- }
+ std::vector<uint_fast64_t> getTopologicalSort(storm::storage::SparseMatrix<T> const& matrix) ;
/*!
* A class needed to compare the distances for two states in the Dijkstra search.
@@ -1084,59 +462,7 @@ namespace storm {
std::pair<std::vector<T>, std::vector<uint_fast64_t>> performDijkstra(storm::models::sparse::Model<T> const& model,
storm::storage::SparseMatrix<T> const& transitions,
storm::storage::BitVector const& startingStates,
- storm::storage::BitVector const* filterStates = nullptr) {
-
- LOG4CPLUS_INFO(logger, "Performing Dijkstra search.");
-
- const uint_fast64_t noPredecessorValue = storm::utility::zero<uint_fast64_t>();
- std::vector<T> probabilities(model.getNumberOfStates(), storm::utility::zero<T>());
- std::vector<uint_fast64_t> predecessors(model.getNumberOfStates(), noPredecessorValue);
-
- // Set the probability to 1 for all starting states.
- std::set<std::pair<T, uint_fast64_t>, DistanceCompare<T>> probabilityStateSet;
-
- for (auto state : startingStates) {
- probabilityStateSet.emplace(storm::utility::one<T>(), state);
- probabilities[state] = storm::utility::one<T>();
- }
-
- // As long as there is one reachable state, we need to consider it.
- while (!probabilityStateSet.empty()) {
- // Get the state with the least distance from the set and remove it.
- std::pair<T, uint_fast64_t> probabilityStatePair = *probabilityStateSet.begin();
- probabilityStateSet.erase(probabilityStateSet.begin());
-
- // Now check the new distances for all successors of the current state.
- typename storm::storage::SparseMatrix<T>::Rows row = transitions.getRow(probabilityStatePair.second);
- for (auto const& transition : row) {
- // Only follow the transition if it lies within the filtered states.
- if (filterStates != nullptr && filterStates->get(transition.first)) {
- // Calculate the distance we achieve when we take the path to the successor via the current state.
- T newDistance = probabilityStatePair.first * transition.second;
-
- // We found a cheaper way to get to the target state of the transition.
- if (newDistance > probabilities[transition.first]) {
- // Remove the old distance.
- if (probabilities[transition.first] != noPredecessorValue) {
- probabilityStateSet.erase(std::make_pair(probabilities[transition.first], transition.first));
- }
-
- // Set and add the new distance.
- probabilities[transition.first] = newDistance;
- predecessors[transition.first] = probabilityStatePair.second;
- probabilityStateSet.insert(std::make_pair(newDistance, transition.first));
- }
- }
- }
- }
-
- // Move the values into the result and return it.
- std::pair<std::vector<T>, std::vector<uint_fast64_t>> result;
- result.first = std::move(probabilities);
- result.second = std::move(predecessors);
- LOG4CPLUS_INFO(logger, "Done performing Dijkstra search.");
- return result;
- }
+ storm::storage::BitVector const* filterStates = nullptr);
} // namespace graph
} // namespace utility