Browse Source

fixed one of two issues raised by TQ

tempestpy_adaptions
dehnert 7 years ago
parent
commit
6042588baf
  1. 2
      src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp
  2. 2
      src/storm/utility/graph.cpp

2
src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp

@ -305,7 +305,7 @@ namespace storm {
bool converged = false;
// Choose initial scheduler.
storm::dd::Bdd<DdType> scheduler = this->hasInitialScheduler() ? this->getInitialScheduler() : this->A.sumAbstract(this->columnMetaVariables).maxAbstractRepresentative(this->choiceVariables);
storm::dd::Bdd<DdType> 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.

2
src/storm/utility/graph.cpp

@ -895,7 +895,7 @@ namespace storm {
uint_fast64_t iterations = 0;
while (!frontier.isZero()) {
storm::dd::Bdd<Type> statesAndChoicesWithProbabilityGreater0E = statesWithProbabilityGreater0E.inverseRelationalProductWithExtendedRelation(transitionMatrix, model.getRowVariables(), model.getColumnVariables());
storm::dd::Bdd<Type> statesAndChoicesWithProbabilityGreater0E = frontier.inverseRelationalProductWithExtendedRelation(transitionMatrix, model.getRowVariables(), model.getColumnVariables());
frontier = phiStates && statesAndChoicesWithProbabilityGreater0E.existsAbstract(model.getNondeterminismVariables()) && !statesWithProbabilityGreater0E;
scheduler = scheduler || (frontier && statesAndChoicesWithProbabilityGreater0E).existsAbstractRepresentative(model.getNondeterminismVariables());
statesWithProbabilityGreater0E |= frontier;

Loading…
Cancel
Save