[SERVER-43660] Measure percent of TLA+ specs' state space is covered by real tests Created: 26/Sep/19 Updated: 06/Dec/22 Resolved: 09/Jan/20 |
|
| Status: | Closed |
| Project: | Core Server |
| Component/s: | Replication |
| Affects Version/s: | None |
| Fix Version/s: | None |
| Type: | New Feature | Priority: | Major - P3 |
| Reporter: | A. Jesse Jiryu Davis | Assignee: | Backlog - Replication Team |
| Resolution: | Won't Fix | Votes: | 0 |
| Labels: | None | ||
| Remaining Estimate: | Not Specified | ||
| Time Spent: | Not Specified | ||
| Original Estimate: | Not Specified | ||
| Assigned Teams: |
Replication
|
| Participants: |
| Description |
|
For each test, for each TLA+ spec, measure percentage of the spec's state space is covered by the test. Accumulate a combined coverage report for each spec. This might be challenging. There could be billions of states, so tracking whether each one has been covered requires some sort of compression. TLC already does this with "fingerprints" to compress storage of many states, plus something like a Bloom filter? Research how this works. |
| Comments |
| Comment by A. Jesse Jiryu Davis [ 09/Jan/20 ] |
|
Cutting scope, this won't be part of the current paper. |