Summary

test/model needs a way to skip over known issues instead of failing the test.

Motivation

The work on test/model keeps getting periodically blocked by bugs that it finds. For example, there have been several issues that have to be fixed before the workload generator can start emitting the evict operation, because otherwise most daily test runs would find an instance of WT-12966, WT-12971, or WT-12939. Or worse, a patch had to be reverted, and now the workload generator can't safely use even the truncate operation until WT-13232 gets fixed.

It would be very helpful if the test driver could identify whether the test failure was due to a known issue, in which case it could then continue the test. In many such cases it would be difficult to avoid generating workloads that would not fail, so hitting a known issue should be detected either during or after the test.

Suggested Approaches

There are two main ways how we can identify known issues:

1. During the test: If the workload runner determines that it is about to execute an operation that would trigger a known bug, it could raise something like model::known_issue_exception. The workload runner would then just skip the rest of the test. This would essentially amount to modeling known bugs, which is actually an approach that MongoDB has done before in its previous formal modeling efforts, except that we would simplify this by only needing to detect the bug as opposed to simulating its effects. This would be simple to implement for a big class of bugs, but it would require engineering effort for each new bug.
2. After the test: After the test driver generates a minimal reproducer ("reduced counterexample"), it would determine how similar it is to provided workload files in a special directory of workloads that are known to fail. This would require larger engineering effort upfront, but would be probably easier to use afterwards. Handling some bugs may require adding several workload files.