[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.

Generated at Thu Feb 08 05:03:45 UTC 2024 using Jira 9.7.1#970001-sha1:2222b88b221c4928ef0de3161136cc90c8356a66.