import/export of explicit models in (binary) UMB format#875
import/export of explicit models in (binary) UMB format#875tquatmann merged 103 commits intostormchecker:masterfrom
Conversation
|
|
||
| // State valuations | ||
| if (model.hasStateValuations()) { | ||
| STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "State valuations are not yet supported for UMB export."); |
There was a problem hiding this comment.
State valuations are not (fully) supported by this PR yet.
I'd like to replace our existing state valuation representation as it is somewhat incompatible with the UMB state valuations. I fear this will require touching another ~20 files, so maybe we should merge the current PR first.
…e custom extensions more easily
| return static_cast<ToType>(v); | ||
| } | ||
| else if constexpr (std::is_same_v<ToType, int>) | ||
| { |
There was a problem hiding this comment.
Ok. Is this something we should try to get into main modernjson?
There was a problem hiding this comment.
The convert function is mainly needed to handle conversions from and to storm::RationalNumber.
Iirc, we made some more intrusive changes, because a json "float" has to represented as a pointer to a rational number for us.
In any case, we should update our shipped modernjson soon. (currently shipped version is apparently from Nov 2023)
| */ | ||
| std::string toString(Type const type); | ||
|
|
||
| struct SizedType { |
There was a problem hiding this comment.
Should this be part of umb headers? Is a umb representation something that is intimately bound to this json serialization (maybe it is, after all, it is currently foremost a file format...)
There was a problem hiding this comment.
What specifically do you mean by "umb headers"?
Generally, most of the things in storm/storage/umb/model/ are closely tied to the UMB standard (by intention).
On the one side, SizedType and Type could into ModelIndex.h , i.e., the main file describing almost all of the JSON of a UMB model.
However, we also need Type and SizedType in other places where it would be odd to include ModelIndex.h (like in ValueEncoding.h where we do low-level bit stuff).
There was a problem hiding this comment.
My point was mostly whether it makes sense to separate umb from the json representation, but I guess it doesnt make sense, currently).
|
whoop whoop. LGTM. I didnt go over the complete umb code.... |
| return (useDefault && haveRational) || (useRational && !haveInterval); | ||
| } else { | ||
| static_assert(std::is_same_v<ValueType, storm::Interval>, "Unhandled value type"); | ||
| // Rational intervals currently not supported. |
There was a problem hiding this comment.
I currently have #885 working which adds rational intervals. Would it be an idea to implement rational intervals at some point?
There was a problem hiding this comment.
Yes, the UMB code is kind of ready for that. Once both PRs are merged, we can probably add rational intervals easily.
|
Merge?! :-) |
3 participants
Import and export of UMB models.
UmbModelclass that serves as an immediate layer between the raw files and astorm::models::sparse::Model.for_each_fieldfrom Boost.PFR for cleaner JSON (de-)serialization and to import/export the different.binfiles from and to the right location.