From d77c285faf1ea79dffa6eb7604c0cc58d46558a9 Mon Sep 17 00:00:00 2001 From: Jip Spel Date: Mon, 28 Jun 2021 12:16:19 +0200 Subject: [PATCH] Fix TODOs --- .../IterativeMinMaxLinearEquationSolver.cpp | 6 +- .../TopologicalMinMaxLinearEquationSolver.cpp | 91 ++++++------------- 2 files changed, 30 insertions(+), 67 deletions(-) diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp index 85d975c6e..d6a088785 100644 --- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp @@ -175,8 +175,7 @@ namespace storm { // Group staat voor de states? for (uint_fast64_t group = 0; group < this->A->getRowGroupCount(); ++group) { uint_fast64_t currentChoice = scheduler[group]; - // TODO: remove, as this should already be fixed by implementation to determine matrix/vector - if (!this->choiceFixedForState || (this->choiceFixedForState && !(this->choiceFixedForState.get()[group]))) { + assert (!this->choiceFixedForState || (this->choiceFixedForState && (!(this->choiceFixedForState.get()[group]) || this->A->getRowGroupSize(group) == 1))); for (uint_fast64_t choice = this->A->getRowGroupIndices()[group]; choice < this->A->getRowGroupIndices()[group + 1]; ++choice) { // If the choice is the currently selected one, we can skip it. @@ -200,9 +199,6 @@ namespace storm { x[group] = std::move(choiceValue); } } - } else { - STORM_LOG_INFO("Ignoring state" << group << " as the choice of this state is fixed"); - } } // If the scheduler did not improve, we are done. diff --git a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp index 5b2740b8f..27d2de8a0 100644 --- a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp @@ -89,14 +89,12 @@ namespace storm { progress.startNewMeasurement(0); for (auto const& scc : *this->sortedSccDecomposition) { if (scc.size() == 1) { - // TODO: directly use localMonRes on this returnValue = solveTrivialScc(*scc.begin(), dir, x, b) && returnValue; } else { STORM_LOG_TRACE("Solving SCC of size " << scc.size() << "."); sccRowGroupsAsBitVector.clear(); sccRowsAsBitVector.clear(); for (auto const& group : scc) { // Group refers to state - bool allIgnored = true; sccRowGroupsAsBitVector.set(group, true); if (!this->choiceFixedForState || !this->choiceFixedForState.get()[group]) { @@ -150,13 +148,12 @@ namespace storm { ValueType& xi = globalX[sccState]; bool firstRow = true; uint64_t bestRow; - if (this->choiceFixedForState && this->choiceFixedForState.get()[sccState]) { - assert (this->hasInitialScheduler()); - uint64_t row = this->A->getRowGroupIndices()[sccState] + this->initialScheduler.get()[sccState]; + assert (!this->choiceFixedForState || !this->choiceFixedForState.get()[sccState] || (this->hasInitialScheduler() && this->A->getRowGroupSize(sccState) == 1)); + for (uint64_t row = this->A->getRowGroupIndices()[sccState]; row < this->A->getRowGroupIndices()[sccState + 1]; ++row) { ValueType rowValue = globalB[row]; bool hasDiagonalEntry = false; ValueType denominator; - for (auto const &entry : this->A->getRow(row)) { + for (auto const& entry : this->A->getRow(row)) { if (entry.getColumn() == sccState) { hasDiagonalEntry = true; denominator = storm::utility::one() - entry.getValue(); @@ -165,69 +162,41 @@ namespace storm { } } if (hasDiagonalEntry) { - STORM_LOG_WARN_COND_DEBUG( storm::NumberTraits::IsExact || !storm::utility::isAlmostZero(denominator) || - storm::utility::isZero(denominator), "State " << sccState << " has a selfloop with probability '1-(" << denominator << ")'. This could be an indication for numerical issues."); - assert (!storm::utility::isZero(denominator)); - rowValue /= denominator; + STORM_LOG_WARN_COND_DEBUG( + storm::NumberTraits::IsExact || !storm::utility::isAlmostZero(denominator) || storm::utility::isZero(denominator), + "State " << sccState << " has a selfloop with probability '1-(" << denominator + << ")'. This could be an indication for numerical issues."); + if (storm::utility::isZero(denominator)) { + // In this case we have a selfloop on this state. This can never an optimal choice: + // When minimizing, we are looking for the largest fixpoint (which will never be attained by this action) + // When maximizing, this choice reflects probability zero (non-optimal) or reward infinity (should already be handled during preprocessing). + continue; + } else { + rowValue /= denominator; + } } - if (minimize(dir)) { + if (firstRow) { xi = std::move(rowValue); + bestRow = row; + firstRow = false; } else { - xi = std::move(rowValue); - } - STORM_LOG_INFO("Ignoring state" << sccState << " as the choice is fixed, current probability for this state is: " << this->schedulerChoices.get()[sccState]); - } else { - for (uint64_t row = this->A->getRowGroupIndices()[sccState]; row < this->A->getRowGroupIndices()[sccState + 1]; ++row) { - ValueType rowValue = globalB[row]; - bool hasDiagonalEntry = false; - ValueType denominator; - for (auto const &entry : this->A->getRow(row)) { - if (entry.getColumn() == sccState) { - hasDiagonalEntry = true; - denominator = storm::utility::one() - entry.getValue(); - } else { - rowValue += entry.getValue() * globalX[entry.getColumn()]; - } - } - if (hasDiagonalEntry) { - STORM_LOG_WARN_COND_DEBUG( - storm::NumberTraits::IsExact || !storm::utility::isAlmostZero(denominator) || - storm::utility::isZero(denominator), - "State " << sccState << " has a selfloop with probability '1-(" << denominator - << ")'. This could be an indication for numerical issues."); - if (storm::utility::isZero(denominator)) { - // In this case we have a selfloop on this state. This can never an optimal choice: - // When minimizing, we are looking for the largest fixpoint (which will never be attained by this action) - // When maximizing, this choice reflects probability zero (non-optimal) or reward infinity (should already be handled during preprocessing). - continue; - } else { - rowValue /= denominator; + if (minimize(dir)) { + if (rowValue < xi) { + xi = std::move(rowValue); + bestRow = row; } - } - if (firstRow) { - xi = std::move(rowValue); - bestRow = row; - firstRow = false; } else { - if (minimize(dir)) { - if (rowValue < xi) { - xi = std::move(rowValue); - bestRow = row; - } - } else { - if (rowValue > xi) { - xi = std::move(rowValue); - bestRow = row; - } + if (rowValue > xi) { + xi = std::move(rowValue); + bestRow = row; } } } - if (this->isTrackSchedulerSet()) { - this->schedulerChoices.get()[sccState] = bestRow - this->A->getRowGroupIndices()[sccState]; - } - STORM_LOG_THROW(!firstRow, storm::exceptions::UnexpectedException, "Empty row group in MinMax equation system."); } - //std::cout << "Solved trivial scc " << sccState << " with result " << globalX[sccState] << std::endl; + if (this->isTrackSchedulerSet()) { + this->schedulerChoices.get()[sccState] = bestRow - this->A->getRowGroupIndices()[sccState]; + } + STORM_LOG_THROW(!firstRow, storm::exceptions::UnexpectedException, "Empty row group in MinMax equation system."); return true; } @@ -301,8 +270,6 @@ namespace storm { } -// std::cout << "Matrix is " << sccA << std::endl; - this->sccSolver->setMatrix(std::move(sccA)); // x Vector