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

adding gap output

tempestpy_adaptions
dehnert 6 years ago
parent
4f4d1f4423
commit
4134630fa6
1 changed files with 15 additions and 6 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. 21
      src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp

21
src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
View File

@ -711,15 +711,19 @@ namespace storm {
if (result) {
return result;
}
ValueType minVal = quantitativeResult.min.getInitialStatesRange().first;
ValueType maxVal = quantitativeResult.max.getInitialStatesRange().second;
ValueType difference = maxVal - minVal;
if (std::is_same<ValueType, double>::value) {
STORM_LOG_INFO("Obtained quantitative bounds [" << minVal << ", " << maxVal << "] on the actual value for the initial states in " << quantitativeWatch.getTimeInMilliseconds() << "ms (after " << totalWatch.getTimeInMilliseconds() << "ms in iteration " << this->iteration << ").");
std::stringstream differenceStream;
differenceStream.setf(std::ios::fixed, std::ios::floatfield);
differenceStream.precision(15);
differenceStream << difference;
STORM_LOG_INFO("Obtained quantitative bounds [" << minVal << ", " << maxVal << "] (difference " << differenceStream.str() << ") on the actual value for the initial states in " << quantitativeWatch.getTimeInMilliseconds() << "ms (after " << totalWatch.getTimeInMilliseconds() << "ms in iteration " << this->iteration << ").");
} else {
STORM_LOG_INFO("Obtained quantitative bounds [" << minVal << ", " << maxVal << "] (approx. [" << storm::utility::convertNumber<double>(minVal) << ", " << storm::utility::convertNumber<double>(maxVal) << "]) on the actual value for the initial states in " << quantitativeWatch.getTimeInMilliseconds() << "ms (after " << totalWatch.getTimeInMilliseconds() << "ms in iteration " << this->iteration << ").");
STORM_LOG_INFO("Obtained quantitative bounds [" << minVal << ", " << maxVal << "] (approx. [" << storm::utility::convertNumber<double>(minVal) << ", " << storm::utility::convertNumber<double>(maxVal) << "], difference " << difference << ") on the actual value for the initial states in " << quantitativeWatch.getTimeInMilliseconds() << "ms (after " << totalWatch.getTimeInMilliseconds() << "ms in iteration " << this->iteration << ").");
}
// (9) Check whether the lower and upper bounds are close enough to terminate with an answer.
result = checkForResultAfterQuantitativeCheck<ValueType>(quantitativeResult.min.getInitialStatesRange().first, quantitativeResult.max.getInitialStatesRange().second, comparator);
@ -1318,10 +1322,15 @@ namespace storm {
ValueType minVal = quantitativeResult.getMin().getRange(initialStates).first;
ValueType maxVal = quantitativeResult.getMax().getRange(initialStates).second;
ValueType difference = maxVal - minVal;
if (std::is_same<ValueType, double>::value) {
STORM_LOG_INFO("Obtained quantitative bounds [" << minVal << ", " << maxVal << "] on the actual value for the initial states in " << quantitativeWatch.getTimeInMilliseconds() << "ms (after " << totalWatch.getTimeInMilliseconds() << "ms in iteration " << this->iteration << ").");
std::stringstream differenceStream;
differenceStream.setf(std::ios::fixed, std::ios::floatfield);
differenceStream.precision(15);
differenceStream << difference;
STORM_LOG_INFO("Obtained quantitative bounds [" << minVal << ", " << maxVal << "] (difference " << differenceStream.str() << ") on the actual value for the initial states in " << quantitativeWatch.getTimeInMilliseconds() << "ms (after " << totalWatch.getTimeInMilliseconds() << "ms in iteration " << this->iteration << ").");
} else {
STORM_LOG_INFO("Obtained quantitative bounds [" << minVal << ", " << maxVal << "] (approx. [" << storm::utility::convertNumber<double>(minVal) << ", " << storm::utility::convertNumber<double>(maxVal) << "]) on the actual value for the initial states in " << quantitativeWatch.getTimeInMilliseconds() << "ms (after " << totalWatch.getTimeInMilliseconds() << "ms in iteration " << this->iteration << ").");
STORM_LOG_INFO("Obtained quantitative bounds [" << minVal << ", " << maxVal << "] (approx. [" << storm::utility::convertNumber<double>(minVal) << ", " << storm::utility::convertNumber<double>(maxVal) << "], difference " << difference << ") on the actual value for the initial states in " << quantitativeWatch.getTimeInMilliseconds() << "ms (after " << totalWatch.getTimeInMilliseconds() << "ms in iteration " << this->iteration << ").");
}
// (9) Check whether the lower and upper bounds are close enough to terminate with an answer.

Write Preview
Loading…
Cancel
Save