{
  "cross_object_invariant": {
    "counterexample_detected": true,
    "invariant": "one username has at most one owner",
    "local_checks_passed": true,
    "merged_state": {
      "user-a": {
        "adds": {
          "mira": [
            "east#1"
          ]
        },
        "clock": {
          "east": 1
        },
        "elements": [
          "mira"
        ],
        "removed": []
      },
      "user-b": {
        "adds": {
          "mira": [
            "west#1"
          ]
        },
        "clock": {
          "west": 1
        },
        "elements": [
          "mira"
        ],
        "removed": []
      }
    },
    "owners": [
      "user-a",
      "user-b"
    ],
    "replicas_converged": true,
    "unique_username_holds": false,
    "username": "mira"
  },
  "environment": {
    "platform": "Linux-5.10.134-013.16.kangaroo.al8.x86_64-x86_64-with-glibc2.39",
    "python": "3.12.3"
  },
  "gates": {
    "counter_join_laws": true,
    "counter_reorder_duplicate_convergence": true,
    "cross_object_counterexample_detected": true,
    "missing_tombstone_mutant_detected": true,
    "orset_observed_remove_semantics": true,
    "orset_reorder_duplicate_convergence": true
  },
  "model": {
    "delivery": "eventual, reordered, duplicated full states",
    "kind": "state_based_crdt",
    "replica_ids_are_unique_and_stable": true
  },
  "mutant": {
    "correct_merge_contains_tea": false,
    "mutant_detected": true,
    "mutant_merge_contains_tea": true,
    "mutation": "forget_removed_tags"
  },
  "not_modeled": [
    "real network, storage, crash recovery, or anti-entropy scheduling",
    "membership changes, replica identifier reuse, or tombstone garbage collection",
    "operation-based or delta-state CRDT delivery",
    "Byzantine replicas or malformed state injection",
    "production multi-primary database APIs, throughput, latency, or metadata growth",
    "read freshness before replicas receive the same update set",
    "cross-object atomicity, uniqueness, or non-negative balance enforcement"
  ],
  "or_set": {
    "base_tag": "seed#1",
    "concurrent_add_survives_observed_remove": true,
    "converged": true,
    "expected_elements": [
      "cake",
      "coffee",
      "tea"
    ],
    "offline_operations": {
      "east": {
        "added": [
          "coffee"
        ],
        "removed_tags": [
          "seed#1"
        ]
      },
      "west": {
        "added": [
          "tea",
          "cake"
        ],
        "concurrent_tea_tag": "west#1"
      }
    },
    "post_sync_remove_elements": {
      "east": [
        "cake",
        "coffee"
      ],
      "west": [
        "cake",
        "coffee"
      ]
    },
    "post_sync_remove_eliminates_observed_tags": true,
    "post_sync_remove_tags": [
      "west#1"
    ],
    "results_by_schedule": {
      "east_west_east": {
        "adds": {
          "cake": [
            "west#2"
          ],
          "coffee": [
            "east#1"
          ],
          "tea": [
            "seed#1",
            "west#1"
          ]
        },
        "clock": {
          "east": 1,
          "seed": 1,
          "west": 2
        },
        "elements": [
          "cake",
          "coffee",
          "tea"
        ],
        "removed": [
          "seed#1"
        ]
      },
      "west_east_west": {
        "adds": {
          "cake": [
            "west#2"
          ],
          "coffee": [
            "east#1"
          ],
          "tea": [
            "seed#1",
            "west#1"
          ]
        },
        "clock": {
          "east": 1,
          "seed": 1,
          "west": 2
        },
        "elements": [
          "cake",
          "coffee",
          "tea"
        ],
        "removed": [
          "seed#1"
        ]
      }
    },
    "stale_replay_does_not_resurrect_removed_tag": true,
    "stale_replay_elements": []
  },
  "pn_counter": {
    "converged": true,
    "delivery_schedules": {
      "east_west_east": [
        {
          "negative": {
            "east": 2
          },
          "positive": {
            "east": 5
          },
          "value": 3
        },
        {
          "negative": {
            "west": 1
          },
          "positive": {
            "west": 4
          },
          "value": 3
        },
        {
          "negative": {
            "east": 2
          },
          "positive": {
            "east": 5
          },
          "value": 3
        }
      ],
      "west_east_west": [
        {
          "negative": {
            "west": 1
          },
          "positive": {
            "west": 4
          },
          "value": 3
        },
        {
          "negative": {
            "east": 2
          },
          "positive": {
            "east": 5
          },
          "value": 3
        },
        {
          "negative": {
            "west": 1
          },
          "positive": {
            "west": 4
          },
          "value": 3
        }
      ]
    },
    "expected_state": {
      "negative": {
        "east": 2,
        "west": 1
      },
      "positive": {
        "east": 5,
        "west": 4
      },
      "value": 6
    },
    "laws": {
      "associative": true,
      "commutative": true,
      "idempotent": true
    },
    "offline_operations": {
      "east": [
        "+5",
        "-2"
      ],
      "west": [
        "+4",
        "-1"
      ]
    },
    "results_by_schedule": {
      "east_west_east": {
        "negative": {
          "east": 2,
          "west": 1
        },
        "positive": {
          "east": 5,
          "west": 4
        },
        "value": 6
      },
      "west_east_west": {
        "negative": {
          "east": 2,
          "west": 1
        },
        "positive": {
          "east": 5,
          "west": 4
        },
        "value": 6
      }
    }
  },
  "schema_version": 1,
  "selected_scenarios": [
    "counter",
    "orset",
    "invariant",
    "mutant"
  ]
}