Perfume's current model checking involves repeatedly summing resource deltas as potentially-violating paths are traversed. Some invariants that should already be satisfied in the model can be flagged as violated if floating point error causes the "violating" path to be some tiny amount out of the invariant's resource bound. Note that this bug could crop up even if we didn't do any addition and instead compared ranges directly, so while continual addition of resources certainly exacerbates the bug, it isn't the (only) cause.
Two potential fix options:
Change the internal representation of DTIME and FTIME resources t be BigDecimal objects instead of floats/doubles.
Loosen what we consider a violation by allowing some margin of error during model checking.
After a bit of offline discussion, I'm proceeding with fix 1.
Perfume's current model checking involves repeatedly summing resource deltas as potentially-violating paths are traversed. Some invariants that should already be satisfied in the model can be flagged as violated if floating point error causes the "violating" path to be some tiny amount out of the invariant's resource bound. Note that this bug could crop up even if we didn't do any addition and instead compared ranges directly, so while continual addition of resources certainly exacerbates the bug, it isn't the (only) cause.
Two potential fix options:
After a bit of offline discussion, I'm proceeding with fix 1.