From aabbea11b8379010af96f811e9e51fa9e4756758 Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 18 Jan 2018 19:23:59 +0100 Subject: [PATCH] various fixes for topological min max solver --- .../modules/TopologicalEquationSolverSettings.cpp | 2 +- src/storm/solver/StandardMinMaxLinearEquationSolver.cpp | 2 ++ .../solver/TopologicalMinMaxLinearEquationSolver.cpp | 9 +++++---- 3 files changed, 8 insertions(+), 5 deletions(-) diff --git a/src/storm/settings/modules/TopologicalEquationSolverSettings.cpp b/src/storm/settings/modules/TopologicalEquationSolverSettings.cpp index fd22757ac..d088b2879 100644 --- a/src/storm/settings/modules/TopologicalEquationSolverSettings.cpp +++ b/src/storm/settings/modules/TopologicalEquationSolverSettings.cpp @@ -31,7 +31,7 @@ namespace storm { .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the used solver.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(linearEquationSolver)).setDefaultValueString("gmm++").build()).build()); std::vector minMaxSolvingTechniques = {"vi", "value-iteration", "pi", "policy-iteration", "linear-programming", "lp", "ratsearch", "qvi", "quick-value-iteration"}; this->addOption(storm::settings::OptionBuilder(moduleName, underlyingMinMaxMethodOptionName, true, "Sets which minmax method is considered for solving the underlying minmax equation systems.") - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the used min max method.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(linearEquationSolver)).setDefaultValueString("value-iteration").build()).build()); + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the used min max method.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(minMaxSolvingTechniques)).setDefaultValueString("value-iteration").build()).build()); } bool TopologicalEquationSolverSettings::isUnderlyingEquationSolverTypeSet() const { diff --git a/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp b/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp index 853f84cf3..a377689e4 100644 --- a/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp @@ -36,12 +36,14 @@ namespace storm { void StandardMinMaxLinearEquationSolver::setMatrix(storm::storage::SparseMatrix const& matrix) { this->localA = nullptr; this->A = &matrix; + clearCache(); } template void StandardMinMaxLinearEquationSolver::setMatrix(storm::storage::SparseMatrix&& matrix) { this->localA = std::make_unique>(std::move(matrix)); this->A = this->localA.get(); + clearCache(); } template diff --git a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp index c90dec99b..573f18f3a 100644 --- a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp @@ -185,8 +185,8 @@ namespace storm { // Now add all successors that are not already sorted. // Successors should only be added once, so we first prepare a set of them and add them afterwards. successorSCCs.clear(); - for (auto const& row : currentScc) { - for (auto const& entry : this->A->getRow(row)) { + for (auto const& group : currentScc) { + for (auto const& entry : this->A->getRowGroup(group)) { auto const& successorSCC = sccIndices[entry.getColumn()]; if (successorSCC != currentSccIndex && unsortedSCCs.get(successorSCC)) { successorSCCs.insert(successorSCC); @@ -236,10 +236,10 @@ namespace storm { uint64_t bestRow; for (uint64_t row = this->A->getRowGroupIndices()[sccState]; row < this->A->getRowGroupIndices()[sccState + 1]; ++row) { - ValueType rowValue = globalB[sccState]; + ValueType rowValue = globalB[row]; bool hasDiagonalEntry = false; ValueType denominator; - for (auto const& entry : this->A->getRow(sccState)) { + for (auto const& entry : this->A->getRow(row)) { if (entry.getColumn() == sccState) { STORM_LOG_ASSERT(!storm::utility::isOne(entry.getValue()), "Diagonal entry of fix point system has value 1."); hasDiagonalEntry = true; @@ -319,6 +319,7 @@ namespace storm { // SCC Matrix storm::storage::SparseMatrix sccA = this->A->getSubmatrix(true, sccRowGroups, sccRowGroups); + //std::cout << "Matrix is " << sccA << std::endl; this->sccSolver->setMatrix(std::move(sccA)); // x Vector