Browse Source

Let the topological equation solvers handle singleton SCCs with self-loops directly.

tempestpy_adaptions
TimQu 6 years ago
parent
commit
2aeab4b2e7
  1. 6
      src/storm/solver/TopologicalLinearEquationSolver.cpp
  2. 12
      src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp

6
src/storm/solver/TopologicalLinearEquationSolver.cpp

@ -80,7 +80,7 @@ namespace storm {
} else { } else {
storm::storage::BitVector sccAsBitVector(x.size(), false); storm::storage::BitVector sccAsBitVector(x.size(), false);
for (auto const& scc : *this->sortedSccDecomposition) { for (auto const& scc : *this->sortedSccDecomposition) {
if (scc.isTrivial()) {
if (scc.size() == 1) {
returnValue = solveTrivialScc(*scc.begin(), x, b) && returnValue; returnValue = solveTrivialScc(*scc.begin(), x, b) && returnValue;
} else { } else {
sccAsBitVector.clear(); sccAsBitVector.clear();
@ -131,8 +131,12 @@ namespace storm {
} }
if (hasDiagonalEntry) { if (hasDiagonalEntry) {
if (storm::utility::isZero(denominator)) {
STORM_LOG_THROW(storm::utility::isZero(xi), storm::exceptions::InvalidOperationException, "The equation system has no solution.");
} else {
xi /= denominator; xi /= denominator;
} }
}
return true; return true;
} }

12
src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp

@ -78,7 +78,7 @@ namespace storm {
storm::storage::BitVector sccRowGroupsAsBitVector(x.size(), false); storm::storage::BitVector sccRowGroupsAsBitVector(x.size(), false);
storm::storage::BitVector sccRowsAsBitVector(b.size(), false); storm::storage::BitVector sccRowsAsBitVector(b.size(), false);
for (auto const& scc : *this->sortedSccDecomposition) { for (auto const& scc : *this->sortedSccDecomposition) {
if (scc.isTrivial()) {
if (scc.size() == 1) {
returnValue = solveTrivialScc(*scc.begin(), dir, x, b) && returnValue; returnValue = solveTrivialScc(*scc.begin(), dir, x, b) && returnValue;
} else { } else {
sccRowGroupsAsBitVector.clear(); sccRowGroupsAsBitVector.clear();
@ -142,8 +142,18 @@ namespace storm {
} }
} }
if (hasDiagonalEntry) { if (hasDiagonalEntry) {
if (storm::utility::isZero(denominator)) {
if (!storm::utility::isZero(rowValue)) {
if (rowValue > storm::utility::zero<ValueType>()) {
rowValue = storm::utility::infinity<ValueType>();
} else {
rowValue = -storm::utility::infinity<ValueType>();
}
}
} else {
rowValue /= denominator; rowValue /= denominator;
} }
}
if (firstRow) { if (firstRow) {
xi = std::move(rowValue); xi = std::move(rowValue);
bestRow = row; bestRow = row;

Loading…
Cancel
Save