More useful stats output by privPrecCompare

[michael-schwarz]

Creates list of buckets and boils down comparisons to per-bucket comparisons.

[sim642]

Can you explain in what way has the output changed over time and why the buckets are needed? I don't recall privPrecCompare being changed.

[michael-schwarz]

The output has not changed over time. However, I am now considering many different configurations, and the pairwise output gets tedious:

protection equal to mine-W    (equal: 427, more precise: 0, less precise: 0, incomparable: 0, total: 427)
protection equal to lock    (equal: 427, more precise: 0, less precise: 0, incomparable: 0, total: 427)
protection equal to write    (equal: 427, more precise: 0, less precise: 0, incomparable: 0, total: 427)
protection equal to write+lock    (equal: 427, more precise: 0, less precise: 0, incomparable: 0, total: 427)
protection less precise than protection-interval    (equal: 51, more precise: 0, less precise: 376, incomparable: 0, total: 427)
protection less precise than mine-W-interval    (equal: 51, more precise: 0, less precise: 376, incomparable: 0, total: 427)
protection less precise than lock-interval    (equal: 51, more precise: 0, less precise: 376, incomparable: 0, total: 427)
protection less precise than write-interval    (equal: 51, more precise: 0, less precise: 376, incomparable: 0, total: 427)
protection less precise than write+lock-interval    (equal: 51, more precise: 0, less precise: 376, incomparable: 0, total: 427)
protection equal to protection-tid    (equal: 427, more precise: 0, less precise: 0, incomparable: 0, total: 427)
protection equal to lock-tid    (equal: 427, more precise: 0, less precise: 0, incomparable: 0, total: 427)
protection equal to write-tid    (equal: 427, more precise: 0, less precise: 0, incomparable: 0, total: 427)
protection equal to write+lock-tid    (equal: 427, more precise: 0, less precise: 0, incomparable: 0, total: 427)
protection less precise than protection-tid-interval    (equal: 51, more precise: 0, less precise: 376, incomparable: 0, total: 427)
protection less precise than lock-tid-interval    (equal: 51, more precise: 0, less precise: 376, incomparable: 0, total: 427)
protection less precise than write-tid-interval    (equal: 51, more precise: 0, less precise: 376, incomparable: 0, total: 427)
protection less precise than write+lock-tid-interval    (equal: 51, more precise: 0, less precise: 376, incomparable: 0, total: 427)
...

I have 18 configurations and thus 288 more pairwise comparisons like this (where many have equal precision).

With this PR, we still create the detailed output, but then at the end create buckets of approaches that have the same precision and then output one comparison per bucket.

For example, this output here (all approaches equally precise, TIDs do not matter, intervals pay off) is much easier to intuitively grasp than the 306 pairwise comparisons.

Bucket 0:
  protection-tid
  write
  write+lock-tid
  write+lock
  write-tid
  protection
  mine-W
  lock
  lock-tid
Bucket 1:
  write-interval
  lock-tid-interval
  write-tid-interval
  protection-interval
  mine-W-interval
  protection-tid-interval
  lock-interval
  write+lock-interval
  write+lock-tid-interval
Comparison between bucket 0 and 1: lock less precise than write+lock-tid-interval    (equal: 51, more precise: 0, less precise: 376, incomparable: 0, total: 427)

I merged this only into my dissertation branch for now, but wanted to have a PR we can refer to do decide if we want to merge this also into master.

[sim642]

This looks more human-readable indeed. It might be worth considering to port it into Goblint (possibly with slight generalization for all of our compare business).