#include "graph.h" #include "utility/OsDetection.h" #include "storm-config.h" #include "storm/adapters/RationalFunctionAdapter.h" #include "storm/storage/sparse/StateType.h" #include "storm/storage/dd/Bdd.h" #include "storm/storage/dd/Add.h" #include "storm/storage/dd/DdManager.h" #include "storm/abstraction/ExplicitGameStrategyPair.h" #include "storm/storage/StronglyConnectedComponentDecomposition.h" #include "storm/models/symbolic/DeterministicModel.h" #include "storm/models/symbolic/NondeterministicModel.h" #include "storm/models/symbolic/StandardRewardModel.h" #include "storm/models/symbolic/StochasticTwoPlayerGame.h" #include "storm/models/sparse/DeterministicModel.h" #include "storm/models/sparse/NondeterministicModel.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/utility/constants.h" #include "storm/utility/macros.h" #include "storm/exceptions/InvalidArgumentException.h" #include 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, bool useStepBound, uint_fast64_t maximalSteps, boost::optional const& choiceFilter) { storm::storage::BitVector reachableStates(initialStates); uint_fast64_t numberOfStates = transitionMatrix.getRowGroupCount(); // Initialize the stack used for the DFS with the states. std::vector stack(initialStates.begin(), initialStates.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(), initialStates.getNumberOfSetBits(), maximalSteps); remainingSteps.resize(numberOfStates); for (auto state : initialStates) { remainingSteps[state] = maximalSteps; } } // Perform the actual DFS. uint_fast64_t currentState = 0, currentStepBound = 0; while (!stack.empty()) { currentState = stack.back(); stack.pop_back(); if (useStepBound) { currentStepBound = stepStack.back(); stepStack.pop_back(); if (currentStepBound == 0) { continue; } } uint64_t row = transitionMatrix.getRowGroupIndices()[currentState]; if (choiceFilter) { row = choiceFilter->getNextSetIndex(row); } uint64_t const rowGroupEnd = transitionMatrix.getRowGroupIndices()[currentState + 1]; while (row < rowGroupEnd) { for (auto const& successor : transitionMatrix.getRow(row)) { // Only explore the state if the transition was actually there and the successor has not yet // been visited. if (!storm::utility::isZero(successor.getValue()) && (!reachableStates.get(successor.getColumn()) || (useStepBound && remainingSteps[successor.getColumn()] < currentStepBound - 1))) { // 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 potentially need to follow it. if (useStepBound) { // As there is at least one more step to go, we need to push the state and the new number of steps. remainingSteps[successor.getColumn()] = currentStepBound - 1; stepStack.push_back(currentStepBound - 1); } reachableStates.set(successor.getColumn()); stack.push_back(successor.getColumn()); } } } ++row; if (choiceFilter) { row = choiceFilter->getNextSetIndex(row); } } } return reachableStates; } template storm::storage::BitVector getBsccCover(storm::storage::SparseMatrix const& transitionMatrix) { storm::storage::BitVector result(transitionMatrix.getRowGroupCount()); storm::storage::StronglyConnectedComponentDecomposition decomposition(transitionMatrix, false, true); // Take the first state out of each BSCC. for (auto const& scc : decomposition) { result.set(*scc.begin()); } return result; } template bool hasCycle(storm::storage::SparseMatrix const& transitionMatrix, boost::optional const& subsystem) { storm::storage::BitVector unexploredStates; // States that have not been visited yet storm::storage::BitVector acyclicStates; // States that are known to not lie on a cycle consisting of subsystem states if (subsystem) { unexploredStates = subsystem.get(); acyclicStates = ~subsystem.get(); } else { unexploredStates.resize(transitionMatrix.getRowGroupCount(), true); acyclicStates.resize(transitionMatrix.getRowGroupCount(), false); } std::vector dfsStack; for (uint64_t start = unexploredStates.getNextSetIndex(0); start < unexploredStates.size(); start = unexploredStates.getNextSetIndex(start + 1)) { dfsStack.push_back(start); while (!dfsStack.empty()) { uint64_t state = dfsStack.back(); if (unexploredStates.get(state)) { unexploredStates.set(state, false); for (auto const& entry : transitionMatrix.getRowGroup(start)) { if (unexploredStates.get(entry.getColumn())) { dfsStack.push_back(entry.getColumn()); } else { if (!acyclicStates.get(entry.getColumn())) { // The state has been visited before but is not known to be acyclic. return true; } } } } else { acyclicStates.set(state, true); dfsStack.pop_back(); } } } return false; } template bool checkIfECWithChoiceExists(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& choices) { STORM_LOG_THROW(subsystem.size() == transitionMatrix.getRowGroupCount(), storm::exceptions::InvalidArgumentException, "Invalid size of subsystem"); STORM_LOG_THROW(choices.size() == transitionMatrix.getRowCount(), storm::exceptions::InvalidArgumentException, "Invalid size of choice vector"); if (subsystem.empty() || choices.empty()) { return false; } storm::storage::BitVector statesWithChoice(transitionMatrix.getRowGroupCount(), false); uint_fast64_t state = 0; for (auto const& choice : choices) { // Get the correct state while (choice >= transitionMatrix.getRowGroupIndices()[state + 1]) { ++state; } assert(choice >= transitionMatrix.getRowGroupIndices()[state]); // make sure that the choice originates from the subsystem and also stays within the subsystem if (subsystem.get(state)) { bool choiceStaysInSubsys = true; for (auto const& entry : transitionMatrix.getRow(choice)) { if (!subsystem.get(entry.getColumn())) { choiceStaysInSubsys = false; break; } } if (choiceStaysInSubsys) { statesWithChoice.set(state, true); } } } // Initialize candidate states that satisfy some necessary conditions for being part of an EC with a specified choice: // Get the states for which a policy can enforce that a choice is reached while staying inside the subsystem storm::storage::BitVector candidateStates = storm::utility::graph::performProb1E(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, subsystem, statesWithChoice); // Only keep the states that can stay in the set of candidates forever candidateStates = storm::utility::graph::performProb0E(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, candidateStates, ~candidateStates); // Only keep the states that can be reached after performing one of the specified choices statesWithChoice &= candidateStates; storm::storage::BitVector choiceTargets(transitionMatrix.getRowGroupCount(), false); for (auto const& state : statesWithChoice) { for (uint_fast64_t choice = choices.getNextSetIndex(transitionMatrix.getRowGroupIndices()[state]); choice < transitionMatrix.getRowGroupIndices()[state + 1]; choice = choices.getNextSetIndex(choice + 1)) { bool choiceStaysInCandidateSet = true; for (auto const& entry : transitionMatrix.getRow(choice)) { if (!candidateStates.get(entry.getColumn())) { choiceStaysInCandidateSet = false; break; } } if (choiceStaysInCandidateSet) { for (auto const& entry : transitionMatrix.getRow(choice)) { choiceTargets.set(entry.getColumn(), true); } } } } candidateStates = storm::utility::graph::getReachableStates(transitionMatrix, choiceTargets, candidateStates, storm::storage::BitVector(candidateStates.size(), false)); // At this point we know that every candidate state can reach a state with a choice without leaving the set of candidate states. // We now compute the states that can reach a choice at least twice, three times, four times, ... until a fixpoint is reached. while (!candidateStates.empty()) { // Update the states with a choice that stays within the set of candidates statesWithChoice &= candidateStates; for (auto const& state : statesWithChoice) { bool stateHasChoice = false; for (uint_fast64_t choice = choices.getNextSetIndex(transitionMatrix.getRowGroupIndices()[state]); choice < transitionMatrix.getRowGroupIndices()[state + 1]; choice = choices.getNextSetIndex(choice + 1)) { bool choiceStaysInCandidateSet = true; for (auto const& entry : transitionMatrix.getRow(choice)) { if (!candidateStates.get(entry.getColumn())) { choiceStaysInCandidateSet = false; break; } } if (choiceStaysInCandidateSet) { stateHasChoice = true; break; } } if (!stateHasChoice) { statesWithChoice.set(state, false); } } // Update the candidates storm::storage::BitVector newCandidates = storm::utility::graph::performProb1E(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, candidateStates, statesWithChoice); // Check if converged if (newCandidates == candidateStates) { assert(!candidateStates.empty()); return true; } candidateStates = std::move(newCandidates); } return false; } template std::vector getDistances(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, boost::optional const& subsystem) { 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())) { if (!subsystem || subsystem.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(); if(currentStepBound == 0) { continue; } } 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))) { statesWithProbabilityGreater0.set(entryIt->getColumn(), true); // If we don't have a bound on the number of steps to take, just add the state to the stack. if (useStepBound) { // As 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; stepStack.push_back(currentStepBound - 1); } stack.push_back(entryIt->getColumn()); } } } // Return result. return statesWithProbabilityGreater0; } template storm::storage::BitVector performProb1(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const&, 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.inverseRelationalProduct(transitionMatrix, model.getRowVariables(), 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&, 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::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { std::pair, storm::dd::Bdd> result; 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 void computeSchedulerStayingInStates(storm::storage::BitVector const& states, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::Scheduler& scheduler) { std::vector const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices(); for (auto const& state : states) { bool setValue = false; STORM_LOG_ASSERT(nondeterministicChoiceIndices[state+1] - nondeterministicChoiceIndices[state] > 0, "Expected at least one action enabled in state " << state); for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) { bool allSuccessorsInStates = true; for (auto const& element : transitionMatrix.getRow(choice)) { if (!states.get(element.getColumn())) { allSuccessorsInStates = false; break; } } if (allSuccessorsInStates) { for (uint_fast64_t memState = 0; memState < scheduler.getNumberOfMemoryStates(); ++memState) { scheduler.setChoice(choice - nondeterministicChoiceIndices[state], state, memState); } setValue = true; break; } } STORM_LOG_ASSERT(setValue, "Expected that at least one action for state " << state << " stays within the selected state"); } } template void computeSchedulerWithOneSuccessorInStates(storm::storage::BitVector const& states, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::Scheduler& scheduler) { std::vector const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices(); for (auto const& state : states) { bool setValue = false; for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) { bool oneSuccessorInStates = false; for (auto const& element : transitionMatrix.getRow(choice)) { if (states.get(element.getColumn())) { oneSuccessorInStates = true; break; } } if (oneSuccessorInStates) { for (uint_fast64_t memState = 0; memState < scheduler.getNumberOfMemoryStates(); ++memState) { scheduler.setChoice(choice - nondeterministicChoiceIndices[state], state, memState); } setValue = true; break; } } STORM_LOG_ASSERT(setValue, "Expected that at least one action for state " << state << " leads with positive probability to the selected state"); } } template void computeSchedulerProbGreater0E(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::Scheduler& scheduler, boost::optional const& rowFilter) { //Perform backwards DFS from psiStates and find a valid choice for each visited state. std::vector stack; storm::storage::BitVector currentStates(psiStates); //the states that are either psiStates or for which we have found a valid choice. stack.insert(stack.end(), currentStates.begin(), currentStates.end()); uint_fast64_t currentState = 0; 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) { uint_fast64_t const& predecessor = predecessorEntryIt->getColumn(); if (phiStates.get(predecessor) && !currentStates.get(predecessor)) { //The predecessor is a probGreater0E state that has not been considered yet. Let's find the right choice that leads to a state in currentStates. bool foundValidChoice = false; for (uint_fast64_t row = transitionMatrix.getRowGroupIndices()[predecessor]; row < transitionMatrix.getRowGroupIndices()[predecessor + 1]; ++row) { if(rowFilter && !rowFilter->get(row)){ continue; } for (typename storm::storage::SparseMatrix::const_iterator successorEntryIt = transitionMatrix.begin(row), successorEntryIte = transitionMatrix.end(row); successorEntryIt != successorEntryIte; ++successorEntryIt) { if(currentStates.get(successorEntryIt->getColumn())){ foundValidChoice = true; break; } } if(foundValidChoice){ for (uint_fast64_t memState = 0; memState < scheduler.getNumberOfMemoryStates(); ++memState) { scheduler.setChoice(row - transitionMatrix.getRowGroupIndices()[predecessor], predecessor, memState); } currentStates.set(predecessor, true); stack.push_back(predecessor); break; } } STORM_LOG_INFO_COND(foundValidChoice, "Could not find a valid choice for ProbGreater0E state " << predecessor << "."); } } } } template void computeSchedulerProb0E(storm::storage::BitVector const& prob0EStates, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::Scheduler& scheduler) { computeSchedulerStayingInStates(prob0EStates, transitionMatrix, scheduler); } template void computeSchedulerRewInf(storm::storage::BitVector const& rewInfStates, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::Scheduler& scheduler) { computeSchedulerWithOneSuccessorInStates(rewInfStates, transitionMatrix, scheduler); } template void computeSchedulerProb1E(storm::storage::BitVector const& prob1EStates, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::Scheduler& scheduler, boost::optional const& rowFilter) { // set an arbitrary (valid) choice for the psi states. for (auto const& psiState : psiStates) { for (uint_fast64_t memState = 0; memState < scheduler.getNumberOfMemoryStates(); ++memState) { scheduler.setChoice(0, psiState, memState); } } // Now perform a backwards search from the psi states and store choices with prob. 1 std::vector const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices(); std::vector stack; storm::storage::BitVector currentStates(psiStates); stack.insert(stack.end(), currentStates.begin(), currentStates.end()); uint_fast64_t currentState = 0; 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()) && !currentStates.get(predecessorEntryIt->getColumn())) { // Check whether the predecessor has only successors in the prob1E state set for one of the // nondeterminstic choices. for (uint_fast64_t row = nondeterministicChoiceIndices[predecessorEntryIt->getColumn()]; row < nondeterministicChoiceIndices[predecessorEntryIt->getColumn() + 1]; ++row) { if (!rowFilter || rowFilter.get().get(row)) { bool allSuccessorsInProb1EStates = true; bool hasSuccessorInCurrentStates = false; for (typename storm::storage::SparseMatrix::const_iterator successorEntryIt = transitionMatrix.begin(row), successorEntryIte = transitionMatrix.end(row); successorEntryIt != successorEntryIte; ++successorEntryIt) { if (!prob1EStates.get(successorEntryIt->getColumn())) { allSuccessorsInProb1EStates = false; break; } else if (currentStates.get(successorEntryIt->getColumn())) { hasSuccessorInCurrentStates = true; } } // If all successors for a given nondeterministic choice are in the prob1E state set, we // perform a backward search from that state. if (allSuccessorsInProb1EStates && hasSuccessorInCurrentStates) { for (uint_fast64_t memState = 0; memState < scheduler.getNumberOfMemoryStates(); ++memState) { scheduler.setChoice(row - nondeterministicChoiceIndices[predecessorEntryIt->getColumn()], predecessorEntryIt->getColumn(), memState); } currentStates.set(predecessorEntryIt->getColumn(), true); stack.push_back(predecessorEntryIt->getColumn()); break; } } } } } } } template storm::storage::BitVector performProbGreater0E(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(); if (currentStepBound == 0) { continue; } } 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) { // 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; stepStack.push_back(currentStepBound - 1); } statesWithProbabilityGreater0.set(entryIt->getColumn(), true); stack.push_back(entryIt->getColumn()); } } } return statesWithProbabilityGreater0; } template storm::storage::BitVector performProb0A(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { storm::storage::BitVector statesWithProbability0 = performProbGreater0E(backwardTransitions, phiStates, psiStates); statesWithProbability0.complement(); return statesWithProbability0; } 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, boost::optional const& choiceConstraint) { 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) { if (!choiceConstraint || choiceConstraint.get().get(row)) { bool allSuccessorsInCurrentStates = true; bool hasNextStateSuccessor = false; 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; } else if (nextStates.get(successorEntryIt->getColumn())) { hasNextStateSuccessor = true; } } // 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 && hasNextStateSuccessor) { 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(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, boost::optional const& choiceConstraint) { 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(); if (currentStepBound == 0) { continue; } } for(typename storm::storage::SparseMatrix::const_iterator predecessorEntryIt = backwardTransitions.begin(currentState), predecessorEntryIte = backwardTransitions.end(currentState); predecessorEntryIt != predecessorEntryIte; ++predecessorEntryIt) { if (phiStates.get(predecessorEntryIt->getColumn())) { if (!statesWithProbabilityGreater0.get(predecessorEntryIt->getColumn())) { // Check whether the predecessor has at least one successor in the current state set for every // nondeterministic choice within the possibly given choiceConstraint. // Note: The backwards edge might be induced by a choice that violates the choiceConstraint. // However this is not problematic as long as there is at least one enabled choice for the predecessor. uint_fast64_t row = nondeterministicChoiceIndices[predecessorEntryIt->getColumn()]; uint_fast64_t const& endOfGroup = nondeterministicChoiceIndices[predecessorEntryIt->getColumn() + 1]; if (!choiceConstraint || choiceConstraint->getNextSetIndex(row) < endOfGroup) { bool addToStatesWithProbabilityGreater0 = true; for (; row < endOfGroup; ++row) { if (!choiceConstraint || choiceConstraint->get(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) { // 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; stepStack.push_back(currentStepBound - 1); } statesWithProbabilityGreater0.set(predecessorEntryIt->getColumn(), true); stack.push_back(predecessorEntryIt->getColumn()); } } } else if (useStepBound && remainingSteps[predecessorEntryIt->getColumn()] < currentStepBound - 1) { // We have found a shorter path to the predecessor. Hence, we need to explore it again. // If there is a choiceConstraint, we still need to check whether the backwards edge was induced by a valid action bool predecessorIsValid = true; if (choiceConstraint) { predecessorIsValid = false; uint_fast64_t row = choiceConstraint->getNextSetIndex(nondeterministicChoiceIndices[predecessorEntryIt->getColumn()]); uint_fast64_t const& endOfGroup = nondeterministicChoiceIndices[predecessorEntryIt->getColumn() + 1]; for (; row < endOfGroup && !predecessorIsValid; row = choiceConstraint->getNextSetIndex(row + 1)) { for (auto const& entry : transitionMatrix.getRow(row)) { if (entry.getColumn() == currentState) { predecessorIsValid = true; break; } } } } if (predecessorIsValid) { remainingSteps[predecessorEntryIt->getColumn()] = currentStepBound - 1; stepStack.push_back(currentStepBound - 1); stack.push_back(predecessorEntryIt->getColumn()); } } } } } 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::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { return performProb1A(model.getTransitionMatrix(), model.getNondeterministicChoiceIndices(), backwardTransitions, phiStates, 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) { 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 computeSchedulerProbGreater0E(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 statesWithProbabilityGreater0E = manager.getBddZero(); storm::dd::Bdd frontier = psiStates; storm::dd::Bdd scheduler = manager.getBddZero(); uint_fast64_t iterations = 0; while (!frontier.isZero()) { storm::dd::Bdd statesAndChoicesWithProbabilityGreater0E = frontier.inverseRelationalProductWithExtendedRelation(transitionMatrix, model.getRowVariables(), model.getColumnVariables()); frontier = phiStates && statesAndChoicesWithProbabilityGreater0E.existsAbstract(model.getNondeterminismVariables()) && !statesWithProbabilityGreater0E; scheduler = scheduler || (frontier && statesAndChoicesWithProbabilityGreater0E).existsAbstractRepresentative(model.getNondeterminismVariables()); statesWithProbabilityGreater0E |= frontier; ++iterations; } return scheduler; } 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.inverseRelationalProduct(abstractedTransitionMatrix, model.getRowVariables(), 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.inverseRelationalProductWithExtendedRelation(transitionMatrix, model.getRowVariables(), 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& 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.inverseRelationalProductWithExtendedRelation(transitionMatrix, model.getRowVariables(), model.getColumnVariables()); temporary = temporary.andExists(temporary2, model.getNondeterminismVariables()); temporary &= phiStates; temporary |= psiStates; if (innerStates == temporary) { innerLoopDone = true; } else { innerStates = temporary; } } if (statesWithProbability1E == innerStates) { outerLoopDone = true; } else { statesWithProbability1E = innerStates; } ++iterations; } return statesWithProbability1E; } template storm::dd::Bdd computeSchedulerProb1E(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& statesWithProbability1E) { // Initialize environment for backward search. storm::dd::DdManager const& manager = model.getManager(); storm::dd::Bdd scheduler = manager.getBddZero(); storm::dd::Bdd innerStates = manager.getBddZero(); uint64_t iterations = 0; 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.inverseRelationalProductWithExtendedRelation(transitionMatrix, model.getRowVariables(), model.getColumnVariables()); temporary &= temporary2; temporary &= phiStates; // Extend the scheduler for those states that have not been seen as inner states before. scheduler |= (temporary && !innerStates).existsAbstractRepresentative(model.getNondeterminismVariables()); temporary = temporary.existsAbstract(model.getNondeterminismVariables()); temporary |= psiStates; if (innerStates == temporary) { innerLoopDone = true; } else { innerStates = temporary; } ++iterations; } return scheduler; } template std::pair, storm::dd::Bdd> performProb01Max(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { return performProb01Max(model, model.getTransitionMatrix().notZero(), phiStates, psiStates); } template std::pair, storm::dd::Bdd> performProb01Max(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { std::pair, storm::dd::Bdd> result; 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) { return performProb01Min(model, model.getTransitionMatrix().notZero(), phiStates, psiStates); } template std::pair, storm::dd::Bdd> performProb01Min(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { std::pair, storm::dd::Bdd> result; result.first = performProb0E(model, transitionMatrix, phiStates, psiStates); result.second = performProb1A(model, transitionMatrix, psiStates, !result.first && model.getReachableStates()); return result; } template ExplicitGameProb01Result performProb0(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1Groups, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::ExplicitGameStrategyPair* strategyPair) { ExplicitGameProb01Result result(psiStates, storm::storage::BitVector(transitionMatrix.getRowGroupCount())); // Initialize the stack used for the DFS with the states std::vector stack(psiStates.begin(), psiStates.end()); // Perform the actual DFS. uint_fast64_t currentState; while (!stack.empty()) { currentState = stack.back(); stack.pop_back(); // Check which player 2 predecessors of the current player 1 state to add. for (auto const& player2PredecessorEntry : player1BackwardTransitions.getRow(currentState)) { uint64_t player2Predecessor = player2PredecessorEntry.getColumn(); if (!result.player2States.get(player2Predecessor)) { bool addPlayer2State = false; if (player2Direction == OptimizationDirection::Minimize) { bool allChoicesHavePlayer1State = true; for (uint64_t row = transitionMatrix.getRowGroupIndices()[player2Predecessor]; row < transitionMatrix.getRowGroupIndices()[player2Predecessor + 1]; ++row) { bool choiceHasPlayer1State = false; for (auto const& entry : transitionMatrix.getRow(row)) { if (result.player1States.get(entry.getColumn())) { choiceHasPlayer1State = true; break; } } if (!choiceHasPlayer1State) { allChoicesHavePlayer1State = false; } } if (allChoicesHavePlayer1State) { addPlayer2State = true; } } else { addPlayer2State = true; } if (addPlayer2State) { result.player2States.set(player2Predecessor); // Now check whether adding the player 2 state changes something with respect to the // (single) player 1 predecessor. uint64_t player1Predecessor = player2BackwardTransitions[player2Predecessor]; if (!result.player1States.get(player1Predecessor)) { bool addPlayer1State = false; if (player1Direction == OptimizationDirection::Minimize) { bool allPlayer2Successors = true; for (uint64_t player2State = player1Groups[player1Predecessor]; player2State < player1Groups[player1Predecessor + 1]; ++player2State) { if (!result.player2States.get(player2State)) { allPlayer2Successors = false; break; } } if (allPlayer2Successors) { addPlayer1State = true; } } else { addPlayer1State = true; } if (addPlayer1State) { result.player1States.set(player1Predecessor); stack.emplace_back(player1Predecessor); } } } } } } // Since we have determined the complements of the desired sets, we need to complement it now. result.player1States.complement(); result.player2States.complement(); // Generate player 1 strategy if required. if (strategyPair) { for (auto player1State : result.player1States) { if (player1Direction == storm::OptimizationDirection::Minimize) { // At least one player 2 successor is a state with probability 0, find it. bool foundProb0Successor = false; uint64_t player2State; for (player2State = player1Groups[player1State]; player2State < player1Groups[player1State + 1]; ++player2State) { if (result.player2States.get(player2State)) { foundProb0Successor = true; break; } } STORM_LOG_ASSERT(foundProb0Successor, "Expected at least one state 2 successor with probability 0."); strategyPair->getPlayer1Strategy().setChoice(player1State, player2State); } else { // Since all player 2 successors are states with probability 0, just pick any. strategyPair->getPlayer1Strategy().setChoice(player1State, player1Groups[player1State]); } } } // Generate player 2 strategy if required. if (strategyPair) { for (auto player2State : result.player2States) { if (player2Direction == storm::OptimizationDirection::Minimize) { // At least one distribution only has successors with probability 0, find it. bool foundProb0SuccessorDistribution = false; uint64_t row; for (row = transitionMatrix.getRowGroupIndices()[player2State]; row < transitionMatrix.getRowGroupIndices()[player2State + 1]; ++row) { bool distributionHasOnlyProb0Successors = true; for (auto const& player1SuccessorEntry : transitionMatrix.getRow(row)) { if (!result.player1States.get(player1SuccessorEntry.getColumn())) { distributionHasOnlyProb0Successors = false; break; } } if (distributionHasOnlyProb0Successors) { foundProb0SuccessorDistribution = true; break; } } STORM_LOG_ASSERT(foundProb0SuccessorDistribution, "Expected at least one distribution with only successors with probability 0."); strategyPair->getPlayer2Strategy().setChoice(player2State, row); } else { // Since all player 1 successors are states with probability 0, just pick any. strategyPair->getPlayer2Strategy().setChoice(player2State, transitionMatrix.getRowGroupIndices()[player2State]); } } } return result; } template SymbolicGameProb01Result performProb0(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy) { // The solution sets. storm::dd::Bdd player1States = psiStates; storm::dd::Bdd player2States = model.getManager().getBddZero(); bool done = false; uint_fast64_t iterations = 0; while (!done) { storm::dd::Bdd tmp = (transitionMatrix && player1States.swapVariables(model.getRowColumnMetaVariablePairs())).existsAbstract(model.getColumnVariables()) && phiStates; if (player2Strategy == OptimizationDirection::Minimize) { tmp = (tmp || model.getIllegalPlayer2Mask()).universalAbstract(model.getPlayer2Variables()); } else { tmp = tmp.existsAbstract(model.getPlayer2Variables()); } player2States |= tmp; if (player1Strategy == OptimizationDirection::Minimize) { tmp = (tmp || model.getIllegalPlayer1Mask()).universalAbstract(model.getPlayer1Variables()); } else { tmp = tmp.existsAbstract(model.getPlayer1Variables()); } // Re-add all previous player 1 states. tmp |= player1States; if (tmp == player1States) { done = true; } player1States = tmp; ++iterations; } // Since we have determined the complements of the desired sets, we need to complement it now. player1States = !player1States && model.getReachableStates(); std::set variablesToAbstract(model.getColumnVariables()); variablesToAbstract.insert(model.getPlayer2Variables().begin(), model.getPlayer2Variables().end()); player2States = !player2States && transitionMatrix.existsAbstract(variablesToAbstract); // Determine all transitions between prob0 states. storm::dd::Bdd transitionsBetweenProb0States = player2States && (transitionMatrix && player1States.swapVariables(model.getRowColumnMetaVariablePairs())); // Determine the distributions that have only successors that are prob0 states. storm::dd::Bdd onlyProb0Successors = (transitionsBetweenProb0States || model.getIllegalSuccessorMask()).universalAbstract(model.getColumnVariables()); boost::optional> player2StrategyBdd; if (producePlayer2Strategy) { // Pick a distribution that has only prob0 successors. player2StrategyBdd = onlyProb0Successors.existsAbstractRepresentative(model.getPlayer2Variables()); } boost::optional> player1StrategyBdd; if (producePlayer1Strategy) { // Move from player 2 choices with only prob0 successors to player 1 choices with only prob 0 successors. onlyProb0Successors = (player1States && onlyProb0Successors).existsAbstract(model.getPlayer2Variables()); // Pick a prob0 player 2 state. player1StrategyBdd = onlyProb0Successors.existsAbstractRepresentative(model.getPlayer1Variables()); } return SymbolicGameProb01Result(player1States, player2States, player1StrategyBdd, player2StrategyBdd); } template ExplicitGameProb01Result performProb1(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1Groups, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::ExplicitGameStrategyPair* strategyPair, boost::optional const& player1Candidates) { // During the execution, the two state sets in the result hold the potential player 1/2 states. ExplicitGameProb01Result result; if (player1Candidates) { result = ExplicitGameProb01Result(player1Candidates.get(), storm::storage::BitVector(transitionMatrix.getRowGroupCount())); } else { result = ExplicitGameProb01Result(storm::storage::BitVector(phiStates.size(), true), storm::storage::BitVector(transitionMatrix.getRowGroupCount())); } // A flag that governs whether strategies are produced in the current iteration. bool produceStrategiesInIteration = false; // Initialize the stack used for the DFS with the states std::vector stack; bool maybeStatesDone = false; uint_fast64_t maybeStateIterations = 0; while (!maybeStatesDone || produceStrategiesInIteration) { storm::storage::BitVector player1Solution = psiStates; storm::storage::BitVector player2Solution(result.player2States.size()); stack.clear(); stack.insert(stack.end(), psiStates.begin(), psiStates.end()); // Perform the actual DFS. uint_fast64_t currentState; while (!stack.empty()) { currentState = stack.back(); stack.pop_back(); for (auto player2PredecessorEntry : player1BackwardTransitions.getRow(currentState)) { uint64_t player2Predecessor = player2PredecessorEntry.getColumn(); if (!player2Solution.get(player2PredecessorEntry.getColumn())) { bool addPlayer2State = player2Direction == storm::OptimizationDirection::Minimize ? true : false; uint64_t validChoice = transitionMatrix.getRowGroupIndices()[player2Predecessor]; for (uint64_t row = validChoice; row < transitionMatrix.getRowGroupIndices()[player2Predecessor + 1]; ++row) { bool choiceHasSolutionSuccessor = false; bool choiceStaysInMaybeStates = true; for (auto const& entry : transitionMatrix.getRow(row)) { if (player1Solution.get(entry.getColumn())) { choiceHasSolutionSuccessor = true; } if (!result.player1States.get(entry.getColumn())) { choiceStaysInMaybeStates = false; break; } } if (choiceHasSolutionSuccessor && choiceStaysInMaybeStates) { if (player2Direction == storm::OptimizationDirection::Maximize) { validChoice = row; addPlayer2State = true; break; } } else if (player2Direction == storm::OptimizationDirection::Minimize) { addPlayer2State = false; break; } } if (addPlayer2State) { player2Solution.set(player2Predecessor); if (produceStrategiesInIteration) { strategyPair->getPlayer2Strategy().setChoice(player2Predecessor, validChoice); } // Check whether the addition of the player 2 state changes the state of the (single) // player 1 predecessor. uint64_t player1Predecessor = player2BackwardTransitions[player2Predecessor]; if (!player1Solution.get(player1Predecessor)) { bool addPlayer1State = player1Direction == storm::OptimizationDirection::Minimize ? true : false; validChoice = player1Groups[player1Predecessor]; for (uint64_t player2Successor = validChoice; player2Successor < player1Groups[player1Predecessor + 1]; ++player2Successor) { if (player2Solution.get(player2Successor)) { if (player1Direction == storm::OptimizationDirection::Maximize) { validChoice = player2Successor; addPlayer1State = true; break; } } else if (player1Direction == storm::OptimizationDirection::Minimize) { addPlayer1State = false; break; } } if (addPlayer1State) { player1Solution.set(player1Predecessor); if (produceStrategiesInIteration) { strategyPair->getPlayer1Strategy().setChoice(player1Predecessor, validChoice); } stack.emplace_back(player1Predecessor); } } } } } } if (result.player1States == player1Solution) { maybeStatesDone = true; result.player2States = player2Solution; // If we were asked to produce strategies, we propagate that by triggering another iteration. // We only do this if at least one strategy will be produced. produceStrategiesInIteration = !produceStrategiesInIteration && strategyPair; } else { result.player1States = player1Solution; result.player2States = player2Solution; } ++maybeStateIterations; } return result; } template SymbolicGameProb01Result performProb1(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy, boost::optional> const& player1Candidates) { // Create the potential prob1 states of player 1. storm::dd::Bdd maybePlayer1States = model.getReachableStates(); if (player1Candidates) { maybePlayer1States &= player1Candidates.get(); } // Initialize potential prob1 states of player 2. storm::dd::Bdd maybePlayer2States = model.getManager().getBddZero(); // A flag that governs whether strategies are produced in the current iteration. bool produceStrategiesInIteration = false; boost::optional> player1StrategyBdd; boost::optional> consideredPlayer1States; boost::optional> player2StrategyBdd; boost::optional> consideredPlayer2States; bool maybeStatesDone = false; uint_fast64_t maybeStateIterations = 0; while (!maybeStatesDone || produceStrategiesInIteration) { bool solutionStatesDone = false; uint_fast64_t solutionStateIterations = 0; // If we are to produce strategies in this iteration, we prepare some storage. if (produceStrategiesInIteration) { if (player1Strategy == storm::OptimizationDirection::Maximize) { player1StrategyBdd = model.getManager().getBddZero(); consideredPlayer1States = model.getManager().getBddZero(); } if (player2Strategy == storm::OptimizationDirection::Maximize) { player2StrategyBdd = model.getManager().getBddZero(); consideredPlayer2States = model.getManager().getBddZero(); } } storm::dd::Bdd player1Solution = psiStates; storm::dd::Bdd player2Solution = model.getManager().getBddZero(); while (!solutionStatesDone) { // Start by computing the transitions that have only maybe states as successors. Note that at // this point, there may be illegal transitions. storm::dd::Bdd distributionsStayingInMaybe = (!transitionMatrix || maybePlayer1States.swapVariables(model.getRowColumnMetaVariablePairs())).universalAbstract(model.getColumnVariables()); // Then, determine all distributions that have at least one successor in the states that have // probability 1. storm::dd::Bdd distributionsWithProb1Successor = (transitionMatrix && player1Solution.swapVariables(model.getRowColumnMetaVariablePairs())).existsAbstract(model.getColumnVariables()); // The valid distributions are then those that emanate from phi states, stay completely in the // maybe states and have at least one successor with probability 1. storm::dd::Bdd valid = phiStates && distributionsStayingInMaybe && distributionsWithProb1Successor; // Depending on the strategy of player 2, we need to check whether all choices are valid or // there exists a valid choice. if (player2Strategy == OptimizationDirection::Minimize) { valid = (valid || model.getIllegalPlayer2Mask()).universalAbstract(model.getPlayer2Variables()); } else { if (produceStrategiesInIteration) { storm::dd::Bdd newValidDistributions = valid && !consideredPlayer2States.get(); player2StrategyBdd.get() = player2StrategyBdd.get() || newValidDistributions.existsAbstractRepresentative(model.getPlayer2Variables()); } valid = valid.existsAbstract(model.getPlayer2Variables()); if (produceStrategiesInIteration) { consideredPlayer2States.get() |= valid; } } player2Solution |= valid; // And do the same for player 1. if (player1Strategy == OptimizationDirection::Minimize) { valid = (valid || model.getIllegalPlayer1Mask()).universalAbstract(model.getPlayer1Variables()); } else { if (produceStrategiesInIteration) { storm::dd::Bdd newValidDistributions = valid && !consideredPlayer1States.get(); player1StrategyBdd.get() = player1StrategyBdd.get() || newValidDistributions.existsAbstractRepresentative(model.getPlayer1Variables()); } valid = valid.existsAbstract(model.getPlayer1Variables()); if (produceStrategiesInIteration) { consideredPlayer1States.get() |= valid; } } // Explicitly add psi states to result since they may have transitions going to some state that // does not have a reachability probability of 1. valid |= psiStates; // If no new states were added, we have found the current hypothesis for the states with // probability 1. if (valid == player1Solution) { solutionStatesDone = true; } else { player1Solution = valid; } ++solutionStateIterations; } // If the states with probability 1 and the potential probability 1 states coincide, we have found // the solution. if (player1Solution == maybePlayer1States) { maybePlayer2States = player2Solution; maybeStatesDone = true; // If we were asked to produce strategies, we propagate that by triggering another iteration. // We only do this if at least one strategy will be produced. produceStrategiesInIteration = !produceStrategiesInIteration && ((producePlayer1Strategy && player1Strategy == OptimizationDirection::Maximize) || (producePlayer2Strategy && player2Strategy == OptimizationDirection::Maximize)); } else { // Otherwise, we use the current hypothesis for the states with probability 1 as the new maybe // state set. maybePlayer1States = player1Solution; } ++maybeStateIterations; } // From now on, the solution is stored in maybeStates (as it coincides with the previous solution). // If we were asked to produce strategies that do not need to pick a certain successor but are // 'arbitrary', do so now. bool strategiesToCompute = (producePlayer1Strategy && !player1StrategyBdd) || (producePlayer2Strategy && !player2StrategyBdd); if (strategiesToCompute) { storm::dd::Bdd relevantStates = (transitionMatrix && maybePlayer2States).existsAbstract(model.getColumnVariables()); if (producePlayer2Strategy && !player2StrategyBdd) { player2StrategyBdd = relevantStates.existsAbstractRepresentative(model.getPlayer2Variables()); } if (producePlayer1Strategy && !player1StrategyBdd) { relevantStates = (maybePlayer1States && relevantStates).existsAbstract(model.getPlayer2Variables()); player1StrategyBdd = relevantStates.existsAbstractRepresentative(model.getPlayer1Variables()); } } return SymbolicGameProb01Result(maybePlayer1States, maybePlayer2States, player1StrategyBdd, player2StrategyBdd); } template void topologicalSortHelper(storm::storage::SparseMatrix const& matrix, uint64_t state, std::vector& topologicalSort, std::vector& recursionStack, std::vector::const_iterator>& iteratorRecursionStack, storm::storage::BitVector& visitedStates) { 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; } } } } template std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix, std::vector const& firstStates) { if (matrix.getRowCount() != matrix.getColumnCount()) { STORM_LOG_ERROR("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 (auto const state : firstStates ) { topologicalSortHelper(matrix, state, topologicalSort, recursionStack, iteratorRecursionStack, visitedStates); } for (uint_fast64_t state = 0; state < numberOfStates; ++state) { topologicalSortHelper(matrix, state, topologicalSort, recursionStack, iteratorRecursionStack, visitedStates); } return topologicalSort; } 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, bool useStepBound, uint_fast64_t maximalSteps, boost::optional const& choiceFilter); template storm::storage::BitVector getBsccCover(storm::storage::SparseMatrix const& transitionMatrix); template bool hasCycle(storm::storage::SparseMatrix const& transitionMatrix, boost::optional const& subsystem); template bool checkIfECWithChoiceExists(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& choices); template std::vector getDistances(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, boost::optional const& subsystem); 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 void computeSchedulerProbGreater0E(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::Scheduler& scheduler, boost::optional const& rowFilter); template void computeSchedulerProb0E(storm::storage::BitVector const& prob0EStates, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::Scheduler& scheduler); template void computeSchedulerRewInf(storm::storage::BitVector const& rewInfStates, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::Scheduler& scheduler); template void computeSchedulerProb1E(storm::storage::BitVector const& prob1EStates, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::Scheduler& scheduler, boost::optional const& rowFilter = boost::none); template storm::storage::BitVector performProbGreater0E(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& 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, boost::optional const& choiceConstraint = boost::none); 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, boost::optional const& choiceConstraint = boost::none); 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); #ifdef STORM_HAVE_CARL template storm::storage::BitVector performProb0E(storm::models::sparse::NondeterministicModel