sosy-lab
Table Min:Max filter produces unexpected results due to rounded values
Consider this unfiltered table from SV-COMP 2025: https://sv-comp.sosy-lab.org/2025/results/results-verified/goblint.2024-11-29_20-22-51.results.SV-COMP25_unreach-call.ReachSafety-Fuzzle.xml.bz2.fixed.xml.bz2.table.html#/table.
With CPU time filter 961: it still shows results with CPU time 960: https://sv-comp.sosy-lab.org/2025/results/results-verified/goblint.2024-11-29_20-22-51.results.SV-COMP25_unreach-call.ReachSafety-Fuzzle.xml.bz2.fixed.xml.bz2.table.html#/table?filter=0(4cpu(value(961%3A))).
Only with filter 962: these get filtered out: https://sv-comp.sosy-lab.org/2025/results/results-verified/goblint.2024-11-29_20-22-51.results.SV-COMP25_unreach-call.ReachSafety-Fuzzle.xml.bz2.fixed.xml.bz2.table.html#/table?filter=0(4cpu(value(962%3A))).
With CPU time filter :960 it doesn't show results with CPU time 960: https://sv-comp.sosy-lab.org/2025/results/results-verified/goblint.2024-11-29_20-22-51.results.SV-COMP25_unreach-call.ReachSafety-Fuzzle.xml.bz2.fixed.xml.bz2.table.html#/table?filter=0(4cpu(value(%3A960))).
Even with filter :961 these get filtered out: https://sv-comp.sosy-lab.org/2025/results/results-verified/goblint.2024-11-29_20-22-51.results.SV-COMP25_unreach-call.ReachSafety-Fuzzle.xml.bz2.fixed.xml.bz2.table.html#/table?filter=0(4cpu(value(%3A961))).
Only with filter :962 they are shown: https://sv-comp.sosy-lab.org/2025/results/results-verified/goblint.2024-11-29_20-22-51.results.SV-COMP25_unreach-call.ReachSafety-Fuzzle.xml.bz2.fixed.xml.bz2.table.html#/table?filter=0(4cpu(value(%3A962))).
It's the same on 3.31-dev tables.
This is caused by rounding. The raw values of these cells is probably something like 961.x, but the rounding of the shown value is to two digits.
I am aware that this is not intuitive, but I am not really sure what the solution should be. Any suggestions?
I'm not sure what the morally and scientifically right approach would be either. Doing the number comparisons on just the rounded results can yield to unexpected results as well. Somehow over- and under-approximating to try to account for both is probably even more confusing.
Perhaps the filtering could be as-is on the raw data, but the table could have asterisks after filtered numbers which seem to violate the filter after rounding. And the tooltip could indicate the raw value. It might not solve the problem, but at least would indicate where something unintuitive has happened without appearing like the table filtering is somehow wrong.
Interesting idea, thanks for bringing it up! I would be fine with it, however, currently I do not have time to implement it (seems relatively complex).