Inspect the claim.
Change the assumptions.

{
  "schemaVersion": "symbolia.handshake.v1",
  "title": "A stale acknowledgement across restart",
  "scope": "Original illustrative finite protocol model; no production PLC or physical machine is verified.",
  "schema": {
    "variants": "One complete reachable transition graph per start policy; labelled edges include self-loops and distinct actions with the same endpoints.",
    "stateCount": "Number of distinct reachable states including the initial state.",
    "edgeCount": "Number of enabled labelled transitions over all reachable states, including cycles.",
    "startTransitionCount": "Number of reachable robot_start edges, not physical starts observed.",
    "shortestCounterexample": "Null when no violating start edge exists; otherwise an initial state and shortest enabled event sequence ending at a violation.",
    "maxShortestDistance": "Greatest shortest-path distance from the initial state; this is a measured graph statistic, not an exploration bound.",
    "checks": "Executable regression checks for this illustrative checker and witness; not an independent proof of the checker implementation."
  },
  "property": {
    "id": "start_ack_has_current_request_identity",
    "statement": "Every robot_start transition carries a nonempty acknowledgement whose identity equals the active request identity.",
    "evaluatedOn": "robot_start transitions"
  },
  "assumptions": [
    "Exactly one active request at a time; at most two operations with fresh identities 1 then 2, without wraparound or reuse.",
    "Events are atomic and interleaved; all enabled event choices are explored without a fairness assumption.",
    "Restart cancels the active request but preserves both the acknowledgement latch and the issued-operation counter.",
    "A new acknowledgement can name only the current active request; an old one can persist until cleared or replaced.",
    "The environment may acknowledge, clear an acknowledgement, or wait indefinitely; no timeout or progress property is asserted.",
    "Start reads the request and acknowledgement identities atomically; later input changes do not change the provenance recorded for that start.",
    "The second operation is the final one; after it, environment actions and restarts remain possible but no third request is issued."
  ],
  "model": {
    "file": "handshake.mjs",
    "sha256": "045d1bc8ac4787058f3e52eb909073a487309a9fdc1ee49a28525b9a6d590d5c",
    "algorithm": "Breadth-first enumeration to reachable-state closure; no depth cutoff; all enabled labelled transitions checked.",
    "stateFields": {
      "issuedOperations": "Persistent count of issued operations: 0, 1 or 2.",
      "phase": "idle, waiting or started.",
      "requestId": "Active operation identity, or null when idle.",
      "ackId": "Latched acknowledgement identity, or null when empty."
    },
    "operationIds": [
      1,
      2
    ]
  },
  "variants": [
    {
      "id": "naive",
      "title": "Accept any acknowledgement",
      "result": "counterexample",
      "stateCount": 16,
      "edgeCount": 56,
      "startTransitionCount": 3,
      "violatingStartTransitionCount": 1,
      "maxShortestDistance": 6,
      "reachableClosureComplete": true,
      "shortestCounterexample": {
        "length": 5,
        "initialState": {
          "issuedOperations": 0,
          "phase": "idle",
          "requestId": null,
          "ackId": null
        },
        "steps": [
          {
            "index": 1,
            "action": "issue_request_1",
            "from": {
              "issuedOperations": 0,
              "phase": "idle",
              "requestId": null,
              "ackId": null
            },
            "to": {
              "issuedOperations": 1,
              "phase": "waiting",
              "requestId": 1,
              "ackId": null
            },
            "start": null
          },
          {
            "index": 2,
            "action": "environment_ack_current",
            "from": {
              "issuedOperations": 1,
              "phase": "waiting",
              "requestId": 1,
              "ackId": null
            },
            "to": {
              "issuedOperations": 1,
              "phase": "waiting",
              "requestId": 1,
              "ackId": 1
            },
            "start": null
          },
          {
            "index": 3,
            "action": "interrupt_and_restart",
            "from": {
              "issuedOperations": 1,
              "phase": "waiting",
              "requestId": 1,
              "ackId": 1
            },
            "to": {
              "issuedOperations": 1,
              "phase": "idle",
              "requestId": null,
              "ackId": 1
            },
            "start": null
          },
          {
            "index": 4,
            "action": "issue_request_2",
            "from": {
              "issuedOperations": 1,
              "phase": "idle",
              "requestId": null,
              "ackId": 1
            },
            "to": {
              "issuedOperations": 2,
              "phase": "waiting",
              "requestId": 2,
              "ackId": 1
            },
            "start": null
          },
          {
            "index": 5,
            "action": "robot_start",
            "from": {
              "issuedOperations": 2,
              "phase": "waiting",
              "requestId": 2,
              "ackId": 1
            },
            "to": {
              "issuedOperations": 2,
              "phase": "started",
              "requestId": 2,
              "ackId": 1
            },
            "start": {
              "requestId": 2,
              "ackId": 1
            }
          }
        ],
        "violatingStep": 5
      }
    },
    {
      "id": "fixed",
      "title": "Require the current request identity",
      "result": "no_counterexample_in_reachable_closure",
      "stateCount": 15,
      "edgeCount": 50,
      "startTransitionCount": 2,
      "violatingStartTransitionCount": 0,
      "maxShortestDistance": 6,
      "reachableClosureComplete": true,
      "shortestCounterexample": null
    }
  ],
  "limitations": [
    "Reachable closure is exhaustive only for these finite models. Two operation identities do not prove arbitrary lifetime behaviour.",
    "Matching provenance is not evidence of physical fixture engagement, sensor integrity, collision avoidance or functional-safety compliance.",
    "No delayed-message queue, identifier reuse, scan/task scheduling, wall-clock timing, firmware, compiler or PLC source-to-binary relationship is modelled.",
    "A matching acknowledgement can still be incorrect about the physical world; the model does not represent that fault.",
    "No liveness, timeout, recovery-progress or performance guarantee follows from this safety property.",
    "The SHA-256 digest binds the results to this script; it does not prove the script correct or authorise any industrial release."
  ],
  "checks": {
    "passed": true,
    "names": [
      "Both policies permit a matching acknowledgement and reject an empty one",
      "Only the naive policy permits a stale acknowledgement",
      "Both complete reachable graphs are closed under every enabled transition",
      "Environment cycles, clearing and restart persistence are present",
      "Both operation identities can start: fixed success is not vacuous",
      "Naive witness replays and has minimum length in the reachable graph",
      "Fixed provenance property holds on every reachable start transition",
      "Mutation removing the fixed identity comparison is rejected"
    ]
  }
}