Storm
A Modern Probabilistic Model Checker
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
ExplicitQuantitativeCheckResult.cpp
Go to the documentation of this file.
1#include "storm/adapters/RationalNumberAdapter.h" // Must come first
2
4
15
16namespace storm {
17namespace modelchecker {
18template<typename ValueType>
22
23template<typename ValueType>
25 // Intentionally left empty.
26}
27
28template<typename ValueType>
30 // Intentionally left empty.
31}
32
33template<typename ValueType>
35 : values(map_type()) {
36 boost::get<map_type>(values).emplace(state, value);
37}
38
39template<typename ValueType>
41 // Intentionally left empty.
42}
43
44template<typename ValueType>
46 // Intentionally left empty.
47}
48
49template<typename ValueType>
50ExplicitQuantitativeCheckResult<ValueType>::ExplicitQuantitativeCheckResult(boost::variant<vector_type, map_type> const& values,
51 boost::optional<std::shared_ptr<storm::storage::Scheduler<ValueType>>> scheduler)
52 : values(values), scheduler(scheduler) {
53 // Intentionally left empty.
54}
55
56template<typename ValueType>
58 boost::optional<std::shared_ptr<storm::storage::Scheduler<ValueType>>> scheduler)
59 : values(std::move(values)), scheduler(scheduler) {
60 // Intentionally left empty.
61}
62
63template<typename ValueType>
65 if (other.isResultForAllStates()) {
66 storm::storage::BitVector const& bvValues = other.getTruthValuesVector();
67
68 vector_type newVector;
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>());
72 }
73
74 values = newVector;
75 } else {
77
78 map_type newMap;
79 for (auto const& e : bitMap) {
80 newMap[e.first] = e.second ? storm::utility::one<ValueType>() : storm::utility::zero<ValueType>();
81 }
82
83 values = newMap;
84 }
85}
86
87template<typename ValueType>
88std::unique_ptr<CheckResult> ExplicitQuantitativeCheckResult<ValueType>::clone() const {
89 return std::make_unique<ExplicitQuantitativeCheckResult<ValueType>>(this->values, this->scheduler);
90}
91
92template<typename ValueType>
96
97template<typename ValueType>
101
102template<typename ValueType>
104 return boost::get<map_type>(values);
105}
106
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.");
112 ExplicitQualitativeCheckResult const& explicitFilter = filter.asExplicitQualitativeCheckResult();
113 ExplicitQualitativeCheckResult::vector_type const& filterTruthValues = explicitFilter.getTruthValuesVector();
114
115 if (this->isResultForAllStates()) {
116 map_type newMap;
117
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]);
121 }
122 this->values = newMap;
123 } else {
124 map_type const& map = boost::get<map_type>(values);
125
126 map_type newMap;
127 for (auto const& element : map) {
128 if (filterTruthValues.get(element.first)) {
129 newMap.insert(element);
130 }
131 }
132
133 STORM_LOG_THROW(newMap.size() == filterTruthValues.getNumberOfSetBits(), storm::exceptions::InvalidOperationException,
134 "The check result fails to contain some results referred to by the filter.");
135
136 this->values = newMap;
137 }
138}
139
140template<typename ValueType>
142 STORM_LOG_THROW(!values.empty(), storm::exceptions::InvalidOperationException, "Minimum of empty set is not defined.");
143
144 if (this->isResultForAllStates()) {
145 return storm::utility::minimum(boost::get<vector_type>(values));
146 } else {
147 return storm::utility::minimum(boost::get<map_type>(values));
148 }
149}
150
151template<typename ValueType>
153 STORM_LOG_THROW(!values.empty(), storm::exceptions::InvalidOperationException, "Minimum of empty set is not defined.");
154
155 if (this->isResultForAllStates()) {
156 return storm::utility::maximum(boost::get<vector_type>(values));
157 } else {
158 return storm::utility::maximum(boost::get<map_type>(values));
159 }
160}
161
162template<typename ValueType>
163std::pair<ValueType, ValueType> ExplicitQuantitativeCheckResult<ValueType>::getMinMax() const {
164 STORM_LOG_THROW(!values.empty(), storm::exceptions::InvalidOperationException, "Minimum/maximum of empty set is not defined.");
165
166 if (this->isResultForAllStates()) {
167 return storm::utility::minmax(boost::get<vector_type>(values));
168 } else {
169 return storm::utility::minmax(boost::get<map_type>(values));
170 }
171}
172
173template<typename ValueType>
175 STORM_LOG_THROW(!values.empty(), storm::exceptions::InvalidOperationException, "Sum of empty set is not defined");
176
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.");
182 sum += element;
183 }
184 } else {
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;
189 }
190 }
191 return sum;
192}
193
194template<typename ValueType>
196 STORM_LOG_THROW(!values.empty(), storm::exceptions::InvalidOperationException, "Average of empty set is not defined");
197
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.");
203 sum += element;
204 }
205 return sum / boost::get<vector_type>(values).size();
206 } else {
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;
211 }
212 return sum / boost::get<map_type>(values).size();
213 }
214}
215
216template<typename ValueType>
218 return static_cast<bool>(scheduler);
219}
220
221template<typename ValueType>
223 this->scheduler = std::move(scheduler);
224}
225
226template<typename ValueType>
228 STORM_LOG_THROW(this->hasScheduler(), storm::exceptions::InvalidOperationException, "Unable to retrieve non-existing scheduler.");
229 return *scheduler.get();
230}
231
232template<typename ValueType>
234 STORM_LOG_THROW(this->hasScheduler(), storm::exceptions::InvalidOperationException, "Unable to retrieve non-existing scheduler.");
235 return *scheduler.get();
236}
237
238template<typename ValueType>
239void print(std::ostream& out, ValueType const& value) {
240 if (value == storm::utility::infinity<ValueType>()) {
241 out << "inf";
242 } else {
243 out << value;
244 if (std::is_same<ValueType, storm::RationalNumber>::value) {
245 out << " (approx. " << storm::utility::convertNumber<double>(value) << ")";
246 }
247 }
248}
249
250template<typename ValueType>
251void printRange(std::ostream& out, ValueType const& min, ValueType const& max) {
252 out << "[";
253 if (min == storm::utility::infinity<ValueType>()) {
254 out << "inf";
255 } else {
256 out << min;
257 }
258 out << ", ";
259 if (max == storm::utility::infinity<ValueType>()) {
260 out << "inf";
261 } else {
262 out << max;
263 }
264 out << "]";
265 if (std::is_same<ValueType, storm::RationalNumber>::value) {
266 out << " (approx. [";
267 if (min == storm::utility::infinity<ValueType>()) {
268 out << "inf";
269 } else {
270 out << storm::utility::convertNumber<double>(min);
271 }
272 out << ", ";
273 if (max == storm::utility::infinity<ValueType>()) {
274 out << "inf";
275 } else {
276 out << storm::utility::convertNumber<double>(max);
277 }
278 out << "])";
279 }
280 out << " (range)";
281}
282
283template<typename ValueType>
284std::ostream& ExplicitQuantitativeCheckResult<ValueType>::writeToStream(std::ostream& out) const {
285 bool minMaxSupported = std::is_same<ValueType, double>::value || std::is_same<ValueType, storm::RationalNumber>::value;
286 bool printAsRange = false;
287
288 if (this->isResultForAllStates()) {
289 vector_type const& valuesAsVector = boost::get<vector_type>(values);
290 if (valuesAsVector.size() >= 10 && minMaxSupported) {
291 printAsRange = true;
292 } else {
293 out << "{";
294 bool first = true;
295 for (auto const& element : valuesAsVector) {
296 if (!first) {
297 out << ", ";
298 } else {
299 first = false;
300 }
301 print(out, element);
302 }
303 out << "}";
304 }
305 } else {
306 map_type const& valuesAsMap = boost::get<map_type>(values);
307 if (valuesAsMap.size() >= 10 && minMaxSupported) {
308 printAsRange = true;
309 } else {
310 if (valuesAsMap.size() == 1) {
311 print(out, valuesAsMap.begin()->second);
312 } else {
313 out << "{";
314 bool first = true;
315 for (auto const& element : valuesAsMap) {
316 if (!first) {
317 out << ", ";
318 } else {
319 first = false;
320 }
321 print(out, element.second);
322 }
323 out << "}";
324 }
325 }
326 }
327
328 if (printAsRange) {
329 std::pair<ValueType, ValueType> minmax = this->getMinMax();
330 printRange(out, minmax.first, minmax.second);
331 }
332
333 return out;
334}
335
336template<typename ValueType>
338 ValueType const& bound) const {
339 if (this->isResultForAllStates()) {
340 vector_type const& valuesAsVector = boost::get<vector_type>(values);
341 storm::storage::BitVector result(valuesAsVector.size());
342 switch (comparisonType) {
344 for (uint_fast64_t index = 0; index < valuesAsVector.size(); ++index) {
345 if (valuesAsVector[index] < bound) {
346 result.set(index);
347 }
348 }
349 break;
351 for (uint_fast64_t index = 0; index < valuesAsVector.size(); ++index) {
352 if (valuesAsVector[index] <= bound) {
353 result.set(index);
354 }
355 }
356 break;
358 for (uint_fast64_t index = 0; index < valuesAsVector.size(); ++index) {
359 if (valuesAsVector[index] > bound) {
360 result.set(index);
361 }
362 }
363 break;
365 for (uint_fast64_t index = 0; index < valuesAsVector.size(); ++index) {
366 if (valuesAsVector[index] >= bound) {
367 result.set(index);
368 }
369 }
370 break;
371 }
372 return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(std::move(result)));
373 } else {
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;
380 }
381 break;
383 for (auto const& element : valuesAsMap) {
384 result[element.first] = element.second <= bound;
385 }
386 break;
388 for (auto const& element : valuesAsMap) {
389 result[element.first] = element.second > bound;
390 }
391 break;
393 for (auto const& element : valuesAsMap) {
394 result[element.first] = element.second >= bound;
395 }
396 break;
397 }
398 return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(std::move(result)));
399 }
400}
401
402#ifdef STORM_HAVE_CARL
403template<>
405 storm::RationalFunction const& bound) const {
406 // Since it is not possible to compare rational functions against bounds, we simply call the base class method.
407 return QuantitativeCheckResult::compareAgainstBound(comparisonType, bound);
408}
409#endif
410
411template<typename ValueType>
413 if (this->isResultForAllStates()) {
414 return boost::get<vector_type>(values)[state];
415 } else {
416 return boost::get<map_type>(values)[state];
417 }
418}
419
420template<typename ValueType>
422 if (this->isResultForAllStates()) {
423 return boost::get<vector_type>(values)[state];
424 } else {
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;
429 }
430}
431
432template<typename ValueType>
436
437template<typename ValueType>
439 return values.which() == 0;
440}
441
442template<typename ValueType>
446
447template<typename ValueType>
449 if (this->isResultForAllStates()) {
450 for (auto& element : boost::get<vector_type>(values)) {
451 element = storm::utility::one<ValueType>() - element;
452 }
453 } else {
454 for (auto& element : boost::get<map_type>(values)) {
455 element.second = storm::utility::one<ValueType>() - element.second;
456 }
457 }
458}
459
460template<typename ValueType>
461void insertJsonEntry(storm::json<ValueType>& json, uint64_t const& id, ValueType const& value,
462 std::optional<storm::storage::sparse::StateValuations> const& stateValuations = std::nullopt,
463 std::optional<storm::models::sparse::StateLabeling> const& stateLabels = std::nullopt) {
464 typename storm::json<ValueType> entry;
465 if (stateValuations) {
466 entry["s"] = stateValuations->template toJson<ValueType>(id);
467 } else {
468 entry["s"] = id;
469 }
470 entry["v"] = value;
471 if (stateLabels) {
472 auto labs = stateLabels->getLabelsOfState(id);
473 entry["l"] = labs;
474 }
475 json.push_back(std::move(entry));
476}
477
478template<typename ValueType>
479storm::json<ValueType> ExplicitQuantitativeCheckResult<ValueType>::toJson(std::optional<storm::storage::sparse::StateValuations> const& stateValuations,
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);
486 }
487 } else {
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);
491 }
492 }
493 return result;
494}
495
496template<>
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.");
500}
501
503
504#ifdef STORM_HAVE_CARL
507#endif
508} // namespace modelchecker
509} // namespace storm
std::map< storm::storage::sparse::state_type, bool > map_type
virtual std::ostream & writeToStream(std::ostream &out) 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
ValueType & operator[](storm::storage::sparse::state_type state)
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 std::pair< ValueType, ValueType > getMinMax() const
virtual void filter(QualitativeCheckResult const &filter) override
Filters the current result wrt.
void setScheduler(std::unique_ptr< storm::storage::Scheduler< ValueType > > &&scheduler)
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.
Definition BitVector.h:18
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.
Definition Scheduler.h:18
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
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)
LabParser.cpp.
Definition cli.cpp:18
nlohmann::basic_json< std::map, std::vector, std::string, bool, int64_t, uint64_t, ValueType > json
Definition JsonForward.h:10