17namespace modelchecker {
18template<
typename ValueType>
23template<
typename ValueType>
28template<
typename ValueType>
33template<
typename ValueType>
36 boost::get<map_type>(values).emplace(state, value);
39template<
typename ValueType>
44template<
typename ValueType>
49template<
typename ValueType>
52 : values(values), scheduler(scheduler) {
56template<
typename ValueType>
59 : values(
std::move(values)), scheduler(scheduler) {
63template<
typename ValueType>
69 newVector.reserve(bvValues.
size());
70 for (std::size_t i = 0, n = bvValues.
size(); i < n; i++) {
71 newVector.push_back(bvValues.
get(i) ? storm::utility::one<ValueType>() : storm::utility::zero<ValueType>());
79 for (
auto const& e : bitMap) {
80 newMap[e.first] = e.second ? storm::utility::one<ValueType>() : storm::utility::zero<ValueType>();
87template<
typename ValueType>
89 return std::make_unique<ExplicitQuantitativeCheckResult<ValueType>>(this->values, this->scheduler);
92template<
typename ValueType>
94 return boost::get<vector_type>(values);
97template<
typename ValueType>
99 return boost::get<vector_type>(values);
102template<
typename ValueType>
104 return boost::get<map_type>(values);
107template<
typename ValueType>
109 STORM_LOG_THROW(filter.isExplicitQualitativeCheckResult(), storm::exceptions::InvalidOperationException,
110 "Cannot filter explicit check result with non-explicit filter.");
111 STORM_LOG_THROW(filter.isResultForAllStates(), storm::exceptions::InvalidOperationException,
"Cannot filter check result with non-complete filter.");
115 if (this->isResultForAllStates()) {
118 for (
auto element : filterTruthValues) {
119 STORM_LOG_THROW(element < this->getValueVector().size(), storm::exceptions::InvalidAccessException,
"Invalid index in results.");
120 newMap.emplace(element, this->getValueVector()[element]);
122 this->values = newMap;
124 map_type const& map = boost::get<map_type>(values);
127 for (
auto const& element : map) {
128 if (filterTruthValues.
get(element.first)) {
129 newMap.insert(element);
134 "The check result fails to contain some results referred to by the filter.");
136 this->values = newMap;
140template<
typename ValueType>
142 STORM_LOG_THROW(!values.empty(), storm::exceptions::InvalidOperationException,
"Minimum of empty set is not defined.");
144 if (this->isResultForAllStates()) {
151template<
typename ValueType>
153 STORM_LOG_THROW(!values.empty(), storm::exceptions::InvalidOperationException,
"Minimum of empty set is not defined.");
155 if (this->isResultForAllStates()) {
162template<
typename ValueType>
164 STORM_LOG_THROW(!values.empty(), storm::exceptions::InvalidOperationException,
"Minimum/maximum of empty set is not defined.");
166 if (this->isResultForAllStates()) {
173template<
typename ValueType>
175 STORM_LOG_THROW(!values.empty(), storm::exceptions::InvalidOperationException,
"Sum of empty set is not defined");
177 ValueType sum = storm::utility::zero<ValueType>();
178 if (this->isResultForAllStates()) {
179 for (
auto& element : boost::get<vector_type>(values)) {
180 STORM_LOG_THROW(element != storm::utility::infinity<ValueType>(), storm::exceptions::InvalidOperationException,
181 "Cannot compute the sum of values containing infinity.");
185 for (
auto& element : boost::get<map_type>(values)) {
186 STORM_LOG_THROW(element.second != storm::utility::infinity<ValueType>(), storm::exceptions::InvalidOperationException,
187 "Cannot compute the sum of values containing infinity.");
188 sum += element.second;
194template<
typename ValueType>
196 STORM_LOG_THROW(!values.empty(), storm::exceptions::InvalidOperationException,
"Average of empty set is not defined");
198 ValueType sum = storm::utility::zero<ValueType>();
199 if (this->isResultForAllStates()) {
200 for (
auto& element : boost::get<vector_type>(values)) {
201 STORM_LOG_THROW(element != storm::utility::infinity<ValueType>(), storm::exceptions::InvalidOperationException,
202 "Cannot compute the average of values containing infinity.");
205 return sum / boost::get<vector_type>(values).size();
207 for (
auto& element : boost::get<map_type>(values)) {
208 STORM_LOG_THROW(element.second != storm::utility::infinity<ValueType>(), storm::exceptions::InvalidOperationException,
209 "Cannot compute the average of values containing infinity.");
210 sum += element.second;
212 return sum / boost::get<map_type>(values).size();
216template<
typename ValueType>
218 return static_cast<bool>(scheduler);
221template<
typename ValueType>
223 this->scheduler = std::move(scheduler);
226template<
typename ValueType>
228 STORM_LOG_THROW(this->hasScheduler(), storm::exceptions::InvalidOperationException,
"Unable to retrieve non-existing scheduler.");
229 return *scheduler.get();
232template<
typename ValueType>
234 STORM_LOG_THROW(this->hasScheduler(), storm::exceptions::InvalidOperationException,
"Unable to retrieve non-existing scheduler.");
235 return *scheduler.get();
238template<
typename ValueType>
239void print(std::ostream& out, ValueType
const& value) {
240 if (value == storm::utility::infinity<ValueType>()) {
244 if (std::is_same<ValueType, storm::RationalNumber>::value) {
245 out <<
" (approx. " << storm::utility::convertNumber<double>(value) <<
")";
239void print(std::ostream& out, ValueType
const& value) {
…}
250template<
typename ValueType>
251void printRange(std::ostream& out, ValueType
const& min, ValueType
const& max) {
253 if (min == storm::utility::infinity<ValueType>()) {
259 if (max == storm::utility::infinity<ValueType>()) {
265 if (std::is_same<ValueType, storm::RationalNumber>::value) {
266 out <<
" (approx. [";
267 if (min == storm::utility::infinity<ValueType>()) {
270 out << storm::utility::convertNumber<double>(min);
273 if (max == storm::utility::infinity<ValueType>()) {
276 out << storm::utility::convertNumber<double>(max);
251void printRange(std::ostream& out, ValueType
const& min, ValueType
const& max) {
…}
283template<
typename ValueType>
285 bool minMaxSupported = std::is_same<ValueType, double>::value || std::is_same<ValueType, storm::RationalNumber>::value;
286 bool printAsRange =
false;
288 if (this->isResultForAllStates()) {
289 vector_type const& valuesAsVector = boost::get<vector_type>(values);
290 if (valuesAsVector.size() >= 10 && minMaxSupported) {
295 for (
auto const& element : valuesAsVector) {
306 map_type const& valuesAsMap = boost::get<map_type>(values);
307 if (valuesAsMap.size() >= 10 && minMaxSupported) {
310 if (valuesAsMap.size() == 1) {
311 print(out, valuesAsMap.begin()->second);
315 for (
auto const& element : valuesAsMap) {
321 print(out, element.second);
329 std::pair<ValueType, ValueType> minmax = this->getMinMax();
336template<
typename ValueType>
338 ValueType
const& bound)
const {
339 if (this->isResultForAllStates()) {
340 vector_type const& valuesAsVector = boost::get<vector_type>(values);
342 switch (comparisonType) {
344 for (uint_fast64_t index = 0; index < valuesAsVector.size(); ++index) {
345 if (valuesAsVector[index] < bound) {
351 for (uint_fast64_t index = 0; index < valuesAsVector.size(); ++index) {
352 if (valuesAsVector[index] <= bound) {
358 for (uint_fast64_t index = 0; index < valuesAsVector.size(); ++index) {
359 if (valuesAsVector[index] > bound) {
365 for (uint_fast64_t index = 0; index < valuesAsVector.size(); ++index) {
366 if (valuesAsVector[index] >= bound) {
374 map_type const& valuesAsMap = boost::get<map_type>(values);
375 std::map<storm::storage::sparse::state_type, bool> result;
376 switch (comparisonType) {
378 for (
auto const& element : valuesAsMap) {
379 result[element.first] = element.second < bound;
383 for (
auto const& element : valuesAsMap) {
384 result[element.first] = element.second <= bound;
388 for (
auto const& element : valuesAsMap) {
389 result[element.first] = element.second > bound;
393 for (
auto const& element : valuesAsMap) {
394 result[element.first] = element.second >= bound;
402#ifdef STORM_HAVE_CARL
411template<
typename ValueType>
413 if (this->isResultForAllStates()) {
414 return boost::get<vector_type>(values)[state];
416 return boost::get<map_type>(values)[state];
420template<
typename ValueType>
422 if (this->isResultForAllStates()) {
423 return boost::get<vector_type>(values)[state];
425 map_type const& valuesAsMap = boost::get<map_type>(values);
426 auto const& keyValuePair = valuesAsMap.find(state);
427 STORM_LOG_THROW(keyValuePair != valuesAsMap.end(), storm::exceptions::InvalidOperationException,
"Unknown key '" << state <<
"'.");
428 return keyValuePair->second;
432template<
typename ValueType>
437template<
typename ValueType>
439 return values.which() == 0;
442template<
typename ValueType>
447template<
typename ValueType>
449 if (this->isResultForAllStates()) {
450 for (
auto& element : boost::get<vector_type>(values)) {
451 element = storm::utility::one<ValueType>() - element;
454 for (
auto& element : boost::get<map_type>(values)) {
455 element.second = storm::utility::one<ValueType>() - element.second;
460template<
typename ValueType>
462 std::optional<storm::storage::sparse::StateValuations>
const& stateValuations = std::nullopt,
463 std::optional<storm::models::sparse::StateLabeling>
const& stateLabels = std::nullopt) {
465 if (stateValuations) {
466 entry[
"s"] = stateValuations->template toJson<ValueType>(
id);
472 auto labs = stateLabels->getLabelsOfState(
id);
475 json.push_back(std::move(entry));
478template<
typename ValueType>
480 std::optional<storm::models::sparse::StateLabeling>
const& stateLabels)
const {
482 if (this->isResultForAllStates()) {
483 vector_type const& valuesAsVector = boost::get<vector_type>(values);
484 for (uint64_t state = 0; state < valuesAsVector.size(); ++state) {
485 insertJsonEntry(result, state, valuesAsVector[state], stateValuations, stateLabels);
488 map_type const& valuesAsMap = boost::get<map_type>(values);
489 for (
auto const& stateValue : valuesAsMap) {
490 insertJsonEntry(result, stateValue.first, stateValue.second, stateValuations, stateLabels);
498 std::optional<storm::storage::sparse::StateValuations>
const&, std::optional<storm::models::sparse::StateLabeling>
const&)
const {
499 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Export of Check results is not supported for Rational Functions.");
504#ifdef STORM_HAVE_CARL
map_type const & getTruthValuesMap() const
std::map< storm::storage::sparse::state_type, bool > map_type
vector_type const & getTruthValuesVector() const
virtual bool isResultForAllStates() const override
virtual std::ostream & writeToStream(std::ostream &out) const override
virtual bool hasScheduler() const override
virtual std::unique_ptr< CheckResult > clone() const override
storm::storage::Scheduler< ValueType > const & getScheduler() const
std::map< storm::storage::sparse::state_type, ValueType > map_type
map_type const & getValueMap() const
ValueType & operator[](storm::storage::sparse::state_type state)
virtual ValueType getMin() const override
ExplicitQuantitativeCheckResult()
storm::json< ValueType > toJson(std::optional< storm::storage::sparse::StateValuations > const &stateValuations=std::nullopt, std::optional< storm::models::sparse::StateLabeling > const &stateLabels=std::nullopt) const
virtual bool isResultForAllStates() const override
virtual bool isExplicit() const override
virtual bool isExplicitQuantitativeCheckResult() const override
virtual ValueType sum() const override
virtual void oneMinus() override
virtual ValueType getMax() const override
std::vector< ValueType > vector_type
virtual std::pair< ValueType, ValueType > getMinMax() const
virtual void filter(QualitativeCheckResult const &filter) override
Filters the current result wrt.
vector_type const & getValueVector() const
void setScheduler(std::unique_ptr< storm::storage::Scheduler< ValueType > > &&scheduler)
virtual ValueType average() const override
virtual std::unique_ptr< CheckResult > compareAgainstBound(storm::logic::ComparisonType comparisonType, ValueType const &bound) const override
virtual std::unique_ptr< CheckResult > compareAgainstBound(storm::logic::ComparisonType comparisonType, ValueType const &bound) const
A bit vector that is internally represented as a vector of 64-bit values.
void set(uint_fast64_t index, bool value=true)
Sets the given truth value at the given index.
size_t size() const
Retrieves the number of bits this bit vector can store.
uint_fast64_t getNumberOfSetBits() const
Returns the number of bits that are set to true in this bit vector.
bool get(uint_fast64_t index) const
Retrieves the truth value of the bit at the given index and performs a bound check.
This class defines which action is chosen in a particular state of a non-deterministic model.
#define STORM_LOG_THROW(cond, exception, message)
void print(std::ostream &out, ValueType const &value)
void printRange(std::ostream &out, ValueType const &min, ValueType const &max)
void insertJsonEntry(storm::json< JsonRationalType > &json, uint64_t const &id, bool value, std::optional< storm::storage::sparse::StateValuations > const &stateValuations=std::nullopt, std::optional< storm::models::sparse::StateLabeling > const &stateLabels=std::nullopt)
ValueType minimum(std::vector< ValueType > const &values)
std::pair< ValueType, ValueType > minmax(std::vector< ValueType > const &values)
ValueType maximum(std::vector< ValueType > const &values)
nlohmann::basic_json< std::map, std::vector, std::string, bool, int64_t, uint64_t, ValueType > json