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

improved printing of result to command line

main
dehnert 8 years ago
parent
603bf3562a
commit
6dce56d0bb
8 changed files with 193 additions and 76 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. 37
      src/storm/modelchecker/results/ExplicitQualitativeCheckResult.cpp
  2. 82
      src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp
  3. 1
      src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.h
  4. 47
      src/storm/modelchecker/results/HybridQuantitativeCheckResult.cpp
  5. 6
      src/storm/modelchecker/results/SymbolicQualitativeCheckResult.cpp
  6. 31
      src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.cpp
  7. 57
      src/storm/utility/constants.cpp
  8. 8
      src/storm/utility/constants.h

37
src/storm/modelchecker/results/ExplicitQualitativeCheckResult.cpp
View File

@ -153,26 +153,45 @@ namespace storm {
}
std::ostream& ExplicitQualitativeCheckResult::writeToStream(std::ostream& out) const {
out << "[";
if (this->isResultForAllStates()) {
out << boost::get<vector_type>(truthValues);
vector_type const& vector = boost::get<vector_type>(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<map_type>(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;
}

82
src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp
View File

@ -84,7 +84,7 @@ namespace storm {
template<typename ValueType>
ValueType ExplicitQuantitativeCheckResult<ValueType>::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<vector_type>(values));
@ -93,10 +93,9 @@ namespace storm {
}
}
template<typename ValueType>
ValueType ExplicitQuantitativeCheckResult<ValueType>::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<vector_type>(values));
@ -105,6 +104,17 @@ namespace storm {
}
}
template<typename ValueType>
std::pair<ValueType, ValueType> ExplicitQuantitativeCheckResult<ValueType>::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<vector_type>(values));
} else {
return storm::utility::minmax(boost::get<map_type>(values));
}
}
template<typename ValueType>
ValueType ExplicitQuantitativeCheckResult<ValueType>::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<typename ValueType>
void print(std::ostream& out, ValueType const& value) {
out << value;
if (std::is_same<ValueType, storm::RationalNumber>::value) {
out << " (approx. " << storm::utility::convertNumber<double>(value) << ")";
}
}
template<typename ValueType>
void printApproxRange(std::ostream& out, ValueType const& min, ValueType const& max) {
if (std::is_same<ValueType, storm::RationalNumber>::value) {
out << " (approx. [" << storm::utility::convertNumber<double>(min) << ", " << storm::utility::convertNumber<double>(max) << "])";
}
}
template<typename ValueType>
std::ostream& ExplicitQuantitativeCheckResult<ValueType>::writeToStream(std::ostream& out) const {
out << "[";
bool minMaxSupported = std::is_same<ValueType, double>::value || std::is_same<ValueType, storm::RationalNumber>::value;
bool printAsRange = false;
if (this->isResultForAllStates()) {
vector_type const& valuesAsVector = boost::get<vector_type>(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<map_type>(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<ValueType, ValueType> minmax = this->getMinMax();
out << "[" << minmax.first << ", " << minmax.second << "]";
printApproxRange(out, minmax.first, minmax.second);
out << " (range)";
}
return out;
}

1
src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.h
View File

@ -56,6 +56,7 @@ namespace storm {
virtual ValueType getMin() const override;
virtual ValueType getMax() const override;
virtual std::pair<ValueType, ValueType> getMinMax() const;
virtual ValueType average() const override;
virtual ValueType sum() const override;

47
src/storm/modelchecker/results/HybridQuantitativeCheckResult.cpp
View File

@ -92,33 +92,42 @@ namespace storm {
template<storm::dd::DdType Type, typename ValueType>
std::ostream& HybridQuantitativeCheckResult<Type, ValueType>::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;
}

6
src/storm/modelchecker/results/SymbolicQualitativeCheckResult.cpp
View File

@ -74,12 +74,12 @@ namespace storm {
template <storm::dd::DdType Type>
std::ostream& SymbolicQualitativeCheckResult<Type>::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;

31
src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.cpp
View File

@ -59,21 +59,28 @@ namespace storm {
template<storm::dd::DdType Type, typename ValueType>
std::ostream& SymbolicQuantitativeCheckResult<Type, ValueType>::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;
}

57
src/storm/utility/constants.cpp
View File

@ -196,42 +196,70 @@ namespace storm {
}
template<>
storm::RationalFunction minimum(std::vector<storm::RationalFunction> const&) {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Minimum for rational functions is not defined");
std::pair<storm::RationalFunction, storm::RationalFunction> minmax(std::vector<storm::RationalFunction> const&) {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Minimum/maximum for rational functions is not defined.");
}
template<typename ValueType>
ValueType minimum(std::vector<ValueType> const& values) {
std::pair<ValueType, ValueType> minmax(std::vector<ValueType> 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<storm::RationalFunction> const&) {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Minimum for rational functions is not defined.");
}
template<typename ValueType>
ValueType minimum(std::vector<ValueType> const& values) {
return minmax(values).first;
}
template<>
storm::RationalFunction maximum(std::vector<storm::RationalFunction> 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<typename ValueType>
ValueType maximum(std::vector<ValueType> const& values) {
return minmax(values).second;
}
template<>
std::pair<storm::RationalFunction, storm::RationalFunction> minmax(std::map<uint64_t, storm::RationalFunction> const&) {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Maximum/maximum for rational functions is not defined.");
}
template< typename K, typename ValueType>
std::pair<ValueType, ValueType> minmax(std::map<K, ValueType> 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<uint64_t, storm::RationalFunction> 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<storm::storage::sparse::state_type, storm::storage::sparse::state_type>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type>& matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type>&& matrixEntry);
template std::pair<double, double> minmax(std::vector<double> const&);
template double minimum(std::vector<double> const&);
template double maximum(std::vector<double> const&);
template std::pair<storm::RationalNumber, storm::RationalNumber> minmax(std::vector<storm::RationalNumber> const&);
template storm::RationalNumber minimum(std::vector<storm::RationalNumber> const&);
template storm::RationalNumber maximum(std::vector<storm::RationalNumber> const&);
template storm::RationalFunction minimum(std::vector<storm::RationalFunction> const&);
template storm::RationalFunction maximum(std::vector<storm::RationalFunction> const&);
template std::pair<double, double> minmax(std::map<uint64_t, double> const&);
template double minimum(std::map<uint64_t, double> const&);
template double maximum(std::map<uint64_t, double> const&);
template std::pair<storm::RationalNumber, storm::RationalNumber> minmax(std::map<uint64_t, storm::RationalNumber> const&);
template storm::RationalNumber minimum(std::map<uint64_t, storm::RationalNumber> const&);
template storm::RationalNumber maximum(std::map<uint64_t, storm::RationalNumber> const&);

8
src/storm/utility/constants.h
View File

@ -52,12 +52,18 @@ namespace storm {
template<typename ValueType>
ValueType simplify(ValueType value);
template<typename ValueType>
std::pair<ValueType, ValueType> minmax(std::vector<ValueType> const& values);
template<typename ValueType>
ValueType minimum(std::vector<ValueType> const& values);
template<typename ValueType>
ValueType maximum(std::vector<ValueType> const& values);
template< typename K, typename ValueType>
std::pair<ValueType, ValueType> minmax(std::map<K, ValueType> const& values);
template< typename K, typename ValueType>
ValueType minimum(std::map<K, ValueType> const& values);

Write Preview
Loading…
Cancel
Save