From b418782bcd49aedb352b6ee47544b5eec4c2e552 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 31 Aug 2015 11:23:04 +0200 Subject: [PATCH] added missing header Former-commit-id: b3b4deddb7068c929630727beb47d5e738c3c578 --- src/utility/graph.cpp | 220 +++++++++++++++++++++--------------------- src/utility/solver.h | 1 + 2 files changed, 111 insertions(+), 110 deletions(-) diff --git a/src/utility/graph.cpp b/src/utility/graph.cpp index b775c5b14..3e12abcd2 100644 --- a/src/utility/graph.cpp +++ b/src/utility/graph.cpp @@ -26,7 +26,7 @@ namespace storm { namespace utility { namespace graph { - template + template storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates) { storm::storage::BitVector reachableStates(initialStates); @@ -59,7 +59,7 @@ namespace storm { return reachableStates; } - template + template std::vector getDistances(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates) { std::vector distances(transitionMatrix.getRowGroupCount()); @@ -90,7 +90,7 @@ namespace storm { return distances; } - template + 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(); @@ -146,14 +146,14 @@ namespace storm { return statesWithProbabilityGreater0; } - template + template storm::storage::BitVector performProb1(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector const& statesWithProbabilityGreater0) { storm::storage::BitVector statesWithProbability1 = performProbGreater0(backwardTransitions, ~psiStates, ~statesWithProbabilityGreater0); statesWithProbability1.complement(); return statesWithProbability1; } - template + 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)); @@ -161,7 +161,7 @@ namespace storm { return statesWithProbability1; } - template + 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(); @@ -171,7 +171,7 @@ namespace storm { return result; } - template + 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); @@ -180,7 +180,7 @@ namespace storm { return result; } - template + 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(); @@ -201,24 +201,24 @@ namespace storm { statesWithProbabilityGreater0 |= lastIterationStates; ++iterations; } - + return statesWithProbabilityGreater0; } - template + template storm::dd::Bdd performProb1(storm::models::symbolic::Model const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0) { storm::dd::Bdd statesWithProbability1 = performProbGreater0(model, transitionMatrix, !psiStates && model.getReachableStates(), !statesWithProbabilityGreater0 && model.getReachableStates()); statesWithProbability1 = !statesWithProbability1 && model.getReachableStates(); return statesWithProbability1; } - template + 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 + 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(); @@ -228,7 +228,7 @@ namespace storm { return result; } - template + template std::pair, storm::dd::Bdd> performProb01(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { std::pair, storm::dd::Bdd> result; storm::dd::Bdd transitionMatrixBdd = transitionMatrix.notZero(); @@ -238,7 +238,7 @@ namespace storm { return result; } - template + template storm::storage::BitVector performProbGreater0E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound, uint_fast64_t maximalSteps) { size_t numberOfStates = phiStates.size(); @@ -301,12 +301,12 @@ namespace storm { return statesWithProbability0; } - template + template storm::storage::BitVector performProb0A(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { return performProb0A(model.getTransitionMatrix(), model.getNondeterministicChoiceIndices(), backwardTransitions, phiStates, psiStates); } - - template + + template storm::storage::BitVector performProb1E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { size_t numberOfStates = phiStates.size(); @@ -364,7 +364,7 @@ namespace storm { return currentStates; } - template + 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); } @@ -377,13 +377,13 @@ namespace storm { result.second = performProb1E(transitionMatrix, nondeterministicChoiceIndices, backwardTransitions, phiStates, psiStates); return result; } - - template + + 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 + template storm::storage::BitVector performProbGreater0A(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound, uint_fast64_t maximalSteps) { size_t numberOfStates = phiStates.size(); @@ -460,13 +460,13 @@ namespace storm { return statesWithProbabilityGreater0; } - template + 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); @@ -474,7 +474,7 @@ namespace storm { return statesWithProbability0; } - template + 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(); @@ -548,19 +548,19 @@ namespace storm { result.second = performProb1A(transitionMatrix, nondeterministicChoiceIndices, backwardTransitions, phiStates, psiStates); return result; } - - template + + 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 + 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) { @@ -571,16 +571,16 @@ namespace storm { statesWithProbabilityGreater0E |= lastIterationStates; ++iterations; } - + return statesWithProbabilityGreater0E; } - template + 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 + 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(); @@ -602,12 +602,12 @@ namespace storm { return statesWithProbabilityGreater0A; } - template + 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 + template storm::dd::Bdd performProb1A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0A) { // Initialize environment for backward search. storm::dd::DdManager const& manager = model.getManager(); @@ -629,12 +629,12 @@ namespace storm { return statesWithProbability1A; } - template + 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) { @@ -666,7 +666,7 @@ namespace storm { } ++iterations; } - + return statesWithProbability1E; } @@ -688,13 +688,13 @@ namespace storm { return result; } - template + 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. @@ -725,10 +725,10 @@ namespace storm { 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()); + recursionStack.push_back(successorIterator->getColumn()); // Also, put initial value for iterator on corresponding recursion stack. - iteratorRecursionStack.push_back(matrix.begin(successorIterator->getColumn())); + iteratorRecursionStack.push_back(matrix.begin(successorIterator->getColumn())); goto recursionStepForward; } @@ -759,7 +759,7 @@ namespace storm { - template + template std::pair, std::vector> performDijkstra(storm::models::sparse::Model const& model, storm::storage::SparseMatrix const& transitions, storm::storage::BitVector const& startingStates, @@ -767,13 +767,13 @@ namespace storm { LOG4CPLUS_INFO(logger, "Performing Dijkstra search."); - const uint_fast64_t noPredecessorValue = storm::utility::zero(); + const uint_fast64_t noPredecessorValue = storm::utility::zero(); std::vector probabilities(model.getNumberOfStates(), storm::utility::zero()); std::vector predecessors(model.getNumberOfStates(), noPredecessorValue); // Set the probability to 1 for all starting states. std::set, DistanceCompare> probabilityStateSet; - + for (auto state : startingStates) { probabilityStateSet.emplace(storm::utility::one(), state); probabilities[state] = storm::utility::one(); @@ -790,7 +790,7 @@ namespace storm { // Only follow the transition if it lies within the filtered states. if (filterStates != nullptr && filterStates->get(transition.first)) { // Calculate the distance we achieve when we take the path to the successor via the current state. - T newDistance = probabilityStatePair.first; + T newDistance = probabilityStatePair.first; // We found a cheaper way to get to the target state of the transition. if (newDistance > probabilities[transition.first]) { // Remove the old distance. @@ -817,209 +817,209 @@ namespace storm { - + template storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates); - + template std::vector getDistances(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates); - + template storm::storage::BitVector performProbGreater0(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0); - + template storm::storage::BitVector performProb1(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector const& statesWithProbabilityGreater0); - + template storm::storage::BitVector performProb1(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - + template std::pair performProb01(storm::models::sparse::DeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - + template std::pair performProb01(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - + template storm::storage::BitVector performProbGreater0E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) ; template storm::storage::BitVector performProb0A(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); template storm::storage::BitVector performProb0A(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; - + template storm::storage::BitVector performProb1E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - + template storm::storage::BitVector performProb1E(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); template std::pair performProb01Max(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; - - + + template std::pair performProb01Max(storm::models::sparse::NondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; - + template storm::storage::BitVector performProbGreater0A(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0); - + template storm::storage::BitVector performProb0E(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); template storm::storage::BitVector performProb0E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; - + template storm::storage::BitVector performProb1A( storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); template std::pair performProb01Min(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; - - + + template std::pair performProb01Min(storm::models::sparse::NondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); template std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix) ; - + template storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates); - + template std::vector getDistances(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates); - + template storm::storage::BitVector performProbGreater0(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0); - + template storm::storage::BitVector performProb1(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector const& statesWithProbabilityGreater0); - + template storm::storage::BitVector performProb1(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - + template std::pair performProb01(storm::models::sparse::DeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - + template std::pair performProb01(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - + template storm::storage::BitVector performProbGreater0E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) ; template storm::storage::BitVector performProb0A(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); template storm::storage::BitVector performProb0A(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; - + template storm::storage::BitVector performProb1E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - + template storm::storage::BitVector performProb1E(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); template std::pair performProb01Max(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; - - + + template std::pair performProb01Max(storm::models::sparse::NondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; - + template storm::storage::BitVector performProbGreater0A(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0); - + template storm::storage::BitVector performProb0E(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); template storm::storage::BitVector performProb0E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; - + template storm::storage::BitVector performProb1A( storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); template std::pair performProb01Min(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; - - + + template std::pair performProb01Min(storm::models::sparse::NondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); template std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix) ; #ifdef STORM_HAVE_CARL - - + + template storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates); - + template std::vector getDistances(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates); - + template storm::storage::BitVector performProbGreater0(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0); - + template storm::storage::BitVector performProb1(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector const& statesWithProbabilityGreater0); - + template storm::storage::BitVector performProb1(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - + template std::pair performProb01(storm::models::sparse::DeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - + template std::pair performProb01(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - + template storm::storage::BitVector performProbGreater0E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) ; template storm::storage::BitVector performProb0A(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); template storm::storage::BitVector performProb0A(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; - + template storm::storage::BitVector performProb1E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - + template storm::storage::BitVector performProb1E(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); template std::pair performProb01Max(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; - - + + template std::pair performProb01Max(storm::models::sparse::NondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; - + template storm::storage::BitVector performProbGreater0A(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0); - + template storm::storage::BitVector performProb0E(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); template storm::storage::BitVector performProb0E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; - + template storm::storage::BitVector performProb1A( storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); template std::pair performProb01Min(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; - - + + template std::pair performProb01Min(storm::models::sparse::NondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); template std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix) ; - -#endif - +#endif + + template storm::dd::Bdd performProbGreater0(storm::models::symbolic::Model const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, boost::optional const& stepBound = boost::optional()); - + template storm::dd::Bdd performProb1(storm::models::symbolic::Model const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0); - + template storm::dd::Bdd performProb1(storm::models::symbolic::Model const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) ; - + template std::pair, storm::dd::Bdd> performProb01(storm::models::symbolic::DeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); - + template std::pair, storm::dd::Bdd> performProb01(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); template storm::dd::Bdd performProbGreater0E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); - + template storm::dd::Bdd performProb0A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) ; - + template storm::dd::Bdd performProbGreater0A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) ; - + template storm::dd::Bdd performProb0E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) ; - + template storm::dd::Bdd performProb1A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0A); - + template storm::dd::Bdd performProb1E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0E) ; - + template std::pair, storm::dd::Bdd> performProb01Max(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) ; template std::pair, storm::dd::Bdd> performProb01Min(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) ; - + } // namespace graph } // namespace utility diff --git a/src/utility/solver.h b/src/utility/solver.h index f112f9a99..e18f435d6 100644 --- a/src/utility/solver.h +++ b/src/utility/solver.h @@ -3,6 +3,7 @@ #include #include +#include #include "src/storage/dd/DdType.h" #include "src/solver/SolverSelectionOptions.h"