storm icon indicating copy to clipboard operation
storm copied to clipboard

More efficient solution for mismatching modulo semantics

Open tquatmann opened this issue 2 years ago • 0 comments

#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.

tquatmann avatar May 31 '22 10:05 tquatmann