|
@ -9,6 +9,7 @@ |
|
|
#include "storm/utility/file.h" |
|
|
#include "storm/utility/file.h" |
|
|
#include "storm/utility/storm-version.h" |
|
|
#include "storm/utility/storm-version.h" |
|
|
#include "storm/utility/macros.h" |
|
|
#include "storm/utility/macros.h" |
|
|
|
|
|
#include "storm/utility/NumberTraits.h" |
|
|
|
|
|
|
|
|
#include "storm/utility/initialize.h" |
|
|
#include "storm/utility/initialize.h" |
|
|
#include "storm/utility/Stopwatch.h" |
|
|
#include "storm/utility/Stopwatch.h" |
|
@ -489,21 +490,22 @@ namespace storm { |
|
|
template<typename ValueType> |
|
|
template<typename ValueType> |
|
|
void printFilteredResult(std::unique_ptr<storm::modelchecker::CheckResult> const& result, storm::modelchecker::FilterType ft) { |
|
|
void printFilteredResult(std::unique_ptr<storm::modelchecker::CheckResult> const& result, storm::modelchecker::FilterType ft) { |
|
|
if (result->isQuantitative()) { |
|
|
if (result->isQuantitative()) { |
|
|
switch (ft) { |
|
|
|
|
|
case storm::modelchecker::FilterType::VALUES: |
|
|
|
|
|
|
|
|
if (ft == storm::modelchecker::FilterType::VALUES) { |
|
|
STORM_PRINT(*result); |
|
|
STORM_PRINT(*result); |
|
|
break; |
|
|
|
|
|
|
|
|
} else { |
|
|
|
|
|
ValueType resultValue; |
|
|
|
|
|
switch (ft) { |
|
|
case storm::modelchecker::FilterType::SUM: |
|
|
case storm::modelchecker::FilterType::SUM: |
|
|
STORM_PRINT(result->asQuantitativeCheckResult<ValueType>().sum()); |
|
|
|
|
|
|
|
|
resultValue = result->asQuantitativeCheckResult<ValueType>().sum(); |
|
|
break; |
|
|
break; |
|
|
case storm::modelchecker::FilterType::AVG: |
|
|
case storm::modelchecker::FilterType::AVG: |
|
|
STORM_PRINT(result->asQuantitativeCheckResult<ValueType>().average()); |
|
|
|
|
|
|
|
|
resultValue = result->asQuantitativeCheckResult<ValueType>().average(); |
|
|
break; |
|
|
break; |
|
|
case storm::modelchecker::FilterType::MIN: |
|
|
case storm::modelchecker::FilterType::MIN: |
|
|
STORM_PRINT(result->asQuantitativeCheckResult<ValueType>().getMin()); |
|
|
|
|
|
|
|
|
resultValue = result->asQuantitativeCheckResult<ValueType>().getMin(); |
|
|
break; |
|
|
break; |
|
|
case storm::modelchecker::FilterType::MAX: |
|
|
case storm::modelchecker::FilterType::MAX: |
|
|
STORM_PRINT(result->asQuantitativeCheckResult<ValueType>().getMax()); |
|
|
|
|
|
|
|
|
resultValue = result->asQuantitativeCheckResult<ValueType>().getMax(); |
|
|
break; |
|
|
break; |
|
|
case storm::modelchecker::FilterType::ARGMIN: |
|
|
case storm::modelchecker::FilterType::ARGMIN: |
|
|
case storm::modelchecker::FilterType::ARGMAX: |
|
|
case storm::modelchecker::FilterType::ARGMAX: |
|
@ -512,6 +514,14 @@ namespace storm { |
|
|
case storm::modelchecker::FilterType::FORALL: |
|
|
case storm::modelchecker::FilterType::FORALL: |
|
|
case storm::modelchecker::FilterType::COUNT: |
|
|
case storm::modelchecker::FilterType::COUNT: |
|
|
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Filter type only defined for qualitative results."); |
|
|
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Filter type only defined for qualitative results."); |
|
|
|
|
|
default: |
|
|
|
|
|
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Unhandled filter type."); |
|
|
|
|
|
} |
|
|
|
|
|
if (storm::NumberTraits<ValueType>::IsExact && storm::utility::isConstant(resultValue)) { |
|
|
|
|
|
STORM_PRINT(resultValue << " (approx. " << storm::utility::convertNumber<double>(resultValue) << ")"); |
|
|
|
|
|
} else { |
|
|
|
|
|
STORM_PRINT(resultValue); |
|
|
|
|
|
} |
|
|
} |
|
|
} |
|
|
} else { |
|
|
} else { |
|
|
switch (ft) { |
|
|
switch (ft) { |
|
|