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 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 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 + storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix 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 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() && !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 + std::vector getDistances(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates) { + std::vector distances(transitionMatrix.getRowGroupCount()); + + std::vector> 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 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 + storm::storage::BitVector performProbGreater0(storm::storage::SparseMatrix 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 stack(psiStates.begin(), psiStates.end()); + + // Initialize the stack for the step bound, if the number of steps is bounded. + std::vector stepStack; + std::vector 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::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 + storm::storage::BitVector performProb1(storm::storage::SparseMatrix 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 + storm::storage::BitVector performProb1(storm::storage::SparseMatrix 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 + std::pair performProb01(storm::models::sparse::DeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + std::pair result; + storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); + result.first = performProbGreater0(backwardTransitions, phiStates, psiStates); + result.second = performProb1(backwardTransitions, phiStates, psiStates, result.first); + result.first.complement(); + return result; + } + + template + std::pair performProb01(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + std::pair result; + result.first = performProbGreater0(backwardTransitions, phiStates, psiStates); + result.second = performProb1(backwardTransitions, phiStates, psiStates, result.first); + result.first.complement(); + return result; + } + + template + storm::dd::Bdd performProbGreater0(storm::models::symbolic::Model const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, boost::optional const& stepBound) { + // Initialize environment for backward search. + storm::dd::DdManager const& manager = model.getManager(); + storm::dd::Bdd lastIterationStates = manager.getBddZero(); + storm::dd::Bdd 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::Bdd performProb1(storm::models::symbolic::Model const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0) { + storm::dd::Bdd statesWithProbability1 = performProbGreater0(model, transitionMatrix, !psiStates && model.getReachableStates(), !statesWithProbabilityGreater0 && model.getReachableStates()); + statesWithProbability1 = !statesWithProbability1 && model.getReachableStates(); + return statesWithProbability1; + } + + template + storm::dd::Bdd performProb1(storm::models::symbolic::Model const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { + storm::dd::Bdd statesWithProbabilityGreater0 = performProbGreater0(model, transitionMatrix, phiStates, psiStates); + return performProb1(model, transitionMatrix, phiStates, psiStates, statesWithProbabilityGreater0); + } + + template + std::pair, storm::dd::Bdd> performProb01(storm::models::symbolic::DeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { + std::pair, storm::dd::Bdd> result; + storm::dd::Bdd 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 + std::pair, storm::dd::Bdd> performProb01(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { + std::pair, storm::dd::Bdd> result; + storm::dd::Bdd 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 + storm::storage::BitVector performProbGreater0E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix 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 stack(psiStates.begin(), psiStates.end()); + + // Initialize the stack for the step bound, if the number of steps is bounded. + std::vector stepStack; + std::vector 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::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 + storm::storage::BitVector performProb0A(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix 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 + storm::storage::BitVector performProb0A(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + return performProb0A(model.getTransitionMatrix(), model.getNondeterministicChoiceIndices(), backwardTransitions, phiStates, psiStates); + } + + template + storm::storage::BitVector performProb1E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix 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 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::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::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 + storm::storage::BitVector performProb1E(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + return performProb1E(model.getTransitionMatrix(), model.getNondeterministicChoiceIndices(), backwardTransitions, phiStates, psiStates); + } + + template + std::pair performProb01Max(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + std::pair result; + + result.first = performProb0A(transitionMatrix, nondeterministicChoiceIndices, backwardTransitions, phiStates, psiStates); + result.second = performProb1E(transitionMatrix, nondeterministicChoiceIndices, backwardTransitions, phiStates, psiStates); + return result; + } + + template + std::pair performProb01Max(storm::models::sparse::NondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + return performProb01Max(model.getTransitionMatrix(), model.getTransitionMatrix().getRowGroupIndices(), model.getBackwardTransitions(), phiStates, psiStates); + } + + template + storm::storage::BitVector performProbGreater0A(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix 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 stack(psiStates.begin(), psiStates.end()); + + // Initialize the stack for the step bound, if the number of steps is bounded. + std::vector stepStack; + std::vector 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::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::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 + storm::storage::BitVector performProb0E(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix 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 + storm::storage::BitVector performProb0E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix 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 + storm::storage::BitVector performProb1A( storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix 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 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::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::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 + std::pair performProb01Min(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + std::pair result; + result.first = performProb0E(transitionMatrix, nondeterministicChoiceIndices, backwardTransitions, phiStates, psiStates); + result.second = performProb1A(transitionMatrix, nondeterministicChoiceIndices, backwardTransitions, phiStates, psiStates); + return result; + } + + template + std::pair performProb01Min(storm::models::sparse::NondeterministicModel 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::Bdd performProbGreater0E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { + // Initialize environment for backward search. + storm::dd::DdManager const& manager = model.getManager(); + storm::dd::Bdd lastIterationStates = manager.getBddZero(); + storm::dd::Bdd statesWithProbabilityGreater0E = psiStates; + + uint_fast64_t iterations = 0; + storm::dd::Bdd 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::Bdd performProb0A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { + return !performProbGreater0E(model, transitionMatrix, phiStates, psiStates) && model.getReachableStates(); + } + + template + storm::dd::Bdd performProbGreater0A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { + // Initialize environment for backward search. + storm::dd::DdManager const& manager = model.getManager(); + storm::dd::Bdd lastIterationStates = manager.getBddZero(); + storm::dd::Bdd 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::Bdd performProb0E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { + return !performProbGreater0A(model, transitionMatrix, phiStates, psiStates) && model.getReachableStates(); + } + + template + storm::dd::Bdd performProb1A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0A) { + // Initialize environment for backward search. + storm::dd::DdManager const& manager = model.getManager(); + storm::dd::Bdd lastIterationStates = manager.getBddZero(); + storm::dd::Bdd 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::Bdd performProb1E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0E) { + // Initialize environment for backward search. + storm::dd::DdManager const& manager = model.getManager(); + storm::dd::Bdd statesWithProbability1E = statesWithProbabilityGreater0E; + + uint_fast64_t iterations = 0; + bool outerLoopDone = false; + while (!outerLoopDone) { + storm::dd::Bdd innerStates = manager.getBddZero(); + + bool innerLoopDone = false; + while (!innerLoopDone) { + storm::dd::Bdd temporary = statesWithProbability1E.swapVariables(model.getRowColumnMetaVariablePairs()); + temporary = transitionMatrix.implies(temporary).universalAbstract(model.getColumnVariables()); + + storm::dd::Bdd 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 + std::pair, storm::dd::Bdd> performProb01Max(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { + std::pair, storm::dd::Bdd> result; + storm::dd::Bdd 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 + std::pair, storm::dd::Bdd> performProb01Min(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { + std::pair, storm::dd::Bdd> result; + storm::dd::Bdd 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 + std::vector getTopologicalSort(storm::storage::SparseMatrix 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 topologicalSort; + topologicalSort.reserve(numberOfStates); + + // Prepare the stacks needed for recursion. + std::vector recursionStack; + recursionStack.reserve(matrix.getRowCount()); + std::vector::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::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 + std::pair, std::vector> performDijkstra(storm::models::sparse::Model const& model, + storm::storage::SparseMatrix 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(); + std::vector probabilities(model.getNumberOfStates(), storm::utility::zero()); + std::vector predecessors(model.getNumberOfStates(), noPredecessorValue); + + // Set the probability to 1 for all starting states. + std::set, DistanceCompare> probabilityStateSet; + + for (auto state : startingStates) { + probabilityStateSet.emplace(storm::utility::one(), state); + probabilities[state] = storm::utility::one(); + } + + // 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 probabilityStatePair = probabilityStateSet.erase(probabilityStateSet.begin()); + + // Now check the new distances for all successors of the current state. + typename storm::storage::SparseMatrix::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> 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 const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates); + + template std::vector getDistances(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates); + + + template storm::storage::BitVector performProbGreater0(storm::storage::SparseMatrix 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 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 const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + + + template std::pair performProb01(storm::models::sparse::DeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + + + template std::pair performProb01(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + + + + template storm::storage::BitVector performProbGreater0E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix 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 const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + + template storm::storage::BitVector performProb0A(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; + + template storm::storage::BitVector performProb1E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + + + template storm::storage::BitVector performProb1E(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + + template std::pair performProb01Max(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; + + + template std::pair performProb01Max(storm::models::sparse::NondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; + + template storm::storage::BitVector performProbGreater0A(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix 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 const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + template storm::storage::BitVector performProb0E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; + + + template storm::storage::BitVector performProb1A( storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + + template std::pair performProb01Min(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; + + + template std::pair performProb01Min(storm::models::sparse::NondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + + + template std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix) ; + + + + template storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates); + + template std::vector getDistances(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates); + + + template storm::storage::BitVector performProbGreater0(storm::storage::SparseMatrix 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 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 const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + + + template std::pair performProb01(storm::models::sparse::DeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + + + template std::pair performProb01(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + + + + template storm::storage::BitVector performProbGreater0E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix 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 const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + + template storm::storage::BitVector performProb0A(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; + + template storm::storage::BitVector performProb1E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + + + template storm::storage::BitVector performProb1E(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + + template std::pair performProb01Max(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; + + + template std::pair performProb01Max(storm::models::sparse::NondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; + + template storm::storage::BitVector performProbGreater0A(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix 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 const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + template storm::storage::BitVector performProb0E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; + + + template storm::storage::BitVector performProb1A( storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + + template std::pair performProb01Min(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; + + + template std::pair performProb01Min(storm::models::sparse::NondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + + + template std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix) ; + +#ifdef STORM_HAVE_CARL + + + template storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates); + + template std::vector getDistances(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates); + + + template storm::storage::BitVector performProbGreater0(storm::storage::SparseMatrix 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 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 const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + + + template std::pair performProb01(storm::models::sparse::DeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + + + template std::pair performProb01(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + + + + template storm::storage::BitVector performProbGreater0E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix 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 const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + + template storm::storage::BitVector performProb0A(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; + + template storm::storage::BitVector performProb1E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + + + template storm::storage::BitVector performProb1E(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + + template std::pair performProb01Max(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; + + + template std::pair performProb01Max(storm::models::sparse::NondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; + + template storm::storage::BitVector performProbGreater0A(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix 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 const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + template storm::storage::BitVector performProb0E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; + + + template storm::storage::BitVector performProb1A( storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + + template std::pair performProb01Min(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; + + + template std::pair performProb01Min(storm::models::sparse::NondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + + + template std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix) ; + +#endif + + + template storm::dd::Bdd performProbGreater0(storm::models::symbolic::Model const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, boost::optional const& stepBound = boost::optional()); + + template storm::dd::Bdd performProb1(storm::models::symbolic::Model const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0); + + + template storm::dd::Bdd performProb1(storm::models::symbolic::Model const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) ; + + + template std::pair, storm::dd::Bdd> performProb01(storm::models::symbolic::DeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); + + + template std::pair, storm::dd::Bdd> performProb01(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); + + + template storm::dd::Bdd performProbGreater0E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); + + template storm::dd::Bdd performProb0A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) ; + + template storm::dd::Bdd performProbGreater0A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) ; + + template storm::dd::Bdd performProb0E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) ; + + + template storm::dd::Bdd performProb1A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0A); + + + template storm::dd::Bdd performProb1E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0E) ; + + + template std::pair, storm::dd::Bdd> performProb01Max(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) ; + + + template std::pair, storm::dd::Bdd> performProb01Min(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd 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 class SparseMatrix; + } + + namespace models { + + namespace symbolic { + template class Model; + template class DeterministicModel; + template class NondeterministicModel; + } + + } + + namespace dd { + template class Bdd; + template class Add; + + } + + namespace utility { namespace graph { @@ -34,38 +48,7 @@ namespace storm { * @param targetStates The target states that may not be passed. */ template - storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix 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 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() && !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 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 - std::vector getDistances(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates) { - std::vector distances(transitionMatrix.getRowGroupCount()); - - std::vector> 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 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 getDistances(storm::storage::SparseMatrix 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 - storm::storage::BitVector performProbGreater0(storm::storage::SparseMatrix 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 stack(psiStates.begin(), psiStates.end()); - - // Initialize the stack for the step bound, if the number of steps is bounded. - std::vector stepStack; - std::vector 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::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 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 - storm::storage::BitVector performProb1(storm::storage::SparseMatrix 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 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 - storm::storage::BitVector performProb1(storm::storage::SparseMatrix 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 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 - static std::pair performProb01(storm::models::sparse::DeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { - std::pair result; - storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); - result.first = performProbGreater0(backwardTransitions, phiStates, psiStates); - result.second = performProb1(backwardTransitions, phiStates, psiStates, result.first); - result.first.complement(); - return result; - } + std::pair performProb01(storm::models::sparse::DeterministicModel 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 - static std::pair performProb01(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { - std::pair result; - result.first = performProbGreater0(backwardTransitions, phiStates, psiStates); - result.second = performProb1(backwardTransitions, phiStates, psiStates, result.first); - result.first.complement(); - return result; - } + std::pair performProb01(storm::storage::SparseMatrix 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::Bdd performProbGreater0(storm::models::symbolic::Model const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, boost::optional const& stepBound = boost::optional()) { - // Initialize environment for backward search. - storm::dd::DdManager const& manager = model.getManager(); - storm::dd::Bdd lastIterationStates = manager.getBddZero(); - storm::dd::Bdd 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 performProbGreater0(storm::models::symbolic::Model const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, boost::optional const& stepBound = boost::optional()); /*! * 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::Bdd performProb1(storm::models::symbolic::Model const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0) { - storm::dd::Bdd statesWithProbability1 = performProbGreater0(model, transitionMatrix, !psiStates && model.getReachableStates(), !statesWithProbabilityGreater0 && model.getReachableStates()); - statesWithProbability1 = !statesWithProbability1 && model.getReachableStates(); - return statesWithProbability1; - } + storm::dd::Bdd performProb1(storm::models::symbolic::Model const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd 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::Bdd performProb1(storm::models::symbolic::Model const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { - storm::dd::Bdd statesWithProbabilityGreater0 = performProbGreater0(model, transitionMatrix, phiStates, psiStates); - return performProb1(model, transitionMatrix, phiStates, psiStates, statesWithProbabilityGreater0); - } + storm::dd::Bdd performProb1(storm::models::symbolic::Model const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd 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 - static std::pair, storm::dd::Bdd> performProb01(storm::models::symbolic::DeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { - std::pair, storm::dd::Bdd> result; - storm::dd::Bdd 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> performProb01(storm::models::symbolic::DeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd 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 - static std::pair, storm::dd::Bdd> performProb01(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { - std::pair, storm::dd::Bdd> result; - storm::dd::Bdd 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> performProb01(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd 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 - storm::storage::BitVector performProbGreater0E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix 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 stack(psiStates.begin(), psiStates.end()); - - // Initialize the stack for the step bound, if the number of steps is bounded. - std::vector stepStack; - std::vector 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::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 const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix 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 const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix 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 const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix 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 - storm::storage::BitVector performProb0A(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix 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 const& model, storm::storage::SparseMatrix 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 - storm::storage::BitVector performProb1E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix 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 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::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::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 const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix 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 - storm::storage::BitVector performProb1E(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix 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 const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); template - std::pair performProb01Max(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { - std::pair result; - - result.first = performProb0A(transitionMatrix, nondeterministicChoiceIndices, backwardTransitions, phiStates, psiStates); - result.second = performProb1E(transitionMatrix, nondeterministicChoiceIndices, backwardTransitions, phiStates, psiStates); - return result; - } + std::pair performProb01Max(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix 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 - std::pair performProb01Max(storm::models::sparse::NondeterministicModel 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 performProb01Max(storm::models::sparse::NondeterministicModel 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 - storm::storage::BitVector performProbGreater0A(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix 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 stack(psiStates.begin(), psiStates.end()); - - // Initialize the stack for the step bound, if the number of steps is bounded. - std::vector stepStack; - std::vector 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::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::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 const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix 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 - storm::storage::BitVector performProb0E(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix 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 const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); template - storm::storage::BitVector performProb0E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix 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 const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix 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 - storm::storage::BitVector performProb1A( storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix 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 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::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::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 const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); template - std::pair performProb01Min(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { - std::pair result; - result.first = performProb0E(transitionMatrix, nondeterministicChoiceIndices, backwardTransitions, phiStates, psiStates); - result.second = performProb1A(transitionMatrix, nondeterministicChoiceIndices, backwardTransitions, phiStates, psiStates); - return result; - } + std::pair performProb01Min(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix 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 - std::pair performProb01Min(storm::models::sparse::NondeterministicModel 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 performProb01Min(storm::models::sparse::NondeterministicModel 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::Bdd performProbGreater0E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { - // Initialize environment for backward search. - storm::dd::DdManager const& manager = model.getManager(); - storm::dd::Bdd lastIterationStates = manager.getBddZero(); - storm::dd::Bdd statesWithProbabilityGreater0E = psiStates; - - uint_fast64_t iterations = 0; - storm::dd::Bdd 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 performProbGreater0E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd 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::Bdd performProb0A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { - return !performProbGreater0E(model, transitionMatrix, phiStates, psiStates) && model.getReachableStates(); - } - + storm::dd::Bdd performProb0A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd 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::Bdd performProbGreater0A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { - // Initialize environment for backward search. - storm::dd::DdManager const& manager = model.getManager(); - storm::dd::Bdd lastIterationStates = manager.getBddZero(); - storm::dd::Bdd 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 performProbGreater0A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd 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::Bdd performProb0E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { - return !performProbGreater0A(model, transitionMatrix, phiStates, psiStates) && model.getReachableStates(); - } + storm::dd::Bdd performProb0E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd 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::Bdd performProb1A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0A) { - // Initialize environment for backward search. - storm::dd::DdManager const& manager = model.getManager(); - storm::dd::Bdd lastIterationStates = manager.getBddZero(); - storm::dd::Bdd 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 performProb1A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd 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::Bdd performProb1E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0E) { - // Initialize environment for backward search. - storm::dd::DdManager const& manager = model.getManager(); - storm::dd::Bdd statesWithProbability1E = statesWithProbabilityGreater0E; - - uint_fast64_t iterations = 0; - bool outerLoopDone = false; - while (!outerLoopDone) { - storm::dd::Bdd innerStates = manager.getBddZero(); - - bool innerLoopDone = false; - while (!innerLoopDone) { - storm::dd::Bdd temporary = statesWithProbability1E.swapVariables(model.getRowColumnMetaVariablePairs()); - temporary = transitionMatrix.implies(temporary).universalAbstract(model.getColumnVariables()); - - storm::dd::Bdd 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 performProb1E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0E) ; template - std::pair, storm::dd::Bdd> performProb01Max(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { - std::pair, storm::dd::Bdd> result; - storm::dd::Bdd 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> performProb01Max(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) ; template - std::pair, storm::dd::Bdd> performProb01Min(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { - std::pair, storm::dd::Bdd> result; - storm::dd::Bdd 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> performProb01Min(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd 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 - std::vector getTopologicalSort(storm::storage::SparseMatrix 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 topologicalSort; - topologicalSort.reserve(numberOfStates); - - // Prepare the stacks needed for recursion. - std::vector recursionStack; - recursionStack.reserve(matrix.getRowCount()); - std::vector::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::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 getTopologicalSort(storm::storage::SparseMatrix 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> performDijkstra(storm::models::sparse::Model const& model, storm::storage::SparseMatrix 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(); - std::vector probabilities(model.getNumberOfStates(), storm::utility::zero()); - std::vector predecessors(model.getNumberOfStates(), noPredecessorValue); - - // Set the probability to 1 for all starting states. - std::set, DistanceCompare> probabilityStateSet; - - for (auto state : startingStates) { - probabilityStateSet.emplace(storm::utility::one(), state); - probabilities[state] = storm::utility::one(); - } - - // 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 probabilityStatePair = *probabilityStateSet.begin(); - probabilityStateSet.erase(probabilityStateSet.begin()); - - // Now check the new distances for all successors of the current state. - typename storm::storage::SparseMatrix::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> 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