storm
storm copied to clipboard
More efficient solution for mismatching modulo semantics
#221 and #225 have dealt with the mismatch between the modulo semantics in C++ and PRISM/JANI for negative operands.
While the solution introduced in PR #225 works (at least for a negative a
in a % b
) , it potentially blows up the expressions.
There might be better ways to deal with this. For example, Expression::simplify
could be extended to detect if both modulo operands are non-negative (which should be the case most of the time)
here is a file with several modulos in there to test.
There also might be other expressions that we treat non-optimally right now.