diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h index b5a474129..eda3ddb63 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h @@ -713,11 +713,11 @@ namespace storm { std::vector scheduler(maybeStates.getNumberOfSetBits()); // For each of the states we need to resolve the nondeterministic choice based on the information we are given. - Type maxProbability = 0; + Type maxProbability = -storm::utility::constGetInfinity(); Type currentProbability = 0; uint_fast64_t currentStateIndex = 0; for (auto state : maybeStates) { - maxProbability = 0; + maxProbability = -storm::utility::constGetInfinity(); for (uint_fast64_t row = 0, rowEnd = this->getModel().getNondeterministicChoiceIndices()[state + 1] - this->getModel().getNondeterministicChoiceIndices()[state]; row < rowEnd; ++row) { typename storm::storage::SparseMatrix::Rows currentRow = this->getModel().getTransitionMatrix().getRow(this->getModel().getNondeterministicChoiceIndices()[state] + row); @@ -725,9 +725,10 @@ namespace storm { for (auto& transition : currentRow) { currentProbability += transition.value() * distancesToTarget[transition.column()]; + // currentProbability -= transition.value() * (1 - distancesToNonTarget[transition.column()]); } - if (currentProbability < maxProbability) { + if (currentProbability > maxProbability) { maxProbability = currentProbability; scheduler[currentStateIndex] = row; } diff --git a/src/utility/graph.h b/src/utility/graph.h index 6f5ab401f..7cad73496 100644 --- a/src/utility/graph.h +++ b/src/utility/graph.h @@ -22,825 +22,821 @@ extern log4cplus::Logger logger; namespace storm { - -namespace utility { - -namespace graph { - - /*! - * Performs a backwards breadt-first search trough the underlying graph structure - * of the given model to determine which states of the model have a positive probability - * of satisfying phi until psi. The resulting states are written to the given bit vector. - * - * @param model The model whose graph structure to search. - * @param phiStates A bit vector of all states satisfying phi. - * @param psiStates A bit vector of all states satisfying psi. - * @param useStepBound A flag that indicates whether or not to use the given number of maximal steps for the search. - * @param maximalSteps The maximal number of steps to reach the psi states. - * @return A bit vector with all indices of states that have a probability greater than 0. - */ - template - storm::storage::BitVector performProbGreater0(storm::models::AbstractDeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) { - // Prepare the resulting bit vector. - storm::storage::BitVector statesWithProbabilityGreater0(model.getNumberOfStates()); - - // Get the backwards transition relation from the model to ease the search. - storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); - - // 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.getSetIndicesList(); - - // Initialize the stack for the step bound, if the number of steps is bounded. - std::vector stepStack; - std::vector remainingSteps; - if (useStepBound) { - stepStack.reserve(model.getNumberOfStates()); - stepStack.insert(stepStack.begin(), psiStates.getNumberOfSetBits(), maximalSteps); - remainingSteps.resize(model.getNumberOfStates()); - for (auto state : psiStates) { - remainingSteps[state] = maximalSteps; + namespace utility { + namespace graph { + + /*! + * Performs a backwards breadt-first search trough the underlying graph structure + * of the given model to determine which states of the model have a positive probability + * of satisfying phi until psi. The resulting states are written to the given bit vector. + * + * @param model The model whose graph structure to search. + * @param phiStates A bit vector of all states satisfying phi. + * @param psiStates A bit vector of all states satisfying psi. + * @param useStepBound A flag that indicates whether or not to use the given number of maximal steps for the search. + * @param maximalSteps The maximal number of steps to reach the psi states. + * @return A bit vector with all indices of states that have a probability greater than 0. + */ + template + storm::storage::BitVector performProbGreater0(storm::models::AbstractDeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) { + // Prepare the resulting bit vector. + storm::storage::BitVector statesWithProbabilityGreater0(model.getNumberOfStates()); + + // Get the backwards transition relation from the model to ease the search. + storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); + + // 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.getSetIndicesList(); + + // Initialize the stack for the step bound, if the number of steps is bounded. + std::vector stepStack; + std::vector remainingSteps; + if (useStepBound) { + stepStack.reserve(model.getNumberOfStates()); + stepStack.insert(stepStack.begin(), psiStates.getNumberOfSetBits(), maximalSteps); + remainingSteps.resize(model.getNumberOfStates()); + 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 (auto predecessorIt = backwardTransitions.constColumnIteratorBegin(currentState), predecessorIte = backwardTransitions.constColumnIteratorEnd(currentState); predecessorIt != predecessorIte; ++predecessorIt) { + if (phiStates.get(*predecessorIt) && (!statesWithProbabilityGreater0.get(*predecessorIt) || (useStepBound && remainingSteps[*predecessorIt] < 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(*predecessorIt, true); + stack.push_back(*predecessorIt); + } 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[*predecessorIt] = currentStepBound - 1; + statesWithProbabilityGreater0.set(*predecessorIt, true); + stack.push_back(*predecessorIt); + stepStack.push_back(currentStepBound - 1); + } + } + } + } + + // Return result. + return statesWithProbabilityGreater0; } - } - - // 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(); + /*! + * 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 + * before. In order to do this, it uses the given set of states that + * characterizes the states that possess at least one path to a target state. + * The results are written to the given bit vector. + * + * @param model The model whose graph structure to search. + * @param phiStates A bit vector of all states satisfying phi. + * @param psiStates A bit vector of all states satisfying psi. + * @param statesWithProbabilityGreater0 A reference to a bit vector of states that possess a positive + * probability mass of satisfying phi until psi. + * @return A bit vector with all indices of states that have a probability greater than 1. + */ + template + storm::storage::BitVector performProb1(storm::models::AbstractDeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector const& statesWithProbabilityGreater0) { + storm::storage::BitVector statesWithProbability1 = performProbGreater0(model, ~psiStates, ~statesWithProbabilityGreater0); + statesWithProbability1.complement(); + return statesWithProbability1; } - - for (auto predecessorIt = backwardTransitions.constColumnIteratorBegin(currentState), predecessorIte = backwardTransitions.constColumnIteratorEnd(currentState); predecessorIt != predecessorIte; ++predecessorIt) { - if (phiStates.get(*predecessorIt) && (!statesWithProbabilityGreater0.get(*predecessorIt) || (useStepBound && remainingSteps[*predecessorIt] < 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(*predecessorIt, true); - stack.push_back(*predecessorIt); - } 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[*predecessorIt] = currentStepBound - 1; - statesWithProbabilityGreater0.set(*predecessorIt, true); - stack.push_back(*predecessorIt); - stepStack.push_back(currentStepBound - 1); + + /*! + * 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 + * before. In order to do this, it uses the given set of states that + * characterizes the states that possess at least one path to a target state. + * The results are written to the given bit vector. + * + * @param model The model whose graph structure to search. + * @param phiStates A bit vector of all states satisfying phi. + * @param psiStates A bit vector of all states satisfying psi. + * @return A bit vector with all indices of states that have a probability greater than 1. + */ + template + storm::storage::BitVector performProb1(storm::models::AbstractDeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + storm::storage::BitVector statesWithProbabilityGreater0 = performProbGreater0(model, phiStates, psiStates); + storm::storage::BitVector statesWithProbability1 = performProbGreater0(model, ~psiStates, ~(statesWithProbabilityGreater0)); + statesWithProbability1.complement(); + return statesWithProbability1; + } + + /*! + * Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi until psi in a + * deterministic model. + * + * @param model The model whose graph structure to search. + * @param phiStates The set of all states satisfying phi. + * @param psiStates The set of all states satisfying psi. + * @return A pair of bit vectors such that the first bit vector stores the indices of all states + * with probability 0 and the second stores all indices of states with probability 1. + */ + template + static std::pair performProb01(storm::models::AbstractDeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + std::pair result; + result.first = performProbGreater0(model, phiStates, psiStates); + result.second = performProb1(model, phiStates, psiStates, result.first); + result.first.complement(); + return result; + } + + /*! + * Computes the sets of states that have probability greater 0 of satisfying phi until psi under at least + * one possible resolution of non-determinism in a non-deterministic model. Stated differently, + * this means that these states have a probability greater 0 of satisfying phi until psi if the + * scheduler tries to minimize this probability. + * + * @param model The model whose graph structure to search. + * @param backwardTransitions The reversed transition relation of the model. + * @param phiStates The set of all states satisfying phi. + * @param psiStates The set of all states satisfying psi. + * @param useStepBound A flag that indicates whether or not to use the given number of maximal steps for the search. + * @param maximalSteps The maximal number of steps to reach the psi states. + * @return A bit vector that represents all states with probability 0. + */ + template + storm::storage::BitVector performProbGreater0E(storm::models::AbstractNondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) { + // Prepare resulting bit vector. + storm::storage::BitVector statesWithProbabilityGreater0(model.getNumberOfStates()); + + // 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.getSetIndicesList(); + + // Initialize the stack for the step bound, if the number of steps is bounded. + std::vector stepStack; + std::vector remainingSteps; + if (useStepBound) { + stepStack.reserve(model.getNumberOfStates()); + stepStack.insert(stepStack.begin(), psiStates.getNumberOfSetBits(), maximalSteps); + remainingSteps.resize(model.getNumberOfStates()); + for (auto state : psiStates) { + remainingSteps[state] = maximalSteps; } - } - } - } - - // Return result. - return statesWithProbabilityGreater0; - } - - /*! - * 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 - * before. In order to do this, it uses the given set of states that - * characterizes the states that possess at least one path to a target state. - * The results are written to the given bit vector. - * - * @param model The model whose graph structure to search. - * @param phiStates A bit vector of all states satisfying phi. - * @param psiStates A bit vector of all states satisfying psi. - * @param statesWithProbabilityGreater0 A reference to a bit vector of states that possess a positive - * probability mass of satisfying phi until psi. - * @return A bit vector with all indices of states that have a probability greater than 1. - */ - template - storm::storage::BitVector performProb1(storm::models::AbstractDeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector const& statesWithProbabilityGreater0) { - storm::storage::BitVector statesWithProbability1 = performProbGreater0(model, ~psiStates, ~statesWithProbabilityGreater0); - statesWithProbability1.complement(); - return statesWithProbability1; - } - - /*! - * 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 - * before. In order to do this, it uses the given set of states that - * characterizes the states that possess at least one path to a target state. - * The results are written to the given bit vector. - * - * @param model The model whose graph structure to search. - * @param phiStates A bit vector of all states satisfying phi. - * @param psiStates A bit vector of all states satisfying psi. - * @return A bit vector with all indices of states that have a probability greater than 1. - */ - template - storm::storage::BitVector performProb1(storm::models::AbstractDeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { - storm::storage::BitVector statesWithProbabilityGreater0 = performProbGreater0(model, phiStates, psiStates); - storm::storage::BitVector statesWithProbability1 = performProbGreater0(model, ~psiStates, ~(statesWithProbabilityGreater0)); - statesWithProbability1.complement(); - return statesWithProbability1; - } - - /*! - * Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi until psi in a - * deterministic model. - * - * @param model The model whose graph structure to search. - * @param phiStates The set of all states satisfying phi. - * @param psiStates The set of all states satisfying psi. - * @return A pair of bit vectors such that the first bit vector stores the indices of all states - * with probability 0 and the second stores all indices of states with probability 1. - */ - template - static std::pair performProb01(storm::models::AbstractDeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { - std::pair result; - result.first = performProbGreater0(model, phiStates, psiStates); - result.second = performProb1(model, phiStates, psiStates, result.first); - result.first.complement(); - return result; - } - - /*! - * Computes the sets of states that have probability greater 0 of satisfying phi until psi under at least - * one possible resolution of non-determinism in a non-deterministic model. Stated differently, - * this means that these states have a probability greater 0 of satisfying phi until psi if the - * scheduler tries to minimize this probability. - * - * @param model The model whose graph structure to search. - * @param backwardTransitions The reversed transition relation of the model. - * @param phiStates The set of all states satisfying phi. - * @param psiStates The set of all states satisfying psi. - * @param useStepBound A flag that indicates whether or not to use the given number of maximal steps for the search. - * @param maximalSteps The maximal number of steps to reach the psi states. - * @return A bit vector that represents all states with probability 0. - */ - template - storm::storage::BitVector performProbGreater0E(storm::models::AbstractNondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) { - // Prepare resulting bit vector. - storm::storage::BitVector statesWithProbabilityGreater0(model.getNumberOfStates()); - - // 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.getSetIndicesList(); - - // Initialize the stack for the step bound, if the number of steps is bounded. - std::vector stepStack; - std::vector remainingSteps; - if (useStepBound) { - stepStack.reserve(model.getNumberOfStates()); - stepStack.insert(stepStack.begin(), psiStates.getNumberOfSetBits(), maximalSteps); - remainingSteps.resize(model.getNumberOfStates()); - 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 (auto predecessorIt = backwardTransitions.constColumnIteratorBegin(currentState), predecessorIte = backwardTransitions.constColumnIteratorEnd(currentState); predecessorIt != predecessorIte; ++predecessorIt) { + if (phiStates.get(*predecessorIt) && (!statesWithProbabilityGreater0.get(*predecessorIt) || (useStepBound && remainingSteps[*predecessorIt] < 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(*predecessorIt, true); + stack.push_back(*predecessorIt); + } 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[*predecessorIt] = currentStepBound - 1; + statesWithProbabilityGreater0.set(*predecessorIt, true); + stack.push_back(*predecessorIt); + stepStack.push_back(currentStepBound - 1); + } + } + } + } + + return statesWithProbabilityGreater0; } - } - - // 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(); + /*! + * Computes the sets of states that have probability 0 of satisfying phi until psi under all + * possible resolutions of non-determinism in a non-deterministic model. Stated differently, + * this means that these states have probability 0 of satisfying phi until psi even if the + * scheduler tries to maximize this probability. + * + * @param model The model whose graph structure to search. + * @param backwardTransitions The reversed transition relation of the model. + * @param phiStates The set of all states satisfying phi. + * @param psiStates The set of all states satisfying psi. + * @param useStepBound A flag that indicates whether or not to use the given number of maximal steps for the search. + * @param maximalSteps The maximal number of steps to reach the psi states. + * @return A bit vector that represents all states with probability 0. + */ + template + storm::storage::BitVector performProb0A(storm::models::AbstractNondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + storm::storage::BitVector statesWithProbability0 = performProbGreater0E(model, backwardTransitions, phiStates, psiStates); + statesWithProbability0.complement(); + return statesWithProbability0; } - for (auto predecessorIt = backwardTransitions.constColumnIteratorBegin(currentState), predecessorIte = backwardTransitions.constColumnIteratorEnd(currentState); predecessorIt != predecessorIte; ++predecessorIt) { - if (phiStates.get(*predecessorIt) && (!statesWithProbabilityGreater0.get(*predecessorIt) || (useStepBound && remainingSteps[*predecessorIt] < 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(*predecessorIt, true); - stack.push_back(*predecessorIt); - } 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[*predecessorIt] = currentStepBound - 1; - statesWithProbabilityGreater0.set(*predecessorIt, true); - stack.push_back(*predecessorIt); - stepStack.push_back(currentStepBound - 1); + /*! + * 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, + * this means that these states have probability 1 of satisfying phi until psi if the + * scheduler tries to maximize this probability. + * + * @param model The model whose graph structure to search. + * @param backwardTransitions The reversed transition relation of the model. + * @param phiStates The set of all states satisfying phi. + * @param psiStates The set of all states satisfying psi. + * @return A bit vector that represents all states with probability 1. + */ + template + storm::storage::BitVector performProb1E(storm::models::AbstractNondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + // Get some temporaries for convenience. + storm::storage::SparseMatrix const& transitionMatrix = model.getTransitionMatrix(); + std::vector const& nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices(); + + // Initialize the environment for the iterative algorithm. + storm::storage::BitVector currentStates(model.getNumberOfStates(), true); + std::vector stack; + stack.reserve(model.getNumberOfStates()); + + // 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); + psiStates.addSetIndicesToVector(stack); + + while (!stack.empty()) { + currentState = stack.back(); + stack.pop_back(); + + for(auto predecessorIt = backwardTransitions.constColumnIteratorBegin(currentState), predecessorIte = backwardTransitions.constColumnIteratorEnd(currentState); predecessorIt != predecessorIte; ++predecessorIt) { + if (phiStates.get(*predecessorIt) && !nextStates.get(*predecessorIt)) { + // Check whether the predecessor has only successors in the current state set for one of the + // nondeterminstic choices. + for (auto row = nondeterministicChoiceIndices[*predecessorIt]; row < nondeterministicChoiceIndices[*predecessorIt + 1]; ++row) { + bool allSuccessorsInCurrentStates = true; + for (auto targetIt = transitionMatrix.constColumnIteratorBegin(row), targetIte = transitionMatrix.constColumnIteratorEnd(row); targetIt != targetIte; ++targetIt) { + if (!currentStates.get(*targetIt)) { + 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(*predecessorIt, true); + stack.push_back(*predecessorIt); + break; + } + } + } + } + } + + // Check whether we need to perform an additional iteration. + if (currentStates == nextStates) { + done = true; + } else { + currentStates = std::move(nextStates); } } - } - } - - return statesWithProbabilityGreater0; - } - - /*! - * Computes the sets of states that have probability 0 of satisfying phi until psi under all - * possible resolutions of non-determinism in a non-deterministic model. Stated differently, - * this means that these states have probability 0 of satisfying phi until psi even if the - * scheduler tries to maximize this probability. - * - * @param model The model whose graph structure to search. - * @param backwardTransitions The reversed transition relation of the model. - * @param phiStates The set of all states satisfying phi. - * @param psiStates The set of all states satisfying psi. - * @param useStepBound A flag that indicates whether or not to use the given number of maximal steps for the search. - * @param maximalSteps The maximal number of steps to reach the psi states. - * @return A bit vector that represents all states with probability 0. - */ - template - storm::storage::BitVector performProb0A(storm::models::AbstractNondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { - storm::storage::BitVector statesWithProbability0 = performProbGreater0E(model, backwardTransitions, phiStates, psiStates); - statesWithProbability0.complement(); - return statesWithProbability0; - } - - /*! - * 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, - * this means that these states have probability 1 of satisfying phi until psi if the - * scheduler tries to maximize this probability. - * - * @param model The model whose graph structure to search. - * @param backwardTransitions The reversed transition relation of the model. - * @param phiStates The set of all states satisfying phi. - * @param psiStates The set of all states satisfying psi. - * @return A bit vector that represents all states with probability 1. - */ - template - storm::storage::BitVector performProb1E(storm::models::AbstractNondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { - // Get some temporaries for convenience. - storm::storage::SparseMatrix const& transitionMatrix = model.getTransitionMatrix(); - std::vector const& nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices(); - - // Initialize the environment for the iterative algorithm. - storm::storage::BitVector currentStates(model.getNumberOfStates(), true); - std::vector stack; - stack.reserve(model.getNumberOfStates()); - - // 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); - psiStates.addSetIndicesToVector(stack); - - while (!stack.empty()) { - currentState = stack.back(); - stack.pop_back(); - - for(auto predecessorIt = backwardTransitions.constColumnIteratorBegin(currentState), predecessorIte = backwardTransitions.constColumnIteratorEnd(currentState); predecessorIt != predecessorIte; ++predecessorIt) { - if (phiStates.get(*predecessorIt) && !nextStates.get(*predecessorIt)) { - // Check whether the predecessor has only successors in the current state set for one of the - // nondeterminstic choices. - for (auto row = nondeterministicChoiceIndices[*predecessorIt]; row < nondeterministicChoiceIndices[*predecessorIt + 1]; ++row) { - bool allSuccessorsInCurrentStates = true; - for (auto targetIt = transitionMatrix.constColumnIteratorBegin(row), targetIte = transitionMatrix.constColumnIteratorEnd(row); targetIt != targetIte; ++targetIt) { - if (!currentStates.get(*targetIt)) { - 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(*predecessorIt, true); - stack.push_back(*predecessorIt); - break; - } - } - } - } - } - - // Check whether we need to perform an additional iteration. - if (currentStates == nextStates) { - done = true; - } else { - currentStates = std::move(nextStates); - } - } - - return currentStates; - } - - /*! - * Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi - * until psi in a non-deterministic model in which all non-deterministic choices are resolved - * such that the probability is maximized. - * - * @param model The model whose graph structure to search. - * @param phiStates The set of all states satisfying phi. - * @param psiStates The set of all states satisfying psi. - * @return A pair of bit vectors that represent all states with probability 0 and 1, respectively. - */ - template - std::pair performProb01Max(storm::models::AbstractNondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { - std::pair result; - - // Get the backwards transition relation from the model to ease the search. - storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); - - result.first = performProb0A(model, backwardTransitions, phiStates, psiStates); - result.second = performProb1E(model, backwardTransitions, phiStates, psiStates); - return result; - } - - /*! - * Computes the sets of states that have probability greater 0 of satisfying phi until psi under any - * possible resolution of non-determinism in a non-deterministic model. Stated differently, - * this means that these states have a probability greater 0 of satisfying phi until psi if the - * scheduler tries to maximize this probability. - * - * @param model The model whose graph structure to search. - * @param backwardTransitions The reversed transition relation of the model. - * @param phiStates The set of all states satisfying phi. - * @param psiStates The set of all states satisfying psi. - * @param useStepBound A flag that indicates whether or not to use the given number of maximal steps for the search. - * @param maximalSteps The maximal number of steps to reach the psi states. - * @return A bit vector that represents all states with probability 0. - */ - template - storm::storage::BitVector performProbGreater0A(storm::models::AbstractNondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) { - // Prepare resulting bit vector. - storm::storage::BitVector statesWithProbabilityGreater0(model.getNumberOfStates()); - - // Get some temporaries for convenience. - storm::storage::SparseMatrix const& transitionMatrix = model.getTransitionMatrix(); - std::vector const& nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices(); - - // 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.getSetIndicesList(); - - // Initialize the stack for the step bound, if the number of steps is bounded. - std::vector stepStack; - std::vector remainingSteps; - if (useStepBound) { - stepStack.reserve(model.getNumberOfStates()); - stepStack.insert(stepStack.begin(), psiStates.getNumberOfSetBits(), maximalSteps); - remainingSteps.resize(model.getNumberOfStates()); - for (auto state : psiStates) { - remainingSteps[state] = maximalSteps; + + return currentStates; } - } - - // 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(); + /*! + * Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi + * until psi in a non-deterministic model in which all non-deterministic choices are resolved + * such that the probability is maximized. + * + * @param model The model whose graph structure to search. + * @param phiStates The set of all states satisfying phi. + * @param psiStates The set of all states satisfying psi. + * @return A pair of bit vectors that represent all states with probability 0 and 1, respectively. + */ + template + std::pair performProb01Max(storm::models::AbstractNondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + std::pair result; + + // Get the backwards transition relation from the model to ease the search. + storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); + + result.first = performProb0A(model, backwardTransitions, phiStates, psiStates); + result.second = performProb1E(model, backwardTransitions, phiStates, psiStates); + return result; } - for(auto predecessorIt = backwardTransitions.constColumnIteratorBegin(currentState), predecessorIte = backwardTransitions.constColumnIteratorEnd(currentState); predecessorIt != predecessorIte; ++predecessorIt) { - if (phiStates.get(*predecessorIt) && (!statesWithProbabilityGreater0.get(*predecessorIt) || (useStepBound && remainingSteps[*predecessorIt] < currentStepBound - 1))) { - // Check whether the predecessor has at least one successor in the current state set for every - // nondeterministic choice. - bool addToStatesWithProbabilityGreater0 = true; - for (auto row = nondeterministicChoiceIndices[*predecessorIt]; row < nondeterministicChoiceIndices[*predecessorIt + 1]; ++row) { - bool hasAtLeastOneSuccessorWithProbabilityGreater0 = false; - for (auto successorIt = transitionMatrix.constColumnIteratorBegin(row), successorIte = transitionMatrix.constColumnIteratorEnd(row); successorIt != successorIte; ++successorIt) { - if (statesWithProbabilityGreater0.get(*successorIt)) { - hasAtLeastOneSuccessorWithProbabilityGreater0 = true; - break; + /*! + * Computes the sets of states that have probability greater 0 of satisfying phi until psi under any + * possible resolution of non-determinism in a non-deterministic model. Stated differently, + * this means that these states have a probability greater 0 of satisfying phi until psi if the + * scheduler tries to maximize this probability. + * + * @param model The model whose graph structure to search. + * @param backwardTransitions The reversed transition relation of the model. + * @param phiStates The set of all states satisfying phi. + * @param psiStates The set of all states satisfying psi. + * @param useStepBound A flag that indicates whether or not to use the given number of maximal steps for the search. + * @param maximalSteps The maximal number of steps to reach the psi states. + * @return A bit vector that represents all states with probability 0. + */ + template + storm::storage::BitVector performProbGreater0A(storm::models::AbstractNondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) { + // Prepare resulting bit vector. + storm::storage::BitVector statesWithProbabilityGreater0(model.getNumberOfStates()); + + // Get some temporaries for convenience. + storm::storage::SparseMatrix const& transitionMatrix = model.getTransitionMatrix(); + std::vector const& nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices(); + + // 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.getSetIndicesList(); + + // Initialize the stack for the step bound, if the number of steps is bounded. + std::vector stepStack; + std::vector remainingSteps; + if (useStepBound) { + stepStack.reserve(model.getNumberOfStates()); + stepStack.insert(stepStack.begin(), psiStates.getNumberOfSetBits(), maximalSteps); + remainingSteps.resize(model.getNumberOfStates()); + 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(auto predecessorIt = backwardTransitions.constColumnIteratorBegin(currentState), predecessorIte = backwardTransitions.constColumnIteratorEnd(currentState); predecessorIt != predecessorIte; ++predecessorIt) { + if (phiStates.get(*predecessorIt) && (!statesWithProbabilityGreater0.get(*predecessorIt) || (useStepBound && remainingSteps[*predecessorIt] < currentStepBound - 1))) { + // Check whether the predecessor has at least one successor in the current state set for every + // nondeterministic choice. + bool addToStatesWithProbabilityGreater0 = true; + for (auto row = nondeterministicChoiceIndices[*predecessorIt]; row < nondeterministicChoiceIndices[*predecessorIt + 1]; ++row) { + bool hasAtLeastOneSuccessorWithProbabilityGreater0 = false; + for (auto successorIt = transitionMatrix.constColumnIteratorBegin(row), successorIte = transitionMatrix.constColumnIteratorEnd(row); successorIt != successorIte; ++successorIt) { + if (statesWithProbabilityGreater0.get(*successorIt)) { + 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(*predecessorIt, true); + stack.push_back(*predecessorIt); + } 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[*predecessorIt] = currentStepBound - 1; + statesWithProbabilityGreater0.set(*predecessorIt, true); + stack.push_back(*predecessorIt); + stepStack.push_back(currentStepBound - 1); + } } } + } + } + + return statesWithProbabilityGreater0; + } + + /*! + * Computes the sets of states that have probability 0 of satisfying phi until psi under at least + * one possible resolution of non-determinism in a non-deterministic model. Stated differently, + * this means that these states have probability 0 of satisfying phi until psi if the + * scheduler tries to minimize this probability. + * + * @param model The model whose graph structure to search. + * @param backwardTransitions The reversed transition relation of the model. + * @param phiStates The set of all states satisfying phi. + * @param psiStates The set of all states satisfying psi. + * @return A bit vector that represents all states with probability 0. + */ + template + storm::storage::BitVector performProb0E(storm::models::AbstractNondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + storm::storage::BitVector statesWithProbability0 = performProbGreater0A(model, backwardTransitions, phiStates, psiStates); + statesWithProbability0.complement(); + return statesWithProbability0; + } + + /*! + * Computes the sets of states that have probability 1 of satisfying phi until psi under all + * possible resolutions of non-determinism in a non-deterministic model. Stated differently, + * this means that these states have probability 1 of satisfying phi until psi even if the + * scheduler tries to minimize this probability. + * + * @param model The model whose graph structure to search. + * @param backwardTransitions The reversed transition relation of the model. + * @param phiStates The set of all states satisfying phi. + * @param psiStates The set of all states satisfying psi. + * @return A bit vector that represents all states with probability 0. + */ + template + storm::storage::BitVector performProb1A(storm::models::AbstractNondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + // Get some temporaries for convenience. + storm::storage::SparseMatrix const& transitionMatrix = model.getTransitionMatrix(); + std::vector const& nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices(); + + // Initialize the environment for the iterative algorithm. + storm::storage::BitVector currentStates(model.getNumberOfStates(), true); + std::vector stack; + stack.reserve(model.getNumberOfStates()); + + // 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); + psiStates.addSetIndicesToVector(stack); + + while (!stack.empty()) { + currentState = stack.back(); + stack.pop_back(); - if (!hasAtLeastOneSuccessorWithProbabilityGreater0) { - addToStatesWithProbabilityGreater0 = false; - break; + for(auto predecessorIt = backwardTransitions.constColumnIteratorBegin(currentState), predecessorIte = backwardTransitions.constColumnIteratorEnd(currentState); predecessorIt != predecessorIte; ++predecessorIt) { + if (phiStates.get(*predecessorIt) && !nextStates.get(*predecessorIt)) { + // Check whether the predecessor has only successors in the current state set for all of the + // nondeterminstic choices. + bool allSuccessorsInCurrentStatesForAllChoices = true; + for (auto row = nondeterministicChoiceIndices[*predecessorIt]; row < nondeterministicChoiceIndices[*predecessorIt + 1]; ++row) { + for (auto successorIt = transitionMatrix.constColumnIteratorBegin(row), successorIte = transitionMatrix.constColumnIteratorEnd(row); successorIt != successorIte; ++successorIt) { + if (!currentStates.get(*successorIt)) { + allSuccessorsInCurrentStatesForAllChoices = false; + goto afterCheckLoop; + } + } + } + + 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 (allSuccessorsInCurrentStatesForAllChoices) { + nextStates.set(*predecessorIt, true); + stack.push_back(*predecessorIt); + } + } } } - // 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(*predecessorIt, true); - stack.push_back(*predecessorIt); - } 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[*predecessorIt] = currentStepBound - 1; - statesWithProbabilityGreater0.set(*predecessorIt, true); - stack.push_back(*predecessorIt); - stepStack.push_back(currentStepBound - 1); - } + // Check whether we need to perform an additional iteration. + if (currentStates == nextStates) { + done = true; + } else { + currentStates = std::move(nextStates); } } - } - } - - return statesWithProbabilityGreater0; - } - - /*! - * Computes the sets of states that have probability 0 of satisfying phi until psi under at least - * one possible resolution of non-determinism in a non-deterministic model. Stated differently, - * this means that these states have probability 0 of satisfying phi until psi if the - * scheduler tries to minimize this probability. - * - * @param model The model whose graph structure to search. - * @param backwardTransitions The reversed transition relation of the model. - * @param phiStates The set of all states satisfying phi. - * @param psiStates The set of all states satisfying psi. - * @return A bit vector that represents all states with probability 0. - */ - template - storm::storage::BitVector performProb0E(storm::models::AbstractNondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { - storm::storage::BitVector statesWithProbability0 = performProbGreater0A(model, backwardTransitions, phiStates, psiStates); - statesWithProbability0.complement(); - return statesWithProbability0; - } - - /*! - * Computes the sets of states that have probability 1 of satisfying phi until psi under all - * possible resolutions of non-determinism in a non-deterministic model. Stated differently, - * this means that these states have probability 1 of satisfying phi until psi even if the - * scheduler tries to minimize this probability. - * - * @param model The model whose graph structure to search. - * @param backwardTransitions The reversed transition relation of the model. - * @param phiStates The set of all states satisfying phi. - * @param psiStates The set of all states satisfying psi. - * @return A bit vector that represents all states with probability 0. - */ - template - storm::storage::BitVector performProb1A(storm::models::AbstractNondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { - // Get some temporaries for convenience. - storm::storage::SparseMatrix const& transitionMatrix = model.getTransitionMatrix(); - std::vector const& nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices(); - - // Initialize the environment for the iterative algorithm. - storm::storage::BitVector currentStates(model.getNumberOfStates(), true); - std::vector stack; - stack.reserve(model.getNumberOfStates()); - - // 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); - psiStates.addSetIndicesToVector(stack); - - while (!stack.empty()) { - currentState = stack.back(); - stack.pop_back(); - - for(auto predecessorIt = backwardTransitions.constColumnIteratorBegin(currentState), predecessorIte = backwardTransitions.constColumnIteratorEnd(currentState); predecessorIt != predecessorIte; ++predecessorIt) { - if (phiStates.get(*predecessorIt) && !nextStates.get(*predecessorIt)) { - // Check whether the predecessor has only successors in the current state set for all of the - // nondeterminstic choices. - bool allSuccessorsInCurrentStatesForAllChoices = true; - for (auto row = nondeterministicChoiceIndices[*predecessorIt]; row < nondeterministicChoiceIndices[*predecessorIt + 1]; ++row) { - for (auto successorIt = transitionMatrix.constColumnIteratorBegin(row), successorIte = transitionMatrix.constColumnIteratorEnd(row); successorIt != successorIte; ++successorIt) { - if (!currentStates.get(*successorIt)) { - allSuccessorsInCurrentStatesForAllChoices = false; - goto afterCheckLoop; - } - } - } - - 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 (allSuccessorsInCurrentStatesForAllChoices) { - nextStates.set(*predecessorIt, true); - stack.push_back(*predecessorIt); - } - } - } - } - - // Check whether we need to perform an additional iteration. - if (currentStates == nextStates) { - done = true; - } else { - currentStates = std::move(nextStates); - } - } - return currentStates; - } - - /*! - * Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi - * until psi in a non-deterministic model in which all non-deterministic choices are resolved - * such that the probability is minimized. - * - * @param model The model whose graph structure to search. - * @param phiStates The set of all states satisfying phi. - * @param psiStates The set of all states satisfying psi. - * @return A pair of bit vectors that represent all states with probability 0 and 1, respectively. - */ - template - std::pair performProb01Min(storm::models::AbstractNondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { - std::pair result; - - // Get the backwards transition relation from the model to ease the search. - storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); - - result.first = performProb0E(model, backwardTransitions, phiStates, psiStates); - result.second = performProb1A(model, backwardTransitions, phiStates, psiStates); - return result; - } - - /*! - * Performs an SCC decomposition using Tarjan's algorithm. - * - * @param startState The state at which the search is started. - * @param currentIndex The index that is to be used as the next free index. - * @param stateIndices The vector that stores the index for each state. - * @param lowlinks A vector that stores the lowlink of each state, i.e. the lowest index of a state reachable from - * a particular state. - * @param tarjanStack A stack used for Tarjan's algorithm. - * @param tarjanStackStates A bit vector that represents all states that are currently contained in tarjanStack. - * @param visitedStates A bit vector that stores all states that have already been visited. - * @param matrix The transition matrix representing the graph structure. - * @param stronglyConnectedComponents A vector of strongly connected components to which newly found SCCs are added. - */ - template - void performSccDecompositionHelper(uint_fast64_t startState, uint_fast64_t& currentIndex, std::vector& stateIndices, std::vector& lowlinks, std::vector& tarjanStack, storm::storage::BitVector& tarjanStackStates, storm::storage::BitVector& visitedStates, storm::storage::SparseMatrix const& matrix, std::vector>& stronglyConnectedComponents) { - // Create the stacks needed for turning the recursive formulation of Tarjan's algorithm - // into an iterative version. In particular, we keep one stack for states and one stack - // for the iterators. The last one is not strictly needed, but reduces iteration work when - // all successors of a particular state are considered. - std::vector recursionStateStack; - recursionStateStack.reserve(lowlinks.size()); - std::vector::ConstIndexIterator> recursionIteratorStack; - recursionIteratorStack.reserve(lowlinks.size()); - std::vector statesInStack(lowlinks.size()); - - // Initialize the recursion stacks with the given initial state (and its successor iterator). - recursionStateStack.push_back(startState); - recursionIteratorStack.push_back(matrix.constColumnIteratorBegin(startState)); - - recursionStepForward: - while (!recursionStateStack.empty()) { - uint_fast64_t currentState = recursionStateStack.back(); - typename storm::storage::SparseMatrix::ConstIndexIterator successorIt = recursionIteratorStack.back(); + return currentStates; + } - // Perform the treatment of newly discovered state as defined by Tarjan's algorithm - visitedStates.set(currentState, true); - stateIndices[currentState] = currentIndex; - lowlinks[currentState] = currentIndex; - ++currentIndex; - tarjanStack.push_back(currentState); - tarjanStackStates.set(currentState, true); + /*! + * Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi + * until psi in a non-deterministic model in which all non-deterministic choices are resolved + * such that the probability is minimized. + * + * @param model The model whose graph structure to search. + * @param phiStates The set of all states satisfying phi. + * @param psiStates The set of all states satisfying psi. + * @return A pair of bit vectors that represent all states with probability 0 and 1, respectively. + */ + template + std::pair performProb01Min(storm::models::AbstractNondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + std::pair result; + + // Get the backwards transition relation from the model to ease the search. + storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); + + result.first = performProb0E(model, backwardTransitions, phiStates, psiStates); + result.second = performProb1A(model, backwardTransitions, phiStates, psiStates); + return result; + } - // Now, traverse all successors of the current state. - for(; successorIt != matrix.constColumnIteratorEnd(currentState); ++successorIt) { - // If we have not visited the successor already, we need to perform the procedure - // recursively on the newly found state. - if (!visitedStates.get(*successorIt)) { - // Save current iterator position so we can continue where we left off later. - recursionIteratorStack.pop_back(); - recursionIteratorStack.push_back(successorIt); + /*! + * Performs an SCC decomposition using Tarjan's algorithm. + * + * @param startState The state at which the search is started. + * @param currentIndex The index that is to be used as the next free index. + * @param stateIndices The vector that stores the index for each state. + * @param lowlinks A vector that stores the lowlink of each state, i.e. the lowest index of a state reachable from + * a particular state. + * @param tarjanStack A stack used for Tarjan's algorithm. + * @param tarjanStackStates A bit vector that represents all states that are currently contained in tarjanStack. + * @param visitedStates A bit vector that stores all states that have already been visited. + * @param matrix The transition matrix representing the graph structure. + * @param stronglyConnectedComponents A vector of strongly connected components to which newly found SCCs are added. + */ + template + void performSccDecompositionHelper(uint_fast64_t startState, uint_fast64_t& currentIndex, std::vector& stateIndices, std::vector& lowlinks, std::vector& tarjanStack, storm::storage::BitVector& tarjanStackStates, storm::storage::BitVector& visitedStates, storm::storage::SparseMatrix const& matrix, std::vector>& stronglyConnectedComponents) { + // Create the stacks needed for turning the recursive formulation of Tarjan's algorithm + // into an iterative version. In particular, we keep one stack for states and one stack + // for the iterators. The last one is not strictly needed, but reduces iteration work when + // all successors of a particular state are considered. + std::vector recursionStateStack; + recursionStateStack.reserve(lowlinks.size()); + std::vector::ConstIndexIterator> recursionIteratorStack; + recursionIteratorStack.reserve(lowlinks.size()); + std::vector statesInStack(lowlinks.size()); + + // Initialize the recursion stacks with the given initial state (and its successor iterator). + recursionStateStack.push_back(startState); + recursionIteratorStack.push_back(matrix.constColumnIteratorBegin(startState)); + + recursionStepForward: + while (!recursionStateStack.empty()) { + uint_fast64_t currentState = recursionStateStack.back(); + typename storm::storage::SparseMatrix::ConstIndexIterator successorIt = recursionIteratorStack.back(); - // Put unvisited successor on top of our recursion stack and remember that. - recursionStateStack.push_back(*successorIt); - statesInStack[*successorIt] = true; + // Perform the treatment of newly discovered state as defined by Tarjan's algorithm + visitedStates.set(currentState, true); + stateIndices[currentState] = currentIndex; + lowlinks[currentState] = currentIndex; + ++currentIndex; + tarjanStack.push_back(currentState); + tarjanStackStates.set(currentState, true); - // Also, put initial value for iterator on corresponding recursion stack. - recursionIteratorStack.push_back(matrix.constColumnIteratorBegin(*successorIt)); + // Now, traverse all successors of the current state. + for(; successorIt != matrix.constColumnIteratorEnd(currentState); ++successorIt) { + // If we have not visited the successor already, we need to perform the procedure + // recursively on the newly found state. + if (!visitedStates.get(*successorIt)) { + // Save current iterator position so we can continue where we left off later. + recursionIteratorStack.pop_back(); + recursionIteratorStack.push_back(successorIt); + + // Put unvisited successor on top of our recursion stack and remember that. + recursionStateStack.push_back(*successorIt); + statesInStack[*successorIt] = true; + + // Also, put initial value for iterator on corresponding recursion stack. + recursionIteratorStack.push_back(matrix.constColumnIteratorBegin(*successorIt)); + + // Perform the actual recursion step in an iterative way. + goto recursionStepForward; + + recursionStepBackward: + lowlinks[currentState] = std::min(lowlinks[currentState], lowlinks[*successorIt]); + } else if (tarjanStackStates.get(*successorIt)) { + // Update the lowlink of the current state. + lowlinks[currentState] = std::min(lowlinks[currentState], stateIndices[*successorIt]); + } + } - // Perform the actual recursion step in an iterative way. - goto recursionStepForward; + // If the current state is the root of a SCC, we need to pop all states of the SCC from + // the algorithm's stack. + if (lowlinks[currentState] == stateIndices[currentState]) { + stronglyConnectedComponents.emplace_back(); + + uint_fast64_t lastState = 0; + do { + // Pop topmost state from the algorithm's stack. + lastState = tarjanStack.back(); + tarjanStack.pop_back(); + tarjanStackStates.set(lastState, false); + + // Add the state to the current SCC. + stronglyConnectedComponents.back().push_back(lastState); + } while (lastState != currentState); + } - recursionStepBackward: - lowlinks[currentState] = std::min(lowlinks[currentState], lowlinks[*successorIt]); - } else if (tarjanStackStates.get(*successorIt)) { - // Update the lowlink of the current state. - lowlinks[currentState] = std::min(lowlinks[currentState], stateIndices[*successorIt]); - } - } - - // If the current state is the root of a SCC, we need to pop all states of the SCC from - // the algorithm's stack. - if (lowlinks[currentState] == stateIndices[currentState]) { - stronglyConnectedComponents.emplace_back(); - - uint_fast64_t lastState = 0; - do { - // Pop topmost state from the algorithm's stack. - lastState = tarjanStack.back(); - tarjanStack.pop_back(); - tarjanStackStates.set(lastState, false); + // 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. + recursionStateStack.pop_back(); + recursionIteratorStack.pop_back(); - // Add the state to the current SCC. - stronglyConnectedComponents.back().push_back(lastState); - } while (lastState != currentState); - } + // 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 (recursionStateStack.size() > 0) { + currentState = recursionStateStack.back(); + successorIt = recursionIteratorStack.back(); + + goto recursionStepBackward; + } + } + } - // 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. - recursionStateStack.pop_back(); - recursionIteratorStack.pop_back(); + /*! + * Performs a decomposition of the given model into its SCCs. + * + * @param model The nondeterminstic model to decompose. + * @return A vector of SCCs of the model. + */ + template + std::vector> performSccDecomposition(storm::models::AbstractModel const& model) { + LOG4CPLUS_INFO(logger, "Computing SCC decomposition."); + + std::vector> scc; + uint_fast64_t numberOfStates = model.getNumberOfStates(); + + // Set up the environment of Tarjan's algorithm. + std::vector tarjanStack; + tarjanStack.reserve(numberOfStates); + storm::storage::BitVector tarjanStackStates(numberOfStates); + std::vector stateIndices(numberOfStates); + std::vector lowlinks(numberOfStates); + storm::storage::BitVector visitedStates(numberOfStates); + + // Start the search for SCCs from every vertex in the graph structure, because there is. + uint_fast64_t currentIndex = 0; + for (uint_fast64_t state = 0; state < numberOfStates; ++state) { + if (!visitedStates.get(state)) { + performSccDecompositionHelper(state, currentIndex, stateIndices, lowlinks, tarjanStack, tarjanStackStates, visitedStates, model.getTransitionMatrix(), scc); + } + } + + LOG4CPLUS_INFO(logger, "Done computing SCC decomposition."); + return scc; + } - // 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 (recursionStateStack.size() > 0) { - currentState = recursionStateStack.back(); - successorIt = recursionIteratorStack.back(); - - goto recursionStepBackward; - } - } - } - - /*! - * Performs a decomposition of the given model into its SCCs. - * - * @param model The nondeterminstic model to decompose. - * @return A vector of SCCs of the model. - */ - template - std::vector> performSccDecomposition(storm::models::AbstractModel const& model) { - LOG4CPLUS_INFO(logger, "Computing SCC decomposition."); - - std::vector> scc; - uint_fast64_t numberOfStates = model.getNumberOfStates(); + /*! + * Performs a topological sort of the states of the system according to the given transitions. + * + * @param matrix A square matrix representing the transition relation of the system. + * @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::ConstIndexIterator> 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.constColumnIteratorBegin(state)); + + recursionStepForward: + while (!recursionStack.empty()) { + uint_fast64_t currentState = recursionStack.back(); + typename storm::storage::SparseMatrix::ConstIndexIterator successorIt = iteratorRecursionStack.back(); + + visitedStates.set(currentState, true); + + recursionStepBackward: + for (; successorIt != matrix.constColumnIteratorEnd(currentState); ++successorIt) { + if (!visitedStates.get(*successorIt)) { + // Put unvisited successor on top of our recursion stack and remember that. + recursionStack.push_back(*successorIt); + + // Save current iterator position so we can continue where we left off later. + iteratorRecursionStack.pop_back(); + iteratorRecursionStack.push_back(successorIt + 1); + + // Also, put initial value for iterator on corresponding recursion stack. + iteratorRecursionStack.push_back(matrix.constColumnIteratorBegin(*successorIt)); + + 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(); + successorIt = iteratorRecursionStack.back(); + + goto recursionStepBackward; + } + } + } + } + + return topologicalSort; + } - // Set up the environment of Tarjan's algorithm. - std::vector tarjanStack; - tarjanStack.reserve(numberOfStates); - storm::storage::BitVector tarjanStackStates(numberOfStates); - std::vector stateIndices(numberOfStates); - std::vector lowlinks(numberOfStates); - storm::storage::BitVector visitedStates(numberOfStates); + /*! + * A class needed to compare the distances for two states in the Dijkstra search. + */ + template + struct DistanceCompare { + bool operator()(std::pair const& lhs, std::pair const& rhs) const { + return lhs.first > rhs.first || (lhs.first == rhs.first && lhs.second > rhs.second); + } + }; - // Start the search for SCCs from every vertex in the graph structure, because there is. - uint_fast64_t currentIndex = 0; - for (uint_fast64_t state = 0; state < numberOfStates; ++state) { - if (!visitedStates.get(state)) { - performSccDecompositionHelper(state, currentIndex, stateIndices, lowlinks, tarjanStack, tarjanStackStates, visitedStates, model.getTransitionMatrix(), scc); - } - } - - LOG4CPLUS_INFO(logger, "Done computing SCC decomposition."); - return scc; - } - - /*! - * Performs a topological sort of the states of the system according to the given transitions. - * - * @param matrix A square matrix representing the transition relation of the system. - * @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::ConstIndexIterator> 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.constColumnIteratorBegin(state)); - - recursionStepForward: - while (!recursionStack.empty()) { - uint_fast64_t currentState = recursionStack.back(); - typename storm::storage::SparseMatrix::ConstIndexIterator successorIt = iteratorRecursionStack.back(); - - visitedStates.set(currentState, true); - - recursionStepBackward: - for (; successorIt != matrix.constColumnIteratorEnd(currentState); ++successorIt) { - if (!visitedStates.get(*successorIt)) { - // Put unvisited successor on top of our recursion stack and remember that. - recursionStack.push_back(*successorIt); - - // Save current iterator position so we can continue where we left off later. - iteratorRecursionStack.pop_back(); - iteratorRecursionStack.push_back(successorIt + 1); - - // Also, put initial value for iterator on corresponding recursion stack. - iteratorRecursionStack.push_back(matrix.constColumnIteratorBegin(*successorIt)); - - 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(); - successorIt = iteratorRecursionStack.back(); - - goto recursionStepBackward; - } - } - } - } - - return topologicalSort; - } - - /*! - * A class needed to compare the distances for two states in the Dijkstra search. - */ - template - struct DistanceCompare { - bool operator()(std::pair const& lhs, std::pair const& rhs) const { - return lhs.first < rhs.first || (lhs.first == rhs.first && lhs.second < rhs.second); - } - }; - - /*! - * Performs a Dijkstra search from the given starting states to determine the most probable paths to all other states - * by only passing through the given state set. - * - * @param model The model whose state space is to be searched. - * @param transitions The transitions wrt to which to compute the most probable paths. - * @param startingStates The starting states of the Dijkstra search. - * @param filterStates A set of states that must not be left on any path. - */ - template - std::pair, std::vector> performDijkstra(storm::models::AbstractModel 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::constGetZero(); - std::vector probabilities(model.getNumberOfStates(), storm::utility::constGetZero()); - 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::constGetZero(), state); - probabilities[state] = 1; - } - - // 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.getRows(probabilityStatePair.second, probabilityStatePair.second); - for (auto& transition : row) { - // Only follow the transition if it lies within the filtered states. - if (filterStates != nullptr && filterStates->get(transition.column())) { - // Calculate the distance we achieve when we take the path to the successor via the current state. - T newDistance = probabilityStatePair.first * transition.value(); + /*! + * Performs a Dijkstra search from the given starting states to determine the most probable paths to all other states + * by only passing through the given state set. + * + * @param model The model whose state space is to be searched. + * @param transitions The transitions wrt to which to compute the most probable paths. + * @param startingStates The starting states of the Dijkstra search. + * @param filterStates A set of states that must not be left on any path. + */ + template + std::pair, std::vector> performDijkstra(storm::models::AbstractModel 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::constGetZero(); + std::vector probabilities(model.getNumberOfStates(), storm::utility::constGetZero()); + 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::constGetOne(), state); + probabilities[state] = storm::utility::constGetOne(); + } + + // 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()); - // We found a cheaper way to get to the target state of the transition. - if (newDistance > probabilities[transition.column()]) { - // Remove the old distance. - if (probabilities[transition.column()] != noPredecessorValue) { - probabilityStateSet.erase(std::make_pair(probabilities[transition.column()], transition.column())); + // Now check the new distances for all successors of the current state. + typename storm::storage::SparseMatrix::Rows row = transitions.getRows(probabilityStatePair.second, probabilityStatePair.second); + for (auto& transition : row) { + // Only follow the transition if it lies within the filtered states. + if (filterStates != nullptr && filterStates->get(transition.column())) { + // Calculate the distance we achieve when we take the path to the successor via the current state. + T newDistance = probabilityStatePair.first * transition.value(); + + // We found a cheaper way to get to the target state of the transition. + if (newDistance > probabilities[transition.column()]) { + // Remove the old distance. + if (probabilities[transition.column()] != noPredecessorValue) { + probabilityStateSet.erase(std::make_pair(probabilities[transition.column()], transition.column())); + } + + // Set and add the new distance. + probabilities[transition.column()] = newDistance; + predecessors[transition.column()] = probabilityStatePair.second; + probabilityStateSet.insert(std::make_pair(newDistance, transition.column())); + } } - - // Set and add the new distance. - probabilities[transition.column()] = newDistance; - predecessors[transition.column()] = probabilityStatePair.second; - probabilityStateSet.insert(std::make_pair(newDistance, transition.column())); } } + + // 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; } - } - - // 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; - } - -} // namespace graph - -} // namespace utility - + + } // namespace graph + } // namespace utility } // namespace storm #endif /* STORM_UTILITY_GRAPH_H_ */