Browse Source

various fixes for topological min max solver

tempestpy_adaptions
TimQu 7 years ago
parent
commit
aabbea11b8
  1. 2
      src/storm/settings/modules/TopologicalEquationSolverSettings.cpp
  2. 2
      src/storm/solver/StandardMinMaxLinearEquationSolver.cpp
  3. 9
      src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp

2
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<std::string> 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 {

2
src/storm/solver/StandardMinMaxLinearEquationSolver.cpp

@ -36,12 +36,14 @@ namespace storm {
void StandardMinMaxLinearEquationSolver<ValueType>::setMatrix(storm::storage::SparseMatrix<ValueType> const& matrix) {
this->localA = nullptr;
this->A = &matrix;
clearCache();
}
template<typename ValueType>
void StandardMinMaxLinearEquationSolver<ValueType>::setMatrix(storm::storage::SparseMatrix<ValueType>&& matrix) {
this->localA = std::make_unique<storm::storage::SparseMatrix<ValueType>>(std::move(matrix));
this->A = this->localA.get();
clearCache();
}
template<typename ValueType>

9
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<ValueType> sccA = this->A->getSubmatrix(true, sccRowGroups, sccRowGroups);
//std::cout << "Matrix is " << sccA << std::endl;
this->sccSolver->setMatrix(std::move(sccA));
// x Vector

Loading…
Cancel
Save