{
  "cases": {
    "clock_contract": {
      "false_interval_contains_real_time": false,
      "false_interval_passes_after": true,
      "status": "PRECONDITION_VIOLATION_FOUND",
      "wide_honest_interval_waits": true
    },
    "normal_commit": {
      "commit_timestamp": 111,
      "decision_replicated_but_waiting": true,
      "ready_after_earliest_passes": true,
      "status": "PASS"
    },
    "skipped_wait": {
      "scope": "external timestamp order, not standalone KV linearizability",
      "status": "COUNTEREXAMPLE_FOUND",
      "t1": {
        "groups": [
          "A",
          "B"
        ],
        "response": 101,
        "timestamp": 111
      },
      "t2": {
        "groups": [
          "C"
        ],
        "start": 103,
        "timestamp": 105
      },
      "violations": [
        {
          "first_response": 101,
          "first_timestamp": 111,
          "second_start": 103,
          "second_timestamp": 105
        }
      ]
    },
    "snapshot_and_safe_time": {
      "safe_time": {
        "after_resolution_and_apply": 130,
        "lagging_replica": 118,
        "requested": 125,
        "unresolved_prepare": 119
      },
      "separate_reads": [
        0,
        1
      ],
      "snapshot_19": [
        0,
        0
      ],
      "snapshot_20": [
        1,
        1
      ],
      "status": "PASS"
    }
  },
  "limits": [
    "Paxos replication is an asserted state transition",
    "logical integer time is not a TrueTime implementation",
    "finite traces do not cover arbitrary schedules or failures",
    "no network, persistent storage, clock hardware, or cloud API is used"
  ],
  "model": "finite educational traces",
  "overall": "PASS"
}