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

Typo in MCRaftMongoReplTimestamp.tla

    • Type: Icon: Bug Bug
    • Resolution: Fixed
    • Priority: Icon: Major - P3 Major - P3
    • 8.1.0-rc0, 8.0.4
    • Affects Version/s: 7.3.0
    • Component/s: None
    • None
    • Replication
    • Fully Compatible
    • ALL
    • v8.0
    • Repl 2024-08-05

      There's a typo in the TLA+ spec for applying oplog entries independently from making them durable:

      Restart(i) ==
          /\ state' = [state EXCEPT ![i] = "Follwer"]
          ...
      

      If restarting a node changes its state to "Follwer", that disables actions which check if its state is "Follower", which means model-checking isn't verifying what we want.

      Also, model-checking could be much faster if you add Symmetry == Permutations(Server) to MCRaftMongoReplTimestamp.tla and add SYMMETRY Symmetry to MCRaftMongoReplTimestamp.cfg

            Assignee:
            jiawei.yang@mongodb.com Jiawei Yang
            Reporter:
            jesse@mongodb.com A. Jesse Jiryu Davis
            Votes:
            0 Vote for this issue
            Watchers:
            4 Start watching this issue

              Created:
              Updated:
              Resolved: