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

Factor RaftMongo.tla with MongoReplReconfig.tla

    XMLWordPrintableJSON

Details

    • Improvement
    • Status: Backlog
    • Major - P3
    • Resolution: Unresolved
    • None
    • None
    • Replication
    • Replication

    Description

      These two TLA+ specs are actively developed, they are both adapted from siyuan.zhou's original RaftMongo.tla in his personal repository. They have divergent copies of many shared chunks of TLA+ code. Although Leslie Lamport advises against factoring TLA+, we should consider it.

      Attachments

        Issue Links

          Activity

            People

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

              Dates

                Created:
                Updated: