{
  "atomic": {
    "counterexample": [],
    "counterexample_length": null,
    "model": "atomic_check_and_grant",
    "replay_matches_bad_state": false,
    "result": "EXHAUSTED_NO_COUNTEREXAMPLE",
    "scope": {
      "clients": [
        0,
        1
      ],
      "faults": [],
      "network": "not modeled",
      "one_shot_requests": true
    },
    "tampered_trace_rejected": false,
    "visited_states": 15
  },
  "environment": {
    "platform": "Linux-5.10.134-013.16.kangaroo.al8.x86_64-x86_64-with-glibc2.39",
    "python": "3.12.3"
  },
  "experiment": "finite explicit-state lock model",
  "gates": {
    "atomic_model_exhausted_without_mutex_violation": true,
    "split_model_has_replayable_counterexample": true,
    "unfair_stutter_does_not_prove_progress": true
  },
  "liveness": {
    "boundary": "This checks one stuttering lasso, not all liveness cycles or a temporal proof.",
    "enabled_actions": [
      {
        "action": "grant_atomic",
        "client": 0
      },
      {
        "action": "request",
        "client": 1
      }
    ],
    "request_eventually_granted_without_fairness": false,
    "state": {
      "owner": null,
      "phase": [
        "waiting",
        "idle"
      ]
    },
    "unfair_lasso": [
      "stutter",
      "stutter"
    ],
    "weak_fairness_excludes_this_specific_lasso": true
  },
  "not_proved_by_this_python_model": [
    "equivalence between this Python model and the PlusCal specifications",
    "all liveness cycles under a stated fairness condition",
    "the correctness of any lock implementation",
    "IronFleet or Dafny proof obligations"
  ],
  "schema_version": 1,
  "split": {
    "counterexample": [
      {
        "action": "request",
        "after": {
          "owner": null,
          "phase": [
            "waiting",
            "idle"
          ]
        },
        "before": {
          "owner": null,
          "phase": [
            "idle",
            "idle"
          ]
        },
        "client": 0
      },
      {
        "action": "check_free",
        "after": {
          "owner": null,
          "phase": [
            "checked",
            "idle"
          ]
        },
        "before": {
          "owner": null,
          "phase": [
            "waiting",
            "idle"
          ]
        },
        "client": 0
      },
      {
        "action": "request",
        "after": {
          "owner": null,
          "phase": [
            "checked",
            "waiting"
          ]
        },
        "before": {
          "owner": null,
          "phase": [
            "checked",
            "idle"
          ]
        },
        "client": 1
      },
      {
        "action": "check_free",
        "after": {
          "owner": null,
          "phase": [
            "checked",
            "checked"
          ]
        },
        "before": {
          "owner": null,
          "phase": [
            "checked",
            "waiting"
          ]
        },
        "client": 1
      },
      {
        "action": "grant_after_check",
        "after": {
          "owner": 0,
          "phase": [
            "held",
            "checked"
          ]
        },
        "before": {
          "owner": null,
          "phase": [
            "checked",
            "checked"
          ]
        },
        "client": 0
      },
      {
        "action": "grant_after_check",
        "after": {
          "owner": 1,
          "phase": [
            "held",
            "held"
          ]
        },
        "before": {
          "owner": 0,
          "phase": [
            "held",
            "checked"
          ]
        },
        "client": 1
      }
    ],
    "counterexample_length": 6,
    "model": "split_check_then_grant",
    "replay_matches_bad_state": true,
    "result": "COUNTEREXAMPLE",
    "scope": {
      "clients": [
        0,
        1
      ],
      "faults": [],
      "network": "not modeled",
      "one_shot_requests": true
    },
    "tampered_trace_rejected": true,
    "visited_states": 24
  }
}