format_version: "0.1"
properties:
  - id: P1
    kind: invariant
    expression: "!(fill_valve && full)"
    justification: "The fill valve must never open on an already-full bottle (overflow protection)."