Browse Source

Fixed --sound switch for LRA properties on deterministic models.

tempestpy_adaptions
Tim Quatmann 4 years ago
parent
commit
5bcdb5f95a
  1. 2
      src/storm/modelchecker/helper/infinitehorizon/SparseDeterministicInfiniteHorizonHelper.cpp

2
src/storm/modelchecker/helper/infinitehorizon/SparseDeterministicInfiniteHorizonHelper.cpp

@ -405,6 +405,8 @@ namespace storm {
solver->setBounds(*lowerUpperBounds.first, *lowerUpperBounds.second);
// Check solver requirements
auto requirements = solver->getRequirements(env);
requirements.clearUpperBounds();
requirements.clearLowerBounds();
STORM_LOG_THROW(!requirements.hasEnabledCriticalRequirement(), storm::exceptions::UnmetRequirementException, "Solver requirements " + requirements.getEnabledRequirementsAsString() + " not checked.");
sspValues.assign(sspMatrixVector.first.getRowCount(), (*lowerUpperBounds.first + *lowerUpperBounds.second) / storm::utility::convertNumber<ValueType,uint64_t>(2));
solver->solveEquations(env, sspValues, sspMatrixVector.second);

Loading…
Cancel
Save