diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h index 5ab063ef7..418724e3a 100644 --- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h @@ -97,11 +97,16 @@ public: // Check if we already know the result (i.e. probability 0) for all initial states and // don't compute anything in this case. - if (this->getInitialStates().isSubsetOf(~statesWithProbabilityGreater0)) { + if (this->getInitialStates().isDisjointFrom(statesWithProbabilityGreater0)) { LOG4CPLUS_INFO(logger, "The probabilities for the initial states were determined in a preprocessing step." << " No exact probabilities were computed."); - } else { // Otherwise, we have have to compute the probabilities. - // Now we can eliminate the rows and columns from the original transition probability matrix that have probability 0. + // Set the values for all maybe-states to 0.5 to indicate that their probability values are not 0 (and + // not necessarily 1). + storm::utility::vector::setVectorValues(*result, statesWithProbabilityGreater0, Type(0.5)); + } else { + // In this case we have have to compute the probabilities. + + // We can eliminate the rows and columns from the original transition probability matrix that have probability 0. storm::storage::SparseMatrix submatrix = this->getModel().getTransitionMatrix().getSubmatrix(statesWithProbabilityGreater0); // Compute the new set of target states in the reduced system. @@ -117,8 +122,7 @@ public: // Perform the matrix vector multiplication as often as required by the formula bound. this->performMatrixVectorMultiplication(submatrix, subresult, nullptr, formula.getBound()); - // Create result vector and set its values accordingly. - + // Set the values of the resulting vector accordingly. storm::utility::vector::setVectorValues(*result, statesWithProbabilityGreater0, subresult); storm::utility::vector::setVectorValues(*result, ~statesWithProbabilityGreater0, storm::utility::constGetZero()); } @@ -260,9 +264,9 @@ public: // are neither 0 nor 1. storm::utility::vector::setVectorValues(*result, maybeStates, Type(0.5)); } else { - // Otherwise, we have have to compute the probabilities. + // In this case we have have to compute the probabilities. - // First, we can eliminate the rows and columns from the original transition probability matrix. + // 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 // system. That is, we go from x = A*x + b to (I-A)x = b. @@ -388,14 +392,14 @@ public: storm::storage::BitVector trueStates(this->getModel().getNumberOfStates(), true); storm::storage::BitVector infinityStates = storm::utility::graph::performProb1(this->getModel(), trueStates, *targetStates); infinityStates.complement(); - LOG4CPLUS_INFO(logger, "Found " << infinityStates.getNumberOfSetBits() << " 'infinity' states."); + storm::storage::BitVector maybeStates = ~(*targetStates) & ~infinityStates; + LOG4CPLUS_INFO(logger, "Found " << infinityStates.getNumberOfSetBits() << " 'infinity' states."); + LOG4CPLUS_INFO(logger, "Found " << targetStates->getNumberOfSetBits() << " 'target' states."); + LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states."); // Create resulting vector. std::vector* result = new std::vector(this->getModel().getNumberOfStates()); - // Check whether there are states for which we have to compute the result. - storm::storage::BitVector maybeStates = ~(*targetStates) & ~infinityStates; - // Check whether we need to compute exact rewards for some states. if (this->getInitialStates().isDisjointFrom(maybeStates)) { LOG4CPLUS_INFO(logger, "The rewards for the initial states were determined in a preprocessing step." @@ -405,7 +409,6 @@ public: storm::utility::vector::setVectorValues(*result, maybeStates, storm::utility::constGetOne()); } else { // In this case we have to compute the reward values for the remaining states. - const int maybeStatesSetBitCount = maybeStates.getNumberOfSetBits(); // Now we can eliminate the rows and columns from the original transition probability matrix. storm::storage::SparseMatrix submatrix = this->getModel().getTransitionMatrix().getSubmatrix(maybeStates); @@ -415,10 +418,10 @@ public: // Initialize the x vector with 1 for each element. This is the initial guess for // the iterative solvers. - std::vector x(maybeStatesSetBitCount, storm::utility::constGetOne()); + std::vector x(submatrix.getColCount(), storm::utility::constGetOne()); // Prepare the right-hand side of the equation system. - std::vector b(maybeStatesSetBitCount); + std::vector b(submatrix.getRowCount()); if (this->getModel().hasTransitionRewards()) { // If a transition-based reward model is available, we initialize the right-hand // side to the vector resulting from summing the rows of the pointwise product @@ -431,7 +434,7 @@ public: // as well. As the state reward vector contains entries not just for the states // that we still consider (i.e. maybeStates), we need to extract these values // first. - std::vector subStateRewards(maybeStatesSetBitCount); + std::vector subStateRewards(b.size()); storm::utility::vector::selectVectorValues(subStateRewards, maybeStates, this->getModel().getStateRewardVector()); storm::utility::vector::addVectorsInPlace(b, subStateRewards); } diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h index 3611a70a2..74b138d58 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h @@ -94,37 +94,49 @@ public: // First, we need to compute the states that satisfy the sub-formulas of the until-formula. storm::storage::BitVector* leftStates = formula.getLeft().check(*this); storm::storage::BitVector* rightStates = formula.getRight().check(*this); + std::vector* result = new std::vector(this->getModel().getNumberOfStates()); // Determine the states that have 0 probability of reaching the target states. - storm::storage::BitVector maybeStates; + storm::storage::BitVector statesWithProbabilityGreater0; if (this->minimumOperatorStack.top()) { - maybeStates = storm::utility::graph::performProbGreater0A(this->getModel(), this->getModel().getBackwardTransitions(), *leftStates, *rightStates, true, formula.getBound()); + statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0A(this->getModel(), this->getModel().getBackwardTransitions(), *leftStates, *rightStates, true, formula.getBound()); } else { - maybeStates = storm::utility::graph::performProbGreater0E(this->getModel(), this->getModel().getBackwardTransitions(), *leftStates, *rightStates, true, formula.getBound()); + statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0E(this->getModel(), this->getModel().getBackwardTransitions(), *leftStates, *rightStates, true, formula.getBound()); } - // Now we can eliminate the rows and columns from the original transition probability matrix that have probability 0. - storm::storage::SparseMatrix submatrix = this->getModel().getTransitionMatrix().getSubmatrix(maybeStates, this->getModel().getNondeterministicChoiceIndices()); - - // Get the "new" nondeterministic choice indices for the submatrix. - std::vector subNondeterministicChoiceIndices = this->computeNondeterministicChoiceIndicesForConstraint(maybeStates); - - // Compute the new set of target states in the reduced system. - storm::storage::BitVector rightStatesInReducedSystem = maybeStates % *rightStates; - - // Make all rows absorbing that satisfy the second sub-formula. - submatrix.makeRowsAbsorbing(rightStatesInReducedSystem, subNondeterministicChoiceIndices); - - // Create the vector with which to multiply. - std::vector subresult(maybeStates.getNumberOfSetBits()); - storm::utility::vector::setVectorValues(subresult, rightStatesInReducedSystem, storm::utility::constGetOne()); - - this->performMatrixVectorMultiplication(submatrix, subresult, subNondeterministicChoiceIndices, nullptr, formula.getBound()); - - // Create the resulting vector. - std::vector* result = new std::vector(this->getModel().getNumberOfStates()); - storm::utility::vector::setVectorValues(*result, maybeStates, subresult); - storm::utility::vector::setVectorValues(*result, ~maybeStates, storm::utility::constGetZero()); + // Check if we already know the result (i.e. probability 0) for all initial states and + // don't compute anything in this case. + if (this->getInitialStates().isDisjointFrom(statesWithProbabilityGreater0)) { + LOG4CPLUS_INFO(logger, "The probabilities for the initial states were determined in a preprocessing step." + << " No exact probabilities were computed."); + // Set the values for all maybe-states to 0.5 to indicate that their probability values are not 0 (and + // not necessarily 1). + storm::utility::vector::setVectorValues(*result, statesWithProbabilityGreater0, Type(0.5)); + } else { + // In this case we have have to compute the probabilities. + + // We can eliminate the rows and columns from the original transition probability matrix that have probability 0. + storm::storage::SparseMatrix submatrix = this->getModel().getTransitionMatrix().getSubmatrix(statesWithProbabilityGreater0, this->getModel().getNondeterministicChoiceIndices()); + + // Get the "new" nondeterministic choice indices for the submatrix. + std::vector subNondeterministicChoiceIndices = this->computeNondeterministicChoiceIndicesForConstraint(statesWithProbabilityGreater0); + + // Compute the new set of target states in the reduced system. + storm::storage::BitVector rightStatesInReducedSystem = statesWithProbabilityGreater0 % *rightStates; + + // Make all rows absorbing that satisfy the second sub-formula. + submatrix.makeRowsAbsorbing(rightStatesInReducedSystem, subNondeterministicChoiceIndices); + + // Create the vector with which to multiply. + std::vector subresult(statesWithProbabilityGreater0.getNumberOfSetBits()); + storm::utility::vector::setVectorValues(subresult, rightStatesInReducedSystem, storm::utility::constGetOne()); + + this->performMatrixVectorMultiplication(submatrix, subresult, subNondeterministicChoiceIndices, nullptr, formula.getBound()); + + // Set the values of the resulting vector accordingly. + storm::utility::vector::setVectorValues(*result, statesWithProbabilityGreater0, subresult); + storm::utility::vector::setVectorValues(*result, ~statesWithProbabilityGreater0, storm::utility::constGetZero()); + } // Delete intermediate results and return result. delete leftStates; @@ -246,17 +258,28 @@ public: delete leftStates; delete rightStates; + storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1); 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. std::vector* result = new std::vector(this->getModel().getNumberOfStates()); - // Only try to solve system if there are states for which the probability is unknown. - uint_fast64_t maybeStatesSetBitCount = maybeStates.getNumberOfSetBits(); - if (maybeStatesSetBitCount > 0) { + // Check whether we need to compute exact probabilities for some states. + if (this->getInitialStates().isDisjointFrom(maybeStates) || qualitative) { + if (qualitative) { + LOG4CPLUS_INFO(logger, "The formula was checked qualitatively. No exact probabilities were computed."); + } else { + LOG4CPLUS_INFO(logger, "The probabilities for the initial states were determined in a preprocessing step." + << " No exact probabilities were computed."); + } + // Set the values for all maybe-states to 0.5 to indicate that their probability values + // are neither 0 nor 1. + storm::utility::vector::setVectorValues(*result, maybeStates, Type(0.5)); + } else { + // In this case we have have to compute the probabilities. + // First, we can eliminate the rows and columns from the original transition probability matrix for states // whose probabilities are already known. storm::storage::SparseMatrix submatrix = this->getModel().getTransitionMatrix().getSubmatrix(maybeStates, this->getModel().getNondeterministicChoiceIndices()); @@ -265,7 +288,7 @@ public: std::vector subNondeterministicChoiceIndices = this->computeNondeterministicChoiceIndicesForConstraint(maybeStates); // Create vector for results for maybe states. - std::vector x(maybeStatesSetBitCount); + std::vector x(maybeStates.getNumberOfSetBits()); // 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. @@ -385,27 +408,33 @@ public: infinityStates = storm::utility::graph::performProb1E(this->getModel(), this->getModel().getBackwardTransitions(), trueStates, *targetStates); } infinityStates.complement(); - + storm::storage::BitVector maybeStates = ~(*targetStates) & ~infinityStates; LOG4CPLUS_INFO(logger, "Found " << infinityStates.getNumberOfSetBits() << " 'infinity' states."); LOG4CPLUS_INFO(logger, "Found " << targetStates->getNumberOfSetBits() << " 'target' states."); - storm::storage::BitVector maybeStates = ~(*targetStates) & ~infinityStates; LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states."); // Create resulting vector. std::vector* result = new std::vector(this->getModel().getNumberOfStates()); - // Check whether there are states for which we have to compute the result. - const int maybeStatesSetBitCount = maybeStates.getNumberOfSetBits(); - if (maybeStatesSetBitCount > 0) { - // First, we can eliminate the rows and columns from the original transition probability matrix for states - // whose probabilities are already known. + // Check whether we need to compute exact rewards for some states. + if (this->getInitialStates().isDisjointFrom(maybeStates)) { + LOG4CPLUS_INFO(logger, "The rewards for the initial states were determined in a preprocessing step." + << " No exact rewards were computed."); + // Set the values for all maybe-states to 1 to indicate that their reward values + // are neither 0 nor infinity. + storm::utility::vector::setVectorValues(*result, maybeStates, storm::utility::constGetOne()); + } else { + // In this case we have to compute the reward values for the remaining states. + + // We can eliminate the rows and columns from the original transition probability matrix for states + // whose reward values are already known. storm::storage::SparseMatrix submatrix = this->getModel().getTransitionMatrix().getSubmatrix(maybeStates, this->getModel().getNondeterministicChoiceIndices()); // Get the "new" nondeterministic choice indices for the submatrix. std::vector subNondeterministicChoiceIndices = this->computeNondeterministicChoiceIndicesForConstraint(maybeStates); // Create vector for results for maybe states. - std::vector x(maybeStatesSetBitCount); + std::vector x(submatrix.getRowCount()); // 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.