diff --git a/src/modelchecker/GmmxxDtmcPrctlModelChecker.h b/src/modelchecker/GmmxxDtmcPrctlModelChecker.h index a75276405..fdd246843 100644 --- a/src/modelchecker/GmmxxDtmcPrctlModelChecker.h +++ b/src/modelchecker/GmmxxDtmcPrctlModelChecker.h @@ -131,7 +131,7 @@ public: // Only try to solve system if there are states for which the probability is unknown. uint_fast64_t mayBeStatesSetBitCount = maybeStates.getNumberOfSetBits(); - if (mayBeStatesSetBitCount > 0) { + if (mayBeStatesSetBitCount > 0 && !qualitative) { // Now we can eliminate the rows and columns from the original transition probability matrix. storm::storage::SparseMatrix* submatrix = this->getModel().getTransitionMatrix()->getSubmatrix(maybeStates); // Converting the matrix from the fixpoint notation to the form needed for the equation @@ -160,6 +160,10 @@ public: // Delete temporary matrix. delete gmmxxMatrix; + } else if (qualitative) { + // If we only need a qualitative result, we can safely assume that the results will only be compared to + // bounds which are either 0 or 1. Setting the value to 0.5 is thus safe. + storm::utility::setVectorValues(result, maybeStates, Type(0.5)); } // Set values of resulting vector that are known exactly. diff --git a/src/modelchecker/GmmxxMdpPrctlModelChecker.h b/src/modelchecker/GmmxxMdpPrctlModelChecker.h index 1c8741ebd..e22da7263 100644 --- a/src/modelchecker/GmmxxMdpPrctlModelChecker.h +++ b/src/modelchecker/GmmxxMdpPrctlModelChecker.h @@ -56,7 +56,7 @@ public: std::shared_ptr> nondeterministicChoiceIndices = this->getModel().getNondeterministicChoiceIndices(); // Make all rows absorbing that violate both sub-formulas or satisfy the second sub-formula. - tmpMatrix.makeRowsAbsorbing(~(*leftStates | *rightStates) | *rightStates); + tmpMatrix.makeRowsAbsorbing(~(*leftStates | *rightStates) | *rightStates, *nondeterministicChoiceIndices); // Transform the transition probability matrix to the gmm++ format to use its arithmetic. gmm::csr_matrix* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(tmpMatrix); @@ -67,12 +67,11 @@ public: // Create vector for result of multiplication, which is reduced to the result vector after // each multiplication. - std::vector* multiplyResult = new std::vector(this->getModel().getTransitionMatrix()->getRowCount()); + std::vector* multiplyResult = new std::vector(this->getModel().getTransitionMatrix()->getRowCount(), 0); // Now perform matrix-vector multiplication as long as we meet the bound of the formula. for (uint_fast64_t i = 0; i < formula.getBound(); ++i) { gmm::mult(*gmmxxMatrix, *result, *multiplyResult); - if (this->minimumOperatorStack.top()) { storm::utility::reduceVectorMin(*multiplyResult, result, *nondeterministicChoiceIndices); } else { diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index 32ddfb7a4..62ed99eca 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -641,12 +641,29 @@ public: bool makeRowsAbsorbing(const storm::storage::BitVector rows) { bool result = true; for (auto row : rows) { - result &= makeRowAbsorbing(row); + result &= makeRowAbsorbing(row, row); } return result; } + /*! + * This function makes the groups of rows given by the bit vector absorbing. + * @param rows A bit vector indicating which row groups to make absorbing. + * @return True iff the operation was successful. + */ + bool makeRowsAbsorbing(const storm::storage::BitVector rows, std::vector const& nondeterministicChoices) { + bool result = true; + for (auto index : rows) { + for (uint_fast64_t row = nondeterministicChoices[index]; row < nondeterministicChoices[index + 1]; ++row) { + result &= makeRowAbsorbing(row, index); + } + } + + return result; + } + + /*! * This function makes the given row absorbing. This means that all * entries in will be set to 0 and the value 1 will be written @@ -654,7 +671,7 @@ public: * @param row The row to be made absorbing. * @returns True iff the operation was successful. */ - bool makeRowAbsorbing(const uint_fast64_t row) { + bool makeRowAbsorbing(const uint_fast64_t row, const uint_fast64_t column) { // Check whether the accessed state exists. if (row > rowCount) { LOG4CPLUS_ERROR(logger, "Trying to make an illegal row " << row << " absorbing."); @@ -668,28 +685,16 @@ public: uint_fast64_t rowEnd = rowIndications[row + 1]; if (rowStart >= rowEnd) { - LOG4CPLUS_ERROR(logger, "Cannot make row absorbing, because there is no entry in this row."); - throw storm::exceptions::InvalidStateException("Cannot make row absorbing, because there is no entry in this row."); + LOG4CPLUS_ERROR(logger, "Cannot make row " << row << " absorbing, because there is no entry in this row."); + throw storm::exceptions::InvalidStateException() << "Cannot make row " << row << " absorbing, because there is no entry in this row."; } - uint_fast64_t pseudoDiagonal = row % colCount; - bool foundDiagonal = false; - while (rowStart < rowEnd) { - if (!foundDiagonal && columnIndications[rowStart] >= pseudoDiagonal) { - foundDiagonal = true; - // insert/replace the diagonal entry - columnIndications[rowStart] = pseudoDiagonal; - valueStorage[rowStart] = storm::utility::constGetOne(); - } else { - valueStorage[rowStart] = storm::utility::constGetZero(); - } - ++rowStart; - } + valueStorage[rowStart] = storm::utility::constGetOne(); + columnIndications[rowStart] = column; - if (!foundDiagonal) { - --rowStart; - columnIndications[rowStart] = pseudoDiagonal; - valueStorage[rowStart] = storm::utility::constGetOne(); + for (uint_fast64_t index = rowStart + 1; index < rowEnd; ++index) { + valueStorage[index] = storm::utility::constGetZero(); + columnIndications[index] = 0; } return true; diff --git a/src/storm.cpp b/src/storm.cpp index 62152c31c..d75982d34 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -226,20 +226,34 @@ void testCheckingDice(storm::models::Mdp& mdp) { void testCheckingAsynchLeader(storm::models::Mdp& mdp) { storm::formula::Ap* electedFormula = new storm::formula::Ap("elected"); storm::formula::Eventually* eventuallyFormula = new storm::formula::Eventually(electedFormula); - storm::formula::ProbabilisticNoBoundOperator* probMaxFormula = new storm::formula::ProbabilisticNoBoundOperator(eventuallyFormula, false); + storm::formula::ProbabilisticNoBoundOperator* probMinFormula = new storm::formula::ProbabilisticNoBoundOperator(eventuallyFormula, true); storm::modelChecker::GmmxxMdpPrctlModelChecker* mc = new storm::modelChecker::GmmxxMdpPrctlModelChecker(mdp); + mc->check(*probMinFormula); + delete probMinFormula; + + electedFormula = new storm::formula::Ap("elected"); + eventuallyFormula = new storm::formula::Eventually(electedFormula); + storm::formula::ProbabilisticNoBoundOperator* probMaxFormula = new storm::formula::ProbabilisticNoBoundOperator(eventuallyFormula, false); + mc->check(*probMaxFormula); delete probMaxFormula; electedFormula = new storm::formula::Ap("elected"); - eventuallyFormula = new storm::formula::Eventually(electedFormula); - storm::formula::ProbabilisticNoBoundOperator* probMinFormula = new storm::formula::ProbabilisticNoBoundOperator(eventuallyFormula, true); + storm::formula::BoundedEventually* boundedEventuallyFormula = new storm::formula::BoundedEventually(electedFormula, 50); + probMinFormula = new storm::formula::ProbabilisticNoBoundOperator(boundedEventuallyFormula, true); mc->check(*probMinFormula); delete probMinFormula; + electedFormula = new storm::formula::Ap("elected"); + boundedEventuallyFormula = new storm::formula::BoundedEventually(electedFormula, 50); + probMaxFormula = new storm::formula::ProbabilisticNoBoundOperator(boundedEventuallyFormula, false); + + mc->check(*probMaxFormula); + delete probMaxFormula; + delete mc; }