Conversation
…nal for scheduler parameter
…nclude IntervalForward in tests
…related components and added tests - Updated AddUncertainty transformer to handle RationalNumber types, allowing for exact arithmetic with RationalInterval. - Modified various helper functions and model checkers to accommodate RationalNumber and RationalInterval. - Introduced new tests for RationalNumber scenarios in model checking and uncertainty transformations. - Ensured compatibility with existing models while expanding functionality for uncertain models using RationalNumber.
|
This includes #832, which should thus be reviewed/merged first? |
…parameters and update tests accordingly
… uncertainty parameter
|
|
||
| #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" | ||
|
|
||
| #include "storm/adapters/IntervalForward.h" |
There was a problem hiding this comment.
It feels a bit strange to use a forward in a cpp file? Or do i miss something?
| .build()) | ||
| .build()); | ||
| this->addOption(storm::settings::OptionBuilder(moduleName, soundOptionName, false, "Sets whether to force sound model checking.").build()); | ||
| this->addOption(storm::settings::OptionBuilder(moduleName, intervalOptionName, false, "Sets whether to enable interval model checking.").build()); |
There was a problem hiding this comment.
Why do we need this? What does this mean? Do we still need this with the recent changes by Tim regarding the ability to parse model files as an interval model based on introspection of the model file?
| #include <optional> | ||
|
|
||
| #include "storm/adapters/IntervalAdapter.h" | ||
| #include "storm/adapters/IntervalForward.h" |
There was a problem hiding this comment.
This should not be necessary if we already include the adapter?
| #include <boost/range/adaptor/reversed.hpp> | ||
| #include <boost/range/irange.hpp> | ||
| #include <functional> | ||
| #include <iostream> |
There was a problem hiding this comment.
this is a really expensive header (especially without PCH).. Why do we need it? If we really need it, does also work?
| } | ||
| }; | ||
| if (storm::solver::minimize(dir)) { | ||
| if (choices) { |
There was a problem hiding this comment.
Why do we maximize when the dir is minimize?
| #include <type_traits> | ||
|
|
||
| #include "storm/adapters/IntervalAdapter.h" | ||
| #include "storm/adapters/IntervalForward.h" |
| method = MinMaxMethod::PolicyIteration; | ||
| } else { | ||
| STORM_LOG_WARN("The selected solution method " << toString(method) << " does not guarantee exact results."); | ||
| // STORM_LOG_WARN("The selected solution method " << toString(method) << " does not guarantee exact results."); |
There was a problem hiding this comment.
I dont think we should comment it out like this :-)
|
Great work! I have not checked the new finite-horizon model checking algorithm (yet). Also, have you checked that we didnt miss (or recently introduce) an instance of std::is_same_v<ValueType, storm::Interval>? I also noted that we are not always consistently using constexpr in front of that, but that is maybe also not so important :) |
3 participants
Add exact Intervals and bounded model checking of intervals