diff --git a/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index d926917a5..95007a9e6 100644 --- a/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -407,33 +407,35 @@ namespace storm { infinityStates = storm::storage::BitVector(numberOfStates); } } - // Now we identify the states for which values need to be computed. storm::storage::BitVector maybeStates = ~(goalStates | infinityStates); - - // Then, we can eliminate the rows and columns for all states whose values are already known to be 0. - std::vector x(maybeStates.getNumberOfSetBits()); - storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, maybeStates, maybeStates); - - // Now prepare the expected reward values for all states so they can be used as the right-hand side of the equation system. - std::vector rewardValues(stateRewards); - for (auto state : markovianStates) { - rewardValues[state] = rewardValues[state] / exitRateVector[state]; - } - - // Finally, prepare the actual right-hand side. - std::vector b(submatrix.getRowCount()); - storm::utility::vector::selectVectorValuesRepeatedly(b, maybeStates, transitionMatrix.getRowGroupIndices(), rewardValues); - - // Solve the corresponding system of equations. - std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(submatrix); - solver->solveEquationSystem(dir, x, b); - + // Create resulting vector. std::vector result(numberOfStates); - // Set values of resulting vector according to previous result and return the result. - storm::utility::vector::setVectorValues(result, maybeStates, x); + if (!maybeStates.empty()) { + // Then, we can eliminate the rows and columns for all states whose values are already known. + std::vector x(maybeStates.getNumberOfSetBits()); + storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, maybeStates, maybeStates); + + // Now prepare the expected reward values for all states so they can be used as the right-hand side of the equation system. + std::vector rewardValues(stateRewards); + for (auto state : markovianStates) { + rewardValues[state] = rewardValues[state] / exitRateVector[state]; + } + + // Finally, prepare the actual right-hand side. + std::vector b(submatrix.getRowCount()); + storm::utility::vector::selectVectorValuesRepeatedly(b, maybeStates, transitionMatrix.getRowGroupIndices(), rewardValues); + + // Solve the corresponding system of equations. + std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(submatrix); + solver->solveEquationSystem(dir, x, b); + + // Set values of resulting vector according to previous result and return the result. + storm::utility::vector::setVectorValues(result, maybeStates, x); + } + storm::utility::vector::setVectorValues(result, goalStates, storm::utility::zero()); storm::utility::vector::setVectorValues(result, infinityStates, storm::utility::infinity()); diff --git a/src/storage/Decomposition.cpp b/src/storage/Decomposition.cpp index 4e2ebcb02..54d7ef12e 100644 --- a/src/storage/Decomposition.cpp +++ b/src/storage/Decomposition.cpp @@ -41,6 +41,11 @@ namespace storm { return blocks.size(); } + template + bool Decomposition::empty() const { + return blocks.empty(); + } + template typename Decomposition::iterator Decomposition::begin() { return blocks.begin(); diff --git a/src/storage/Decomposition.h b/src/storage/Decomposition.h index ce522c171..76f8a28a8 100644 --- a/src/storage/Decomposition.h +++ b/src/storage/Decomposition.h @@ -63,6 +63,13 @@ namespace storm { */ std::size_t size() const; + /*! + * Checks if the decomposition is empty. + * + * @return True, if the decomposition is empty. + */ + bool empty() const; + /*! * Retrieves an iterator that points to the first block of this decomposition. * diff --git a/src/storage/MaximalEndComponentDecomposition.cpp b/src/storage/MaximalEndComponentDecomposition.cpp index 31c421224..a944ecd23 100644 --- a/src/storage/MaximalEndComponentDecomposition.cpp +++ b/src/storage/MaximalEndComponentDecomposition.cpp @@ -86,48 +86,52 @@ namespace storm { mecChanged |= sccs.size() > 1 || (sccs.size() > 0 && sccs[0].size() < mec.size()); // Check for each of the SCCs whether there is at least one action for each state that does not leave the SCC. - for (auto& scc : sccs) { - statesToCheck.set(scc.begin(), scc.end()); - - while (!statesToCheck.empty()) { - storm::storage::BitVector statesToRemove(numberOfStates); + if (sccs.empty()) { + mecChanged = true; + } else { + for (auto& scc : sccs) { + statesToCheck.set(scc.begin(), scc.end()); - for (auto state : statesToCheck) { - bool keepStateInMEC = false; + while (!statesToCheck.empty()) { + storm::storage::BitVector statesToRemove(numberOfStates); - for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) { - bool choiceContainedInMEC = true; - for (auto const& entry : transitionMatrix.getRow(choice)) { - if (!scc.containsState(entry.getColumn())) { - choiceContainedInMEC = false; + for (auto state : statesToCheck) { + bool keepStateInMEC = false; + + for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) { + bool choiceContainedInMEC = true; + for (auto const& entry : transitionMatrix.getRow(choice)) { + if (!scc.containsState(entry.getColumn())) { + choiceContainedInMEC = false; + break; + } + } + + // If there is at least one choice whose successor states are fully contained in the MEC, we can leave the state in the MEC. + if (choiceContainedInMEC) { + keepStateInMEC = true; break; } } - // If there is at least one choice whose successor states are fully contained in the MEC, we can leave the state in the MEC. - if (choiceContainedInMEC) { - keepStateInMEC = true; - break; + if (!keepStateInMEC) { + statesToRemove.set(state, true); } } - if (!keepStateInMEC) { - statesToRemove.set(state, true); + // Now erase the states that have no option to stay inside the MEC with all successors. + mecChanged |= !statesToRemove.empty(); + for (uint_fast64_t state : statesToRemove) { + scc.erase(state); } - } - - // Now erase the states that have no option to stay inside the MEC with all successors. - mecChanged |= !statesToRemove.empty(); - for (uint_fast64_t state : statesToRemove) { - scc.erase(state); - } - - // Now check which states should be reconsidered, because successors of them were removed. - statesToCheck.clear(); - for (auto state : statesToRemove) { - for (auto const& entry : backwardTransitions.getRow(state)) { - if (scc.containsState(entry.getColumn())) { - statesToCheck.set(entry.getColumn()); + + // Now check which states should be reconsidered, because successors of them were removed. + statesToCheck.clear(); + for (auto state : statesToRemove) { + for (auto const& entry : backwardTransitions.getRow(state)) { + if (scc.containsState(entry.getColumn())) { + statesToCheck.set(entry.getColumn()); + } } } }