Browse Source

Unif+: Update kappa only based on the results at the initial state

main
Tim Quatmann 5 years ago
parent
commit
14f07a2d1a
  1. 7
      src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp

7
src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp

@ -224,7 +224,12 @@ namespace storm {
if (relativePrecision) { if (relativePrecision) {
// Reduce kappa a bit // Reduce kappa a bit
ValueType minValue = *std::min_element(maybeStatesValuesUpper.begin(), maybeStatesValuesUpper.end());
ValueType minValue;
if (relevantMaybeStates) {
minValue = storm::utility::vector::min_if(maybeStatesValuesUpper, relevantMaybeStates.get());
} else {
minValue = *std::min_element(maybeStatesValuesUpper.begin(), maybeStatesValuesUpper.end());
}
minValue *= storm::utility::convertNumber<ValueType>(env.solver().timeBounded().getUnifPlusKappa()); minValue *= storm::utility::convertNumber<ValueType>(env.solver().timeBounded().getUnifPlusKappa());
kappa = std::min(kappa, minValue); kappa = std::min(kappa, minValue);
STORM_LOG_DEBUG("Decreased kappa to " << kappa << "."); STORM_LOG_DEBUG("Decreased kappa to " << kappa << ".");

Loading…
Cancel
Save