sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Fix TODOs

tempestpy_adaptions
Jip Spel 4 years ago
parent
24fa7c9529
commit
d77c285faf
2 changed files with 30 additions and 67 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 6
      src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
  2. 91
      src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp

6
src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
View File

@ -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.

91
src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp
View File

@ -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<ValueType>() - entry.getValue();
@ -165,69 +162,41 @@ namespace storm {
}
}
if (hasDiagonalEntry) {
STORM_LOG_WARN_COND_DEBUG( storm::NumberTraits<ValueType>::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<ValueType>::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<ValueType>() - entry.getValue();
} else {
rowValue += entry.getValue() * globalX[entry.getColumn()];
}
}
if (hasDiagonalEntry) {
STORM_LOG_WARN_COND_DEBUG(
storm::NumberTraits<ValueType>::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

Write Preview
Loading…
Cancel
Save