format_version: "0.1"
properties:
  - id: P1
    kind: invariant
    expression: "!Run || !Stop"
    justification: "Stop always drops the seal-in coil: Run and Stop never hold together."