storm
storm copied to clipboard
moves-rwth
ModernJson is outdated
The difficulty is that we have a patched version: https://github.com/moves-rwth/storm/commit/632c9c2e1e7cdfe36aba1287788021261671164f#diff-e1d25a1c865ce280fc884d097b0030464e4f3e58d24acc4baa0981d3d69a9671.
When redoing these changes, I would suggest to do this not on the single include header, but on the complete project structure. If we could reduce the number of changes necessary that would be even better :-)
Reason to update: e.g., support for compiling with C++20
The modifications were necessary to parse and write floats like e.g. 0.1 exactly. When doing, e.g., exact model checking we want to deal with 1/10 and not whatever IEEE floats get out of that.
Whoever does this update (maybe future me?) should check if there is no major performance regression in parsing and dumping some of the more complicated JANI files. I guess some storm-conv call for the oscillators model in QVBS is a good benchmark.
I am also in favour of updating our dependencies.
Just as a memo to myself: a newer version of modernjson also allows to simplify code (see DFTJsonParser).
Could we, until modernjson supports arbitrary number types, consider a pass in which we replace 0.1 by {/, 1, 10} ? I understand that this may lead to a slight performance regression, but it would simplify our lives.
How would you implement such a pass? You can not really use (vanilla) modernjson for that since it will already have parsed the numbers as inaccurate doubles. So we have to cook up something ourselves, right?
Okay, very pragmatically, when using --exact, we could issue a warning saying that using doubles in jani means that we have doubles as input (as doubles in jani are doubles) and that if you want to ensure exact values, you need to replace doubles by fractions? At least that would be consistent with jani semantics in which doubles are doubles?
At least that would be consistent with jani semantics in which doubles are doubles?
Is this somewhere specified? I couldn't find it in the JANI spec and afaik JSON does not require this either.
I'm fine with implementing this pragmatic solution temporarily between two releases, i.e. after releasing 1.8 and before releasing 1.9 (at which point @tquatmann hopefully re-implements the arbitrary precision handling in modern modernjson).