diff --git a/src/modelchecker/SparseMdpPrctlModelChecker.h b/src/modelchecker/SparseMdpPrctlModelChecker.h index 0c951ae8f..f76092cd2 100644 --- a/src/modelchecker/SparseMdpPrctlModelChecker.h +++ b/src/modelchecker/SparseMdpPrctlModelChecker.h @@ -360,9 +360,9 @@ public: storm::storage::BitVector infinityStates; storm::storage::BitVector trueStates(this->getModel().getNumberOfStates(), true); if (this->minimumOperatorStack.top()) { - infinityStates = storm::utility::GraphAnalyzer::performProb1A(this->getModel(), trueStates, *targetStates); + infinityStates = storm::utility::GraphAnalyzer::performProb1A(this->getModel(), this->getModel().getBackwardTransitions(), trueStates, *targetStates); } else { - infinityStates = storm::utility::GraphAnalyzer::performProb1E(this->getModel(), trueStates, *targetStates); + infinityStates = storm::utility::GraphAnalyzer::performProb1E(this->getModel(), this->getModel().getBackwardTransitions(), trueStates, *targetStates); } infinityStates.complement(); diff --git a/src/utility/GraphAnalyzer.h b/src/utility/GraphAnalyzer.h index 577bccf74..b3eab9727 100644 --- a/src/utility/GraphAnalyzer.h +++ b/src/utility/GraphAnalyzer.h @@ -139,8 +139,12 @@ public: template static std::pair performProb01Max(storm::models::AbstractNondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { std::pair result; - result.first = GraphAnalyzer::performProb0A(model, phiStates, psiStates); - result.second = GraphAnalyzer::performProb1E(model, phiStates, psiStates); + + // Get the backwards transition relation from the model to ease the search. + storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); + + result.first = GraphAnalyzer::performProb0A(model, backwardTransitions, phiStates, psiStates); + result.second = GraphAnalyzer::performProb1E(model, backwardTransitions, phiStates, psiStates); return result; } @@ -151,17 +155,15 @@ public: * scheduler tries to maximize this probability. * * @param model The model whose graph structure to search. + * @param backwardTransitions The reversed transition relation of the model. * @param phiStates The set of all states satisfying phi. * @param psiStates The set of all states satisfying psi. * @return A bit vector that represents all states with probability 0. */ template - static storm::storage::BitVector performProb0A(storm::models::AbstractNondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + static storm::storage::BitVector performProb0A(storm::models::AbstractNondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { // Prepare the resulting bit vector. storm::storage::BitVector statesWithProbability0(model.getNumberOfStates()); - - // Get the backwards transition relation from the model to ease the search. - storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); // Add all psi states as the already satisfy the condition. statesWithProbability0 |= psiStates; @@ -196,19 +198,17 @@ public: * scheduler tries to maximize this probability. * * @param model The model whose graph structure to search. + * @param backwardTransitions The reversed transition relation of the model. * @param phiStates The set of all states satisfying phi. * @param psiStates The set of all states satisfying psi. * @return A bit vector that represents all states with probability 1. */ template - static storm::storage::BitVector performProb1E(storm::models::AbstractNondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + static storm::storage::BitVector performProb1E(storm::models::AbstractNondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { // Get some temporaries for convenience. std::shared_ptr> transitionMatrix = model.getTransitionMatrix(); std::shared_ptr> nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices(); - // Get the backwards transition relation from the model to ease the search. - storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); - storm::storage::BitVector currentStates(model.getNumberOfStates(), true); std::vector stack; @@ -274,8 +274,12 @@ public: template static std::pair performProb01Min(storm::models::AbstractNondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { std::pair result; - result.first = GraphAnalyzer::performProb0E(model, phiStates, psiStates); - result.second = GraphAnalyzer::performProb1A(model, phiStates, psiStates); + + // Get the backwards transition relation from the model to ease the search. + storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); + + result.first = GraphAnalyzer::performProb0E(model, backwardTransitions, phiStates, psiStates); + result.second = GraphAnalyzer::performProb1A(model, backwardTransitions, phiStates, psiStates); return result; } @@ -286,12 +290,13 @@ public: * scheduler tries to minimize this probability. * * @param model The model whose graph structure to search. + * @param backwardTransitions The reversed transition relation of the model. * @param phiStates The set of all states satisfying phi. * @param psiStates The set of all states satisfying psi. * @return A bit vector that represents all states with probability 0. */ template - static storm::storage::BitVector performProb0E(storm::models::AbstractNondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + static storm::storage::BitVector performProb0E(storm::models::AbstractNondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { // Prepare resulting bit vector. storm::storage::BitVector statesWithProbability0(model.getNumberOfStates()); @@ -299,9 +304,6 @@ public: std::shared_ptr> transitionMatrix = model.getTransitionMatrix(); std::shared_ptr> nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices(); - // Get the backwards transition relation from the model to ease the search. - storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); - // Add all psi states as the already satisfy the condition. statesWithProbability0 |= psiStates; @@ -355,19 +357,17 @@ public: * scheduler tries to minimize this probability. * * @param model The model whose graph structure to search. + * @param backwardTransitions The reversed transition relation of the model. * @param phiStates The set of all states satisfying phi. * @param psiStates The set of all states satisfying psi. * @return A bit vector that represents all states with probability 0. */ template - static storm::storage::BitVector performProb1A(storm::models::AbstractNondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + static storm::storage::BitVector performProb1A(storm::models::AbstractNondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { // Get some temporaries for convenience. std::shared_ptr> transitionMatrix = model.getTransitionMatrix(); std::shared_ptr> nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices(); - // Get the backwards transition relation from the model to ease the search. - storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); - storm::storage::BitVector currentStates(model.getNumberOfStates(), true); std::vector stack;