Browse Source

return more precise result in dd equation solver

tempestpy_adaptions
dehnert 8 years ago
parent
commit
76c99b55af
  1. 3
      src/storm/modelchecker/results/HybridQuantitativeCheckResult.cpp
  2. 3
      src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.cpp
  3. 3
      src/storm/solver/SymbolicLinearEquationSolver.cpp

3
src/storm/modelchecker/results/HybridQuantitativeCheckResult.cpp

@ -115,6 +115,9 @@ namespace storm {
} }
out << valuationValuePair.second; out << valuationValuePair.second;
} }
if (symbolicStates.getNonZeroCount() != this->symbolicValues.getNonZeroCount()) {
out << ", 0";
}
} }
} }
if (!this->explicitStates.isZero()) { if (!this->explicitStates.isZero()) {

3
src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.cpp

@ -75,6 +75,9 @@ namespace storm {
} }
out << valuationValuePair.second; out << valuationValuePair.second;
} }
if (states.getNonZeroCount() != this->values.getNonZeroCount()) {
out << ", 0";
}
} }
out << "}"; out << "}";
} else { } else {

3
src/storm/solver/SymbolicLinearEquationSolver.cpp

@ -55,10 +55,7 @@ namespace storm {
// Now check if the process already converged within our precision. // Now check if the process already converged within our precision.
converged = xCopy.equalModuloPrecision(tmp, precision, relative); converged = xCopy.equalModuloPrecision(tmp, precision, relative);
// If the method did not converge yet, we prepare the x vector for the next iteration.
if (!converged) {
xCopy = tmp; xCopy = tmp;
}
// Increase iteration count so we can abort if convergence is too slow. // Increase iteration count so we can abort if convergence is too slow.
++iterationCount; ++iterationCount;

Loading…
Cancel
Save