diff --git a/src/modelchecker/EigenDtmcPrctlModelChecker.h b/src/modelchecker/EigenDtmcPrctlModelChecker.h index 61867620d..6965b3a0c 100644 --- a/src/modelchecker/EigenDtmcPrctlModelChecker.h +++ b/src/modelchecker/EigenDtmcPrctlModelChecker.h @@ -126,17 +126,16 @@ public: // Then, we need to identify the states which have to be taken out of the matrix, i.e. // all states that have probability 0 and 1 of satisfying the until-formula. - storm::storage::BitVector notExistsPhiUntilPsiStates(this->getModel().getNumberOfStates()); - storm::storage::BitVector alwaysPhiUntilPsiStates(this->getModel().getNumberOfStates()); - storm::utility::GraphAnalyzer::getPhiUntilPsiStates(this->getModel(), *leftStates, *rightStates, ¬ExistsPhiUntilPsiStates, &alwaysPhiUntilPsiStates); - notExistsPhiUntilPsiStates.complement(); + storm::storage::BitVector statesWithProbability0(this->getModel().getNumberOfStates()); + storm::storage::BitVector statesWithProbability1(this->getModel().getNumberOfStates()); + storm::utility::GraphAnalyzer::performProb01(this->getModel(), *leftStates, *rightStates, &statesWithProbability0, &statesWithProbability1); delete leftStates; delete rightStates; - LOG4CPLUS_INFO(logger, "Found " << notExistsPhiUntilPsiStates.getNumberOfSetBits() << " 'no' states."); - LOG4CPLUS_INFO(logger, "Found " << alwaysPhiUntilPsiStates.getNumberOfSetBits() << " 'yes' states."); - storm::storage::BitVector maybeStates = ~(notExistsPhiUntilPsiStates | alwaysPhiUntilPsiStates); + LOG4CPLUS_INFO(logger, "Found " << statesWithProbability0.getNumberOfSetBits() << " 'no' states."); + LOG4CPLUS_INFO(logger, "Found " << statesWithProbability1.getNumberOfSetBits() << " 'yes' states."); + storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1); LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states."); // Create resulting vector and set values accordingly. @@ -175,7 +174,7 @@ public: Type *pb = &(b[0]); // get the address storing the data for b MapType vectorB(pb, b.size()); // vectorB shares data - this->getModel().getTransitionProbabilityMatrix()->getConstrainedRowCountVector(maybeStates, alwaysPhiUntilPsiStates, &x); + this->getModel().getTransitionProbabilityMatrix()->getConstrainedRowCountVector(maybeStates, statesWithProbability1, &x); Eigen::BiCGSTAB> solver; solver.compute(*eigenSubMatrix); @@ -212,8 +211,8 @@ public: delete eigenSubMatrix; } - storm::utility::setVectorValues(result, notExistsPhiUntilPsiStates, storm::utility::constGetZero()); - storm::utility::setVectorValues(result, alwaysPhiUntilPsiStates, storm::utility::constGetOne()); + storm::utility::setVectorValues(result, statesWithProbability0, storm::utility::constGetZero()); + storm::utility::setVectorValues(result, statesWithProbability1, storm::utility::constGetOne()); return result; } diff --git a/src/modelchecker/GmmxxDtmcPrctlModelChecker.h b/src/modelchecker/GmmxxDtmcPrctlModelChecker.h index 6d11358b9..359462c1f 100644 --- a/src/modelchecker/GmmxxDtmcPrctlModelChecker.h +++ b/src/modelchecker/GmmxxDtmcPrctlModelChecker.h @@ -111,18 +111,17 @@ public: // Then, we need to identify the states which have to be taken out of the matrix, i.e. // all states that have probability 0 and 1 of satisfying the until-formula. - storm::storage::BitVector notExistsPhiUntilPsiStates(this->getModel().getNumberOfStates()); - storm::storage::BitVector alwaysPhiUntilPsiStates(this->getModel().getNumberOfStates()); - storm::utility::GraphAnalyzer::getPhiUntilPsiStates(this->getModel(), *leftStates, *rightStates, ¬ExistsPhiUntilPsiStates, &alwaysPhiUntilPsiStates); - notExistsPhiUntilPsiStates.complement(); + storm::storage::BitVector statesWithProbability0(this->getModel().getNumberOfStates()); + storm::storage::BitVector statesWithProbability1(this->getModel().getNumberOfStates()); + storm::utility::GraphAnalyzer::performProb01(this->getModel(), *leftStates, *rightStates, &statesWithProbability0, &statesWithProbability1); // Delete sub-results that are obsolete now. delete leftStates; delete rightStates; - LOG4CPLUS_INFO(logger, "Found " << notExistsPhiUntilPsiStates.getNumberOfSetBits() << " 'no' states."); - LOG4CPLUS_INFO(logger, "Found " << alwaysPhiUntilPsiStates.getNumberOfSetBits() << " 'yes' states."); - storm::storage::BitVector maybeStates = ~(notExistsPhiUntilPsiStates | alwaysPhiUntilPsiStates); + LOG4CPLUS_INFO(logger, "Found " << statesWithProbability0.getNumberOfSetBits() << " 'no' states."); + LOG4CPLUS_INFO(logger, "Found " << statesWithProbability1.getNumberOfSetBits() << " 'yes' states."); + storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1); LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states."); // Create resulting vector. @@ -149,7 +148,7 @@ public: // Prepare the right-hand side of the equation system. For entry i this corresponds to // the accumulated probability of going from state i to some 'yes' state. std::vector b(mayBeStatesSetBitCount); - this->getModel().getTransitionMatrix()->getConstrainedRowCountVector(maybeStates, alwaysPhiUntilPsiStates, &b); + this->getModel().getTransitionMatrix()->getConstrainedRowCountVector(maybeStates, statesWithProbability1, &b); // Solve the corresponding system of linear equations. this->solveLinearEquationSystem(*gmmxxMatrix, x, b); @@ -162,8 +161,8 @@ public: } // Set values of resulting vector that are known exactly. - storm::utility::setVectorValues(result, notExistsPhiUntilPsiStates, storm::utility::constGetZero()); - storm::utility::setVectorValues(result, alwaysPhiUntilPsiStates, storm::utility::constGetOne()); + storm::utility::setVectorValues(result, statesWithProbability0, storm::utility::constGetZero()); + storm::utility::setVectorValues(result, statesWithProbability1, storm::utility::constGetOne()); return result; } @@ -253,7 +252,7 @@ public: // Determine which states have a reward of infinity by definition. storm::storage::BitVector infinityStates(this->getModel().getNumberOfStates()); storm::storage::BitVector trueStates(this->getModel().getNumberOfStates(), true); - storm::utility::GraphAnalyzer::getAlwaysPhiUntilPsiStates(this->getModel(), trueStates, *targetStates, &infinityStates); + storm::utility::GraphAnalyzer::performProb1(this->getModel(), trueStates, *targetStates, &infinityStates); infinityStates.complement(); // Create resulting vector. diff --git a/src/utility/GraphAnalyzer.h b/src/utility/GraphAnalyzer.h index 02c122d89..07ba3eeaf 100644 --- a/src/utility/GraphAnalyzer.h +++ b/src/utility/GraphAnalyzer.h @@ -22,30 +22,58 @@ namespace utility { class GraphAnalyzer { public: + /*! + * Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi until psi in a + * deterministic model. + * @param model The model whose graph structure to search. + * @param phiStates The set of all states satisfying phi. + * @param psiStates The set of all states satisfying psi. + * @param statesWithProbability0 A pointer to a bit vector that is initially empty and will contain all states with + * probability 0 after the invocation of the function. + * @param statesWithProbability1 A pointer to a bit vector that is initially empty and will contain all states with + * probability 1 after the invocation of the function. + */ + template + static void performProb01(storm::models::AbstractDeterministicModel& model, const storm::storage::BitVector& phiStates, const storm::storage::BitVector& psiStates, storm::storage::BitVector* statesWithProbability0, storm::storage::BitVector* statesWithProbability1) { + // Check for valid parameters. + if (statesWithProbability0 == nullptr) { + LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability0' must not be null."); + throw storm::exceptions::InvalidArgumentException("Parameter 'statesWithProbability0' must not be null."); + } + if (statesWithProbability1 == nullptr) { + LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability1' must not be null."); + throw storm::exceptions::InvalidArgumentException("Parameter 'statesWithProbability1' must not be null."); + } + + // Perform the actual search. + GraphAnalyzer::performProbGreater0(model, phiStates, psiStates, statesWithProbability0); + GraphAnalyzer::performProb1(model, phiStates, psiStates, *statesWithProbability0, statesWithProbability1); + statesWithProbability0->complement(); + } + /*! * Performs a backwards depth-first search trough the underlying graph structure - * of the given model to determine which states of the model can reach one - * of the given target states whilst always staying in the set of filter states - * before. The resulting states are written to the given bit vector. + * of the given model to determine which states of the model have a positive probability + * of satisfying phi until psi. The resulting states are written to the given bit vector. * @param model The model whose graph structure to search. * @param phiStates A bit vector of all states satisfying phi. * @param psiStates A bit vector of all states satisfying psi. - * @param existsPhiUntilPsiStates A pointer to the result of the search for states that possess - * a paths satisfying phi until psi. + * @param statesWithProbabilityGreater0 A pointer to the result of the search for states that possess + * a positive probability of satisfying phi until psi. */ template - static void getExistsPhiUntilPsiStates(storm::models::AbstractDeterministicModel& model, const storm::storage::BitVector& phiStates, const storm::storage::BitVector& psiStates, storm::storage::BitVector* existsPhiUntilPsiStates) { + static void performProbGreater0(storm::models::AbstractDeterministicModel& model, const storm::storage::BitVector& phiStates, const storm::storage::BitVector& psiStates, storm::storage::BitVector* statesWithProbabilityGreater0) { // Check for valid parameter. - if (existsPhiUntilPsiStates == nullptr) { - LOG4CPLUS_ERROR(logger, "Parameter 'existsPhiUntilPhiStates' must not be null."); - throw storm::exceptions::InvalidArgumentException("Parameter 'existsPhiUntilPhiStates' must not be null."); + if (statesWithProbabilityGreater0 == nullptr) { + LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbabilityGreater0' must not be null."); + throw storm::exceptions::InvalidArgumentException("Parameter 'statesWithProbabilityGreater0' must not be null."); } // Get the backwards transition relation from the model to ease the search. storm::models::GraphTransitions& backwardTransitions = model.getBackwardTransitions(); // Add all psi states as the already satisfy the condition. - *existsPhiUntilPsiStates |= psiStates; + *statesWithProbabilityGreater0 |= psiStates; // Initialize the stack used for the DFS with the states std::vector stack; @@ -58,8 +86,8 @@ public: stack.pop_back(); for(auto it = backwardTransitions.beginStateSuccessorsIterator(currentState); it != backwardTransitions.endStateSuccessorsIterator(currentState); ++it) { - if (phiStates.get(*it) && !existsPhiUntilPsiStates->get(*it)) { - existsPhiUntilPsiStates->set(*it, true); + if (phiStates.get(*it) && !statesWithProbabilityGreater0->get(*it)) { + statesWithProbabilityGreater0->set(*it, true); stack.push_back(*it); } } @@ -75,27 +103,29 @@ public: * @param model The model whose graph structure to search. * @param phiStates A bit vector of all states satisfying phi. * @param psiStates A bit vector of all states satisfying psi. - * @param existsPhiUntilPsiStates A reference to a bit vector of states that possess a path - * satisfying phi until psi. + * @param statesWithProbabilityGreater0 A reference to a bit vector of states that possess a positive + * probability mass of satisfying phi until psi. * @param alwaysPhiUntilPsiStates A pointer to the result of the search for states that only * have paths satisfying phi until psi. */ template - static void getAlwaysPhiUntilPsiStates(storm::models::AbstractDeterministicModel& model, const storm::storage::BitVector& phiStates, const storm::storage::BitVector& psiStates, const storm::storage::BitVector& existsPhiUntilPsiStates, storm::storage::BitVector* alwaysPhiUntilPsiStates) { + static void performProb1(storm::models::AbstractDeterministicModel& model, const storm::storage::BitVector& phiStates, const storm::storage::BitVector& psiStates, const storm::storage::BitVector& statesWithProbabilityGreater0, storm::storage::BitVector* statesWithProbability1) { // Check for valid parameter. - if (alwaysPhiUntilPsiStates == nullptr) { - LOG4CPLUS_ERROR(logger, "Parameter 'alwaysPhiUntilPhiStates' must not be null."); - throw storm::exceptions::InvalidArgumentException("Parameter 'alwaysPhiUntilPhiStates' must not be null."); + if (statesWithProbability1 == nullptr) { + LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability1' must not be null."); + throw storm::exceptions::InvalidArgumentException("Parameter 'statesWithProbability1' must not be null."); } - GraphAnalyzer::getExistsPhiUntilPsiStates(model, ~psiStates, ~existsPhiUntilPsiStates, alwaysPhiUntilPsiStates); - alwaysPhiUntilPsiStates->complement(); + GraphAnalyzer::performProbGreater0(model, ~psiStates, ~statesWithProbabilityGreater0, statesWithProbability1); + statesWithProbability1->complement(); } /*! * Computes the set of states of the given model for which all paths lead to * the given set of target states and only visit states from the filter set - * before. The results are written to the given bit vector. + * before. In order to do this, it uses the given set of states that + * characterizes the states that possess at least one path to a target state. + * The results are written to the given bit vector. * @param model The model whose graph structure to search. * @param phiStates A bit vector of all states satisfying phi. * @param psiStates A bit vector of all states satisfying psi. @@ -103,49 +133,19 @@ public: * have paths satisfying phi until psi. */ template - static void getAlwaysPhiUntilPsiStates(storm::models::AbstractDeterministicModel& model, const storm::storage::BitVector& phiStates, const storm::storage::BitVector& psiStates, storm::storage::BitVector* alwaysPhiUntilPsiStates) { + static void performProb1(storm::models::AbstractDeterministicModel& model, const storm::storage::BitVector& phiStates, const storm::storage::BitVector& psiStates, storm::storage::BitVector* statesWithProbability1) { // Check for valid parameter. - if (alwaysPhiUntilPsiStates == nullptr) { - LOG4CPLUS_ERROR(logger, "Parameter 'alwaysPhiUntilPhiStates' must not be null."); - throw storm::exceptions::InvalidArgumentException("Parameter 'alwaysPhiUntilPhiStates' must not be null."); + if (statesWithProbability1 == nullptr) { + LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability1' must not be null."); + throw storm::exceptions::InvalidArgumentException("Parameter 'statesWithProbability1' must not be null."); } - storm::storage::BitVector existsPhiUntilPsiStates(model.getNumberOfStates()); - GraphAnalyzer::getExistsPhiUntilPsiStates(model, phiStates, psiStates, &existsPhiUntilPsiStates); - GraphAnalyzer::getExistsPhiUntilPsiStates(model, ~psiStates, ~existsPhiUntilPsiStates, alwaysPhiUntilPsiStates); - alwaysPhiUntilPsiStates->complement(); + storm::storage::BitVector* statesWithProbabilityGreater0 = new storm::storage::BitVector(model.getNumberOfStates()); + GraphAnalyzer::performProbGreater0(model, phiStates, psiStates, statesWithProbabilityGreater0); + GraphAnalyzer::performProbGreater0(model, ~psiStates, ~(*statesWithProbabilityGreater0), statesWithProbability1); + delete statesWithProbabilityGreater0; + statesWithProbability1->complement(); } - - - /*! - * Computes the set of states of the given model for which all paths lead to - * the given set of target states and only visit states from the filter set - * before. - * @param model The model whose graph structure to search. - * @param phiStates A bit vector of all states satisfying phi. - * @param psiStates A bit vector of all states satisfying psi. - * @param existsPhiUntilPsiStates A pointer to the result of the search for states that possess - * a path satisfying phi until psi. - * @param alwaysPhiUntilPsiStates A pointer to the result of the search for states that only - * have paths satisfying phi until psi. - */ - template - static void getPhiUntilPsiStates(storm::models::AbstractDeterministicModel& model, const storm::storage::BitVector& phiStates, const storm::storage::BitVector& psiStates, storm::storage::BitVector* existsPhiUntilPsiStates, storm::storage::BitVector* alwaysPhiUntilPsiStates) { - // Check for valid parameters. - if (existsPhiUntilPsiStates == nullptr) { - LOG4CPLUS_ERROR(logger, "Parameter 'existsPhiUntilPhiStates' must not be null."); - throw storm::exceptions::InvalidArgumentException("Parameter 'existsPhiUntilPhiStates' must not be null."); - } - if (alwaysPhiUntilPsiStates == nullptr) { - LOG4CPLUS_ERROR(logger, "Parameter 'alwaysPhiUntilPhiStates' must not be null."); - throw storm::exceptions::InvalidArgumentException("Parameter 'alwaysPhiUntilPhiStates' must not be null."); - } - - // Perform search. - GraphAnalyzer::getExistsPhiUntilPsiStates(model, phiStates, psiStates, existsPhiUntilPsiStates); - GraphAnalyzer::getAlwaysPhiUntilPsiStates(model, phiStates, psiStates, *existsPhiUntilPsiStates, alwaysPhiUntilPsiStates); - } - }; } // namespace utility