diff --git a/src/storm/modelchecker/results/ExplicitQualitativeCheckResult.cpp b/src/storm/modelchecker/results/ExplicitQualitativeCheckResult.cpp index 5a39247a5..e12de8862 100644 --- a/src/storm/modelchecker/results/ExplicitQualitativeCheckResult.cpp +++ b/src/storm/modelchecker/results/ExplicitQualitativeCheckResult.cpp @@ -153,26 +153,45 @@ namespace storm { } std::ostream& ExplicitQualitativeCheckResult::writeToStream(std::ostream& out) const { - out << "["; if (this->isResultForAllStates()) { - out << boost::get(truthValues); + vector_type const& vector = boost::get(truthValues); + bool allTrue = vector.full(); + bool allFalse = !allTrue && vector.empty(); + if (allTrue) { + out << "{true}"; + } else if (allFalse) { + out << "{false}"; + } else { + out << "{true, false}"; + } } else { std::ios::fmtflags oldflags(std::cout.flags()); out << std::boolalpha; map_type const& map = boost::get(truthValues); - bool first = true; - for (auto const& element : map) { - if (!first) { - out << ", "; + if (map.size() == 1) { + out << map.begin()->second; + } else { + bool allTrue = true; + bool allFalse = true; + for (auto const& entry : map) { + if (entry.second) { + allFalse = false; + } else { + allTrue = false; + } + } + if (allTrue) { + out << "{true}"; + } else if (allFalse) { + out << "{false}"; } else { - first = false; + out << "{true, false}"; } - out << element.second; } + std::cout.flags(oldflags); } - out << "]"; return out; } diff --git a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp index 1af0e1daa..ff46fc8f4 100644 --- a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp +++ b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp @@ -84,7 +84,7 @@ namespace storm { template ValueType ExplicitQuantitativeCheckResult::getMin() const { - STORM_LOG_THROW(!values.empty(),storm::exceptions::InvalidOperationException, "Minimum of empty set is not defined"); + STORM_LOG_THROW(!values.empty(), storm::exceptions::InvalidOperationException, "Minimum of empty set is not defined."); if (this->isResultForAllStates()) { return storm::utility::minimum(boost::get(values)); @@ -93,10 +93,9 @@ namespace storm { } } - template ValueType ExplicitQuantitativeCheckResult::getMax() const { - STORM_LOG_THROW(!values.empty(),storm::exceptions::InvalidOperationException, "Minimum of empty set is not defined"); + STORM_LOG_THROW(!values.empty(), storm::exceptions::InvalidOperationException, "Minimum of empty set is not defined."); if (this->isResultForAllStates()) { return storm::utility::maximum(boost::get(values)); @@ -105,6 +104,17 @@ namespace storm { } } + template + std::pair ExplicitQuantitativeCheckResult::getMinMax() const { + STORM_LOG_THROW(!values.empty(), storm::exceptions::InvalidOperationException, "Minimum/maximum of empty set is not defined."); + + if (this->isResultForAllStates()) { + return storm::utility::minmax(boost::get(values)); + } else { + return storm::utility::minmax(boost::get(values)); + } + } + template ValueType ExplicitQuantitativeCheckResult::sum() const { STORM_LOG_THROW(!values.empty(),storm::exceptions::InvalidOperationException, "Minimum of empty set is not defined"); @@ -156,33 +166,67 @@ namespace storm { return *scheduler.get(); } + template + void print(std::ostream& out, ValueType const& value) { + out << value; + if (std::is_same::value) { + out << " (approx. " << storm::utility::convertNumber(value) << ")"; + } + } + + template + void printApproxRange(std::ostream& out, ValueType const& min, ValueType const& max) { + if (std::is_same::value) { + out << " (approx. [" << storm::utility::convertNumber(min) << ", " << storm::utility::convertNumber(max) << "])"; + } + } + template std::ostream& ExplicitQuantitativeCheckResult::writeToStream(std::ostream& out) const { - out << "["; + bool minMaxSupported = std::is_same::value || std::is_same::value; + bool printAsRange = false; + if (this->isResultForAllStates()) { vector_type const& valuesAsVector = boost::get(values); - bool first = true; - for (auto const& element : valuesAsVector) { - if (!first) { - out << ", "; - } else { - first = false; + if (valuesAsVector.size() >= 10 && minMaxSupported) { + printAsRange = true; + } else { + out << "{"; + bool first = true; + for (auto const& element : valuesAsVector) { + if (!first) { + out << ", "; + } else { + first = false; + } + print(out, element); } - out << element; + out << "}"; } } else { map_type const& valuesAsMap = boost::get(values); - bool first = true; - for (auto const& element : valuesAsMap) { - if (!first) { - out << ", "; - } else { - first = false; + if (valuesAsMap.size() >= 10 && minMaxSupported) { + printAsRange = true; + } else { + bool first = true; + for (auto const& element : valuesAsMap) { + if (!first) { + out << ", "; + } else { + first = false; + } + print(out, element.second); } - out << element.second; } } - out << "]"; + + if (printAsRange) { + std::pair minmax = this->getMinMax(); + out << "[" << minmax.first << ", " << minmax.second << "]"; + printApproxRange(out, minmax.first, minmax.second); + out << " (range)"; + } + return out; } diff --git a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.h b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.h index 87689e50c..9fe1e2c29 100644 --- a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.h +++ b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.h @@ -56,6 +56,7 @@ namespace storm { virtual ValueType getMin() const override; virtual ValueType getMax() const override; + virtual std::pair getMinMax() const; virtual ValueType average() const override; virtual ValueType sum() const override; diff --git a/src/storm/modelchecker/results/HybridQuantitativeCheckResult.cpp b/src/storm/modelchecker/results/HybridQuantitativeCheckResult.cpp index 4fd8a7326..008dab7d1 100644 --- a/src/storm/modelchecker/results/HybridQuantitativeCheckResult.cpp +++ b/src/storm/modelchecker/results/HybridQuantitativeCheckResult.cpp @@ -92,33 +92,42 @@ namespace storm { template std::ostream& HybridQuantitativeCheckResult::writeToStream(std::ostream& out) const { - out << "["; - bool first = true; - if (!this->symbolicStates.isZero()) { - if (this->symbolicValues.isZero()) { - out << "0"; - } else { - for (auto valuationValuePair : this->symbolicValues) { + uint64_t totalNumberOfStates = this->symbolicStates.getNonZeroCount() + this->explicitStates.getNonZeroCount(); + + if (totalNumberOfStates < 10) { + out << "{"; + bool first = true; + if (!this->symbolicStates.isZero()) { + if (this->symbolicValues.isZero()) { + out << "0"; + } else { + for (auto valuationValuePair : this->symbolicValues) { + if (!first) { + out << ", "; + } else { + first = false; + } + out << valuationValuePair.second; + } + } + } + if (!this->explicitStates.isZero()) { + for (auto const& element : this->explicitValues) { if (!first) { out << ", "; } else { first = false; } - out << valuationValuePair.second; - } - } - } - if (!this->explicitStates.isZero()) { - for (auto const& element : this->explicitValues) { - if (!first) { - out << ", "; - } else { - first = false; + out << element; } - out << element; } + out << "}"; + } else { + ValueType min = this->getMin(); + ValueType max = this->getMax(); + + out << "[" << min << ", " << max << "] (range)"; } - out << "]"; return out; } diff --git a/src/storm/modelchecker/results/SymbolicQualitativeCheckResult.cpp b/src/storm/modelchecker/results/SymbolicQualitativeCheckResult.cpp index f593f9596..b638c031f 100644 --- a/src/storm/modelchecker/results/SymbolicQualitativeCheckResult.cpp +++ b/src/storm/modelchecker/results/SymbolicQualitativeCheckResult.cpp @@ -74,12 +74,12 @@ namespace storm { template std::ostream& SymbolicQualitativeCheckResult::writeToStream(std::ostream& out) const { if (states == truthValues) { - out << "[true]" << std::endl; + out << "{true}" << std::endl; } else { if (truthValues.isZero()) { - out << "[false]" << std::endl; + out << "{false}" << std::endl; } else { - out << "[true false]" << std::endl; + out << "{true, false}" << std::endl; } } return out; diff --git a/src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.cpp b/src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.cpp index 0a4b1b665..f46c1dc68 100644 --- a/src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.cpp +++ b/src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.cpp @@ -59,21 +59,28 @@ namespace storm { template std::ostream& SymbolicQuantitativeCheckResult::writeToStream(std::ostream& out) const { - out << "["; - if (this->values.isZero()) { - out << "0"; - } else { - bool first = true; - for (auto valuationValuePair : this->values) { - if (!first) { - out << ", "; - } else { - first = false; + if (states.getNonZeroCount() < 10) { + out << "{"; + if (this->values.isZero()) { + out << "0"; + } else { + bool first = true; + for (auto valuationValuePair : this->values) { + if (!first) { + out << ", "; + } else { + first = false; + } + out << valuationValuePair.second; } - out << valuationValuePair.second; } + out << "}"; + } else { + ValueType min = this->getMin(); + ValueType max = this->getMax(); + + out << "[" << min << ", " << max << "] (range)"; } - out << "]"; return out; } diff --git a/src/storm/utility/constants.cpp b/src/storm/utility/constants.cpp index 42be42060..d5cf20a46 100644 --- a/src/storm/utility/constants.cpp +++ b/src/storm/utility/constants.cpp @@ -196,42 +196,70 @@ namespace storm { } template<> - storm::RationalFunction minimum(std::vector const&) { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Minimum for rational functions is not defined"); + std::pair minmax(std::vector const&) { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Minimum/maximum for rational functions is not defined."); } - + template - ValueType minimum(std::vector const& values) { + std::pair minmax(std::vector const& values) { assert(!values.empty()); ValueType min = values.front(); + ValueType max = values.front(); for (auto const& vt : values) { if (vt < min) { min = vt; } + if (vt > max) { + max = vt; + } } - return min; + return std::make_pair(min, max); + } + + template<> + storm::RationalFunction minimum(std::vector const&) { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Minimum for rational functions is not defined."); + } + + template + ValueType minimum(std::vector const& values) { + return minmax(values).first; } template<> storm::RationalFunction maximum(std::vector const&) { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Maximum for rational functions is not defined"); + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Maximum for rational functions is not defined."); } template ValueType maximum(std::vector const& values) { + return minmax(values).second; + } + + template<> + std::pair minmax(std::map const&) { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Maximum/maximum for rational functions is not defined."); + } + + template< typename K, typename ValueType> + std::pair minmax(std::map const& values) { assert(!values.empty()); - ValueType max = values.front(); + ValueType min = values.begin()->second; + ValueType max = values.begin()->second; for (auto const& vt : values) { - if (vt > max) { - max = vt; + if (vt.second < min) { + min = vt.second; + } + if (vt.second > max) { + max = vt.second; } } - return max; + return std::make_pair(min, max); } - + template<> storm::RationalFunction minimum(std::map const&) { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Minimum for rational functions is not defined"); + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Minimum for rational functions is not defined."); } template< typename K, typename ValueType> @@ -460,19 +488,22 @@ namespace storm { template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); - + template std::pair minmax(std::vector const&); template double minimum(std::vector const&); template double maximum(std::vector const&); + template std::pair minmax(std::vector const&); template storm::RationalNumber minimum(std::vector const&); template storm::RationalNumber maximum(std::vector const&); template storm::RationalFunction minimum(std::vector const&); template storm::RationalFunction maximum(std::vector const&); + template std::pair minmax(std::map const&); template double minimum(std::map const&); template double maximum(std::map const&); + template std::pair minmax(std::map const&); template storm::RationalNumber minimum(std::map const&); template storm::RationalNumber maximum(std::map const&); diff --git a/src/storm/utility/constants.h b/src/storm/utility/constants.h index e66d0e0ad..e8bd62de0 100644 --- a/src/storm/utility/constants.h +++ b/src/storm/utility/constants.h @@ -52,12 +52,18 @@ namespace storm { template ValueType simplify(ValueType value); + template + std::pair minmax(std::vector const& values); + template ValueType minimum(std::vector const& values); template ValueType maximum(std::vector const& values); - + + template< typename K, typename ValueType> + std::pair minmax(std::map const& values); + template< typename K, typename ValueType> ValueType minimum(std::map const& values);