From 6042588baf3fbdee35287b51d49324d308e1cdc1 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 24 Nov 2017 17:27:31 +0100 Subject: [PATCH] fixed one of two issues raised by TQ --- src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp | 2 +- src/storm/utility/graph.cpp | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp index 037179e2c..177be55c3 100644 --- a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp @@ -305,7 +305,7 @@ namespace storm { bool converged = false; // Choose initial scheduler. - storm::dd::Bdd scheduler = this->hasInitialScheduler() ? this->getInitialScheduler() : this->A.sumAbstract(this->columnMetaVariables).maxAbstractRepresentative(this->choiceVariables); + storm::dd::Bdd scheduler = this->hasInitialScheduler() ? this->getInitialScheduler() : (this->A.sumAbstract(this->columnMetaVariables).notZero() || b.notZero()).existsAbstractRepresentative(this->choiceVariables); // Initialize linear equation solver. // It should be at least as precise as this solver. diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp index c12ca39e5..a2716ba8d 100644 --- a/src/storm/utility/graph.cpp +++ b/src/storm/utility/graph.cpp @@ -895,7 +895,7 @@ namespace storm { uint_fast64_t iterations = 0; while (!frontier.isZero()) { - storm::dd::Bdd statesAndChoicesWithProbabilityGreater0E = statesWithProbabilityGreater0E.inverseRelationalProductWithExtendedRelation(transitionMatrix, model.getRowVariables(), model.getColumnVariables()); + storm::dd::Bdd statesAndChoicesWithProbabilityGreater0E = frontier.inverseRelationalProductWithExtendedRelation(transitionMatrix, model.getRowVariables(), model.getColumnVariables()); frontier = phiStates && statesAndChoicesWithProbabilityGreater0E.existsAbstract(model.getNondeterminismVariables()) && !statesWithProbabilityGreater0E; scheduler = scheduler || (frontier && statesAndChoicesWithProbabilityGreater0E).existsAbstractRepresentative(model.getNondeterminismVariables()); statesWithProbabilityGreater0E |= frontier;