{
  "final_values": {
    "apple": 30,
    "apple_owner": "B",
    "stale_source_has_apple": false,
    "zebra": 7,
    "zebra_owner": "B"
  },
  "history_check": {
    "checked_operations": 10,
    "final_abstract_state": {
      "apple": 30,
      "zebra": 7
    },
    "scope": "complete sequential successful-operation projection",
    "valid": true
  },
  "leader_failure": {
    "elected": "a1",
    "group_a_log_length_after_recovery": 4,
    "restarted_and_caught_up": "a0",
    "stopped": "a0"
  },
  "migration": {
    "destination_install_receipt_count": 1,
    "final_controller": {
      "epoch": 2,
      "migration": {
        "destination": "B",
        "from_epoch": 1,
        "id": "move-shard-0-epoch-2",
        "phase": "done",
        "shard": 0,
        "source": "A",
        "to_epoch": 2
      },
      "owners": {
        "0": "B",
        "1": "B"
      },
      "revision": 6,
      "shard_epochs": {
        "0": 2,
        "1": 1
      }
    },
    "phase_after_crash": "frozen",
    "resume_exit": 0,
    "source_tombstone_epoch": 2,
    "worker_exit_before_controller_receipt": 73
  },
  "model": "bounded file-backed teaching system",
  "not_modeled": [
    "Raft election or arbitrary message schedules",
    "concurrent operations or a general linearizability checker",
    "disk power-loss durability or fsync",
    "concurrent migrations, controller failure, or Byzantine faults",
    "real network, load, or performance"
  ],
  "replica_digests": {
    "A": [
      "e3ff2a7b3729e83abd5c31568cee942b9d5bae1faacd150d9a08a24c7848b6e1"
    ],
    "B": [
      "4ba1d5c438f94cedbd0ae5c2930d077885f4f3ed25d60ab4be8bf2ac0626e81f"
    ]
  },
  "tampered_history_check": {
    "reason": "bad read at step 9",
    "valid": false
  },
  "workload": [
    {
      "acks": [
        "a0",
        "a1",
        "a2"
      ],
      "group": "A",
      "index": 1,
      "key": "apple",
      "op": "put",
      "request_id": "client-1:1",
      "status": "ok",
      "step": 1,
      "value": 10
    },
    {
      "group": "A",
      "key": "apple",
      "op": "get",
      "result": 10,
      "status": "ok",
      "step": 2
    },
    {
      "acks": [
        "b0",
        "b1",
        "b2"
      ],
      "group": "B",
      "index": 1,
      "key": "zebra",
      "op": "put",
      "request_id": "client-2:1",
      "status": "ok",
      "step": 3,
      "value": 7
    },
    {
      "acks": [
        "a1",
        "a2"
      ],
      "group": "A",
      "index": 2,
      "key": "apple",
      "op": "put",
      "request_id": "client-1:2",
      "status": "ok",
      "step": 4,
      "value": 20
    },
    {
      "deduplicated": true,
      "group": "A",
      "key": "apple",
      "op": "put",
      "request_id": "client-1:2",
      "status": "ok",
      "step": 5,
      "value": 20
    },
    {
      "group": "A",
      "key": "apple",
      "op": "get",
      "result": 20,
      "status": "ok",
      "step": 6
    },
    {
      "group": "B",
      "key": "apple",
      "op": "get",
      "result": 20,
      "status": "ok",
      "step": 7
    },
    {
      "acks": [
        "b0",
        "b1",
        "b2"
      ],
      "group": "B",
      "index": 3,
      "key": "apple",
      "op": "put",
      "request_id": "client-1:3",
      "status": "ok",
      "step": 8,
      "value": 30
    },
    {
      "group": "B",
      "key": "apple",
      "op": "get",
      "result": 30,
      "status": "ok",
      "step": 9
    },
    {
      "group": "B",
      "key": "zebra",
      "op": "get",
      "result": 7,
      "status": "ok",
      "step": 10
    },
    {
      "error": "ErrStaleConfig",
      "group": "A",
      "key": "apple",
      "op": "put",
      "request_id": "stale-client:1",
      "status": "error",
      "step": 11,
      "value": 99
    }
  ]
}