Uploaded image for project: 'Core Server'
  1. Core Server
  2. SERVER-43660

Measure percent of TLA+ specs' state space is covered by real tests

    XMLWordPrintableJSON

Details

    • Icon: New Feature New Feature
    • Resolution: Won't Fix
    • Icon: Major - P3 Major - P3
    • None
    • None
    • Replication
    • None
    • Replication

    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.

      Attachments

        Activity

          People

            backlog-server-repl Backlog - Replication Team
            jesse@mongodb.com A. Jesse Jiryu Davis
            Votes:
            0 Vote for this issue
            Watchers:
            3 Start watching this issue

            Dates

              Created:
              Updated:
              Resolved: