From e4c270288904fdb531969501823b1a177bedb5b8 Mon Sep 17 00:00:00 2001
From: Mavo <matthias.volk@rwth-aachen.de>
Date: Tue, 1 Mar 2016 12:18:01 +0100
Subject: [PATCH] Fixed problem in MaximalEndComponents
Former-commit-id: 950b9cfdfa677f47567e2c90fdadd3a65867dac4
---
.../helper/SparseMarkovAutomatonCslHelper.cpp | 46 +++++++------
src/storage/Decomposition.cpp | 5 ++
src/storage/Decomposition.h | 7 ++
.../MaximalEndComponentDecomposition.cpp | 68 ++++++++++---------
4 files changed, 72 insertions(+), 54 deletions(-)
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<ValueType> x(maybeStates.getNumberOfSetBits());
- storm::storage::SparseMatrix<ValueType> 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<ValueType> rewardValues(stateRewards);
- for (auto state : markovianStates) {
- rewardValues[state] = rewardValues[state] / exitRateVector[state];
- }
-
- // Finally, prepare the actual right-hand side.
- std::vector<ValueType> b(submatrix.getRowCount());
- storm::utility::vector::selectVectorValuesRepeatedly(b, maybeStates, transitionMatrix.getRowGroupIndices(), rewardValues);
-
- // Solve the corresponding system of equations.
- std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = minMaxLinearEquationSolverFactory.create(submatrix);
- solver->solveEquationSystem(dir, x, b);
-
+
// Create resulting vector.
std::vector<ValueType> result(numberOfStates);
- // Set values of resulting vector according to previous result and return the result.
- storm::utility::vector::setVectorValues<ValueType>(result, maybeStates, x);
+ if (!maybeStates.empty()) {
+ // Then, we can eliminate the rows and columns for all states whose values are already known.
+ std::vector<ValueType> x(maybeStates.getNumberOfSetBits());
+ storm::storage::SparseMatrix<ValueType> 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<ValueType> rewardValues(stateRewards);
+ for (auto state : markovianStates) {
+ rewardValues[state] = rewardValues[state] / exitRateVector[state];
+ }
+
+ // Finally, prepare the actual right-hand side.
+ std::vector<ValueType> b(submatrix.getRowCount());
+ storm::utility::vector::selectVectorValuesRepeatedly(b, maybeStates, transitionMatrix.getRowGroupIndices(), rewardValues);
+
+ // Solve the corresponding system of equations.
+ std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> 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<ValueType>(result, maybeStates, x);
+ }
+
storm::utility::vector::setVectorValues(result, goalStates, storm::utility::zero<ValueType>());
storm::utility::vector::setVectorValues(result, infinityStates, storm::utility::infinity<ValueType>());
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 <typename BlockType>
+ bool Decomposition<BlockType>::empty() const {
+ return blocks.empty();
+ }
+
template <typename BlockType>
typename Decomposition<BlockType>::iterator Decomposition<BlockType>::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());
+ }
}
}
}